# HG changeset patch
# User wenzelm
# Date 918245071 -3600
# Node ID ebce4ebba491df8a72ad54d7319b6366471f327f
# Parent  daecd68ecc8c38a7533e231251bdc9689ac2c3f4
improved 'theory';
context / update_context autoload;

diff -r daecd68ecc8c -r ebce4ebba491 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Feb 05 21:03:33 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 05 21:04:31 1999 +0100
@@ -5,6 +5,8 @@
 Pure outer syntax.
 
 TODO:
+  - add_parsers: warn if command name coincides with other keyword (if
+    not already present) (!?);
   - constdefs;
   - axclass axioms: attribs;
   - instance: theory_to_proof (with special attribute to add result arity);
@@ -30,21 +32,23 @@
 
 (** init and exit **)
 
-val contextP =
-  OuterSyntax.parser false "context" "switch theory context"
-    (name >> (fn x => Toplevel.print o Toplevel.init_theory (IsarThy.the_theory x) (K ())));
-
 val theoryP =
   OuterSyntax.parser false "theory" "begin theory"
-    (name -- ($$$ "=" |-- !!! (enum "+" name --| (Scan.ahead eof || $$$ ":")))
-      >> (fn x => Toplevel.print o
-            Toplevel.init_theory (IsarThy.begin_theory x) IsarThy.end_theory));
+    (OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));
 
 (*end current theory / sub-proof / excursion*)
 val endP =
   OuterSyntax.parser false "end" "end current theory / sub-proof / excursion"
     (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
 
+val contextP =
+  OuterSyntax.parser true "context" "switch theory context"
+    (name >> (Toplevel.print oo IsarThy.context));
+
+val update_contextP =
+  OuterSyntax.parser true "update_context" "switch theory context, forcing update"
+    (name >> (Toplevel.print oo IsarThy.update_context));
+
 
 
 (** theory sections **)
@@ -512,7 +516,7 @@
 
 val parsers = [
   (*theory structure*)
-  contextP, theoryP, endP,
+  theoryP, endP, contextP, update_contextP,
   (*theory sections*)
   textP, chapterP, sectionP, subsectionP, subsubsectionP, classesP,
   classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, aritiesP,