'context': demand 'begin', support local theory;
authorwenzelm
Wed Oct 11 22:55:16 2006 +0200 (2006-10-11)
changeset 209797e5ba4a1f72f
parent 20978 51956522c306
child 20980 e4fd72aecd03
'context': demand 'begin', support local theory;
removed 'undo_end', recovered 'cannot_undo';
tuned Toplevel.begin_local_theory;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Oct 11 22:55:15 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 11 22:55:16 2006 +0200
     1.3 @@ -19,13 +19,14 @@
     1.4  
     1.5  val endP =
     1.6    OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
     1.7 -    (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.exit_local_theory));
     1.8 +    (Scan.succeed (Toplevel.exit o Toplevel.exit_local_theory));
     1.9  
    1.10  val contextP =
    1.11    OuterSyntax.improper_command "context" "switch (local) theory context"
    1.12      (K.tag_theory K.thy_switch)
    1.13 -    (P.name >> (Toplevel.print oo IsarThy.context));
    1.14 -
    1.15 +    (P.name --| P.begin >> (fn name =>
    1.16 +      Toplevel.print o IsarThy.context name o
    1.17 +      Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
    1.18  
    1.19  
    1.20  (** markup commands **)
    1.21 @@ -357,7 +358,8 @@
    1.22          -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
    1.23          -- P.opt_begin
    1.24        >> (fn (((is_open, name), (expr, elems)), begin) =>
    1.25 -          Toplevel.begin_local_theory begin (Locale.add_locale is_open name expr elems)));
    1.26 +          Toplevel.begin_local_theory begin
    1.27 +            (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin)));
    1.28  
    1.29  val interpretationP =
    1.30    OuterSyntax.command "interpretation"
    1.31 @@ -621,13 +623,9 @@
    1.32  
    1.33  (* history *)
    1.34  
    1.35 -val cannot_undoP =    (* FIXME ProofGeneral compatibility *)
    1.36 -  OuterSyntax.improper_command "cannot_undo" "attempt to undo 'end'" K.control
    1.37 -    (P.name >> K (Toplevel.no_timing o IsarCmd.undo_end));
    1.38 -
    1.39 -val undo_endP =
    1.40 -  OuterSyntax.improper_command "undo_end" "attempt to undo 'end'" K.control
    1.41 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo_end));
    1.42 +val cannot_undoP =
    1.43 +  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
    1.44 +    (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
    1.45  
    1.46  val clear_undosP =
    1.47    OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
    1.48 @@ -917,8 +915,8 @@
    1.49    qedP, terminal_proofP, default_proofP, immediate_proofP,
    1.50    done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
    1.51    apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
    1.52 -  cannot_undoP, undo_endP, clear_undosP, redoP, undos_proofP, undoP,
    1.53 -  killP, interpretationP, interpretP,
    1.54 +  cannot_undoP, clear_undosP, redoP, undos_proofP, undoP, killP,
    1.55 +  interpretationP, interpretP,
    1.56    (*diagnostic commands*)
    1.57    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    1.58    print_syntaxP, print_theoremsP, print_localesP, print_localeP,