src/Pure/Isar/isar_syn.ML
changeset 20803 ac78eee049ce
parent 20621 29d57880ba00
child 20907 9673c67dde9b
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Sep 30 21:39:27 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Sep 30 21:39:29 2006 +0200
     1.3 @@ -618,9 +618,13 @@
     1.4  
     1.5  (* history *)
     1.6  
     1.7 -val cannot_undoP =
     1.8 -  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
     1.9 -    (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
    1.10 +val cannot_undoP =    (* FIXME ProofGeneral compatibility *)
    1.11 +  OuterSyntax.improper_command "cannot_undo" "attempt to undo 'end'" K.control
    1.12 +    (P.name >> (Toplevel.no_timing oo IsarCmd.undo_end));
    1.13 +
    1.14 +val undo_endP =
    1.15 +  OuterSyntax.improper_command "undo_end" "attempt to undo 'end'" K.control
    1.16 +    (P.name >> (Toplevel.no_timing oo IsarCmd.undo_end));
    1.17  
    1.18  val clear_undosP =
    1.19    OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
    1.20 @@ -910,8 +914,8 @@
    1.21    terminal_proofP, default_proofP, immediate_proofP, done_proofP,
    1.22    skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
    1.23    proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
    1.24 -  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
    1.25 -  interpretationP, interpretP,
    1.26 +  cannot_undoP, undo_endP, clear_undosP, redoP, undos_proofP, undoP,
    1.27 +  killP, interpretationP, interpretP,
    1.28    (*diagnostic commands*)
    1.29    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    1.30    print_syntaxP, print_theoremsP, print_localesP, print_localeP,