From 3022b60aa7a4d19f52829a2957c1f28dc9f3f1f4 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 3 Jan 2007 21:58:27 +0000 Subject: Demonstrate faulty error reporting. Somewhat obscure, unless some tactics are using Output.error_msg rather than the "error" function. --- etc/isar/FaultyErrors.thy | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 etc/isar/FaultyErrors.thy (limited to 'etc') diff --git a/etc/isar/FaultyErrors.thy b/etc/isar/FaultyErrors.thy new file mode 100644 index 00000000..81e8be1d --- /dev/null +++ b/etc/isar/FaultyErrors.thy @@ -0,0 +1,28 @@ +theory FaultyErrors imports Main +begin + +lemma foo: "P --> P" by auto + +ML_setup {* Output.error_msg "Fake error"; *} (* now *not* an error *) +ML_setup {* error "Real error" :unit; *} (* a true error, command fails *) + +(* After an error message, the system wrongly thinks the + command has succeeded, currently 03.01.07. + This means that undo>redo fails. + + This happens immediately after processing to the error and undoing + all the way back: redoing "theory" in Eclipse fails, because is + used each time, and it doesn't get far enough. Repeating theory gives + the error "can't use theory in theory mode". + + The lemma helps exercise the case that is used + to undo the theory quickly (as it should be, and as it is in + Emacs, by looking at the buffer), which fixes the "theory" redo. + + 1. Do until error + 2. Undo to before lemma + 3. Redo should not give warning message "foo is already defined". + + Now fixed for Eclipse and Emacs in Isabelle >=03.01.07. +*) +end -- cgit v1.2.3