src/Pure/Isar/isar_syn.ML
changeset 6735 e5138b3dbd3b
parent 6727 c8dba1da73cc
child 6742 6b5cb872d997
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed May 26 22:43:50 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed May 26 22:44:41 1999 +0200
     1.3 @@ -325,12 +325,13 @@
     1.4      (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
     1.5  
     1.6  val qed_withP =
     1.7 -  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes" K.qed
     1.8 +  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
     1.9 +    K.qed_block
    1.10      (Scan.option P.name -- Scan.option P.attribs -- Scan.option (P.method -- P.interest)
    1.11        >> (uncurry IsarThy.global_qed_with));
    1.12  
    1.13  val qedP =
    1.14 -  OuterSyntax.command "qed" "conclude (sub-)proof" K.qed
    1.15 +  OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
    1.16      (Scan.option (P.method -- P.interest) >> IsarThy.qed);
    1.17  
    1.18  val terminal_proofP =
    1.19 @@ -364,6 +365,10 @@
    1.20  
    1.21  (* proof history *)
    1.22  
    1.23 +val cannot_undoP =
    1.24 +  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
    1.25 +    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
    1.26 +
    1.27  val clear_undoP =
    1.28    OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
    1.29      (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
    1.30 @@ -525,8 +530,8 @@
    1.31    theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
    1.32    thenP, fromP, factsP, beginP, endP, nextP, kill_proofP, qed_withP,
    1.33    qedP, terminal_proofP, immediate_proofP, default_proofP, refineP,
    1.34 -  then_refineP, proofP, clear_undoP, undoP, redoP, undosP, backP,
    1.35 -  prevP, upP, topP,
    1.36 +  then_refineP, proofP, cannot_undoP, clear_undoP, undoP, redoP,
    1.37 +  undosP, backP, prevP, upP, topP,
    1.38    (*diagnostic commands*)
    1.39    print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
    1.40    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,