src/Pure/Isar/isar_syn.ML
changeset 21306 7ab6e95e6b0b
parent 21269 c605503bb4ef
child 21350 6e58289b6685
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 11 16:11:42 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 11 16:11:43 2006 +0100
     1.3 @@ -21,13 +21,6 @@
     1.4    OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
     1.5      (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
     1.6  
     1.7 -val contextP =
     1.8 -  OuterSyntax.improper_command "context" "switch (local) theory context"
     1.9 -    (K.tag_theory K.thy_switch)
    1.10 -    (P.name --| P.begin >> (fn name =>
    1.11 -      Toplevel.print o IsarThy.context name o
    1.12 -      Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
    1.13 -
    1.14  
    1.15  (** markup commands **)
    1.16  
    1.17 @@ -345,6 +338,14 @@
    1.18        -- P.text >> (Toplevel.theory o PureThy.add_oracle o P.triple1));
    1.19  
    1.20  
    1.21 +(* local theories *)
    1.22 +
    1.23 +val contextP =
    1.24 +  OuterSyntax.command "context" "enter local theory context" K.thy_decl
    1.25 +    (P.name --| P.begin >> (fn name =>
    1.26 +      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.init (SOME name))));
    1.27 +
    1.28 +
    1.29  (* locales *)
    1.30  
    1.31  val locale_val =
    1.32 @@ -896,7 +897,7 @@
    1.33  
    1.34  val _ = OuterSyntax.add_parsers [
    1.35    (*theory structure*)
    1.36 -  theoryP, endP, contextP,
    1.37 +  theoryP, endP,
    1.38    (*markup commands*)
    1.39    headerP, chapterP, sectionP, subsectionP, subsubsectionP, textP,
    1.40    text_rawP, sectP, subsectP, subsubsectP, txtP, txt_rawP,
    1.41 @@ -909,7 +910,7 @@
    1.42    ml_commandP, ml_setupP, setupP, method_setupP,
    1.43    parse_ast_translationP, parse_translationP, print_translationP,
    1.44    typed_print_translationP, print_ast_translationP,
    1.45 -  token_translationP, oracleP, localeP,
    1.46 +  token_translationP, oracleP, contextP, localeP,
    1.47    (*proof commands*)
    1.48    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
    1.49    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,