Opened 16 years ago

Closed 16 years ago

#189 closed defect (fixed)

Undo does not work for diagnostic commands in proofs

Reported by: Stefan Berghofer Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-3.7
Component: 4:prover-isabelle Keywords:
Cc:

Description

When trying to undo a diagnostic command (such as thm) occurring inside a proof, as in 

lemma "True"
  apply (rule TrueI)
  thm TrueI

ProofGeneral crashes with the error message "wrong-type-argument char-or-string-p nil". The error occurs with both XEmacs 21.4 and 21.5.

Attachments (1)

my-trace4​ (4.3 KB) - added by Stefan Berghofer 16 years ago.
Debugger output

Download all attachments as: .zip

Change History (2)

Changed 16 years ago by Stefan Berghofer

Attachment: my-trace4​ added

Debugger output

comment:1 Changed 16 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Fixed. Thanks for reporting this. It was caused by a half-complete code simplification, see task #191.

Note: See TracTickets for help on using tickets.