'end': handle local theory;
authorwenzelm
Wed Oct 11 00:27:31 2006 +0200 (2006-10-11 ago)
changeset 20958802705101b2a
parent 20957 f2a795db0500
child 20959 34cfe3bbeff4
'end': handle local theory;
'locale': begin local theory;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Oct 11 00:27:30 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 11 00:27:31 2006 +0200
     1.3 @@ -17,12 +17,13 @@
     1.4    OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
     1.5      (ThyHeader.args >> (Toplevel.print oo IsarThy.theory));
     1.6  
     1.7 -val end_excursionP =
     1.8 -  OuterSyntax.command "end" "end current excursion" (K.tag_theory K.thy_end)
     1.9 -    (Scan.succeed (Toplevel.print o Toplevel.exit));
    1.10 +val endP =
    1.11 +  OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
    1.12 +    (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.exit_local_theory));
    1.13  
    1.14  val contextP =
    1.15 -  OuterSyntax.improper_command "context" "switch theory context" (K.tag_theory K.thy_switch)
    1.16 +  OuterSyntax.improper_command "context" "switch (local) theory context"
    1.17 +    (K.tag_theory K.thy_switch)
    1.18      (P.name >> (Toplevel.print oo IsarThy.context));
    1.19  
    1.20  
    1.21 @@ -354,8 +355,9 @@
    1.22    OuterSyntax.command "locale" "define named proof context" K.thy_decl
    1.23      ((P.opt_keyword "open" >> not) -- P.name
    1.24          -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
    1.25 -      >> (Toplevel.theory_context o (fn ((is_open, name), (expr, elems)) =>
    1.26 -             Locale.add_locale is_open name expr elems #> (fn ((_, ctxt), thy) => (ctxt, thy)))));
    1.27 +        -- P.opt_begin
    1.28 +      >> (fn (((is_open, name), (expr, elems)), begin) =>
    1.29 +          Toplevel.begin_local_theory begin (Locale.add_locale is_open name expr elems)));
    1.30  
    1.31  val interpretationP =
    1.32    OuterSyntax.command "interpretation"
    1.33 @@ -499,12 +501,12 @@
    1.34  
    1.35  (* proof structure *)
    1.36  
    1.37 -val beginP =
    1.38 +val begin_blockP =
    1.39    OuterSyntax.command "{" "begin explicit proof block"
    1.40      (K.tag_proof K.prf_open)
    1.41      (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
    1.42  
    1.43 -val endP =
    1.44 +val end_blockP =
    1.45    OuterSyntax.command "}" "end explicit proof block"
    1.46      (K.tag_proof K.prf_close)
    1.47      (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
    1.48 @@ -621,11 +623,11 @@
    1.49  
    1.50  val cannot_undoP =    (* FIXME ProofGeneral compatibility *)
    1.51    OuterSyntax.improper_command "cannot_undo" "attempt to undo 'end'" K.control
    1.52 -    (P.name >> (Toplevel.no_timing oo IsarCmd.undo_end));
    1.53 +    (P.name >> K (Toplevel.no_timing o IsarCmd.undo_end));
    1.54  
    1.55  val undo_endP =
    1.56    OuterSyntax.improper_command "undo_end" "attempt to undo 'end'" K.control
    1.57 -    (P.name >> (Toplevel.no_timing oo IsarCmd.undo_end));
    1.58 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo_end));
    1.59  
    1.60  val clear_undosP =
    1.61    OuterSyntax.improper_command "clear_undos" "clear theory-level undo information" K.control
    1.62 @@ -894,7 +896,7 @@
    1.63  
    1.64  val _ = OuterSyntax.add_parsers [
    1.65    (*theory structure*)
    1.66 -  theoryP, end_excursionP, contextP,
    1.67 +  theoryP, endP, contextP,
    1.68    (*markup commands*)
    1.69    headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
    1.70    text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
    1.71 @@ -911,10 +913,10 @@
    1.72    (*proof commands*)
    1.73    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
    1.74    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
    1.75 -  withP, noteP, usingP, unfoldingP, beginP, endP, nextP, qedP,
    1.76 -  terminal_proofP, default_proofP, immediate_proofP, done_proofP,
    1.77 -  skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
    1.78 -  proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
    1.79 +  withP, noteP, usingP, unfoldingP, begin_blockP, end_blockP, nextP,
    1.80 +  qedP, terminal_proofP, default_proofP, immediate_proofP,
    1.81 +  done_proofP, skip_proofP, forget_proofP, deferP, preferP, applyP,
    1.82 +  apply_endP, proofP, alsoP, finallyP, moreoverP, ultimatelyP, backP,
    1.83    cannot_undoP, undo_endP, clear_undosP, redoP, undos_proofP, undoP,
    1.84    killP, interpretationP, interpretP,
    1.85    (*diagnostic commands*)