# HG changeset patch
# User wenzelm
# Date 927751481 -7200
# Node ID e5138b3dbd3bafaca78c3245afafa2d1b66f90b1
# Parent  151c07f5b70a6a17f73a10c1906d1ba625804556
cannot_undo;
qed_block keywords;

diff -r 151c07f5b70a -r e5138b3dbd3b src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed May 26 22:43:50 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed May 26 22:44:41 1999 +0200
@@ -325,12 +325,13 @@
     (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
 
 val qed_withP =
-  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes" K.qed
+  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
+    K.qed_block
     (Scan.option P.name -- Scan.option P.attribs -- Scan.option (P.method -- P.interest)
       >> (uncurry IsarThy.global_qed_with));
 
 val qedP =
-  OuterSyntax.command "qed" "conclude (sub-)proof" K.qed
+  OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
     (Scan.option (P.method -- P.interest) >> IsarThy.qed);
 
 val terminal_proofP =
@@ -364,6 +365,10 @@
 
 (* proof history *)
 
+val cannot_undoP =
+  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
+    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
+
 val clear_undoP =
   OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
     (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
@@ -525,8 +530,8 @@
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
   thenP, fromP, factsP, beginP, endP, nextP, kill_proofP, qed_withP,
   qedP, terminal_proofP, immediate_proofP, default_proofP, refineP,
-  then_refineP, proofP, clear_undoP, undoP, redoP, undosP, backP,
-  prevP, upP, topP,
+  then_refineP, proofP, cannot_undoP, clear_undoP, undoP, redoP,
+  undosP, backP, prevP, upP, topP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,