more standard bootstrapping of Pure outer syntax;

--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 01 22:12:29 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 01 23:33:26 2012 +0200
@@ -7,38 +7,6 @@
 structure Isar_Syn: sig end =
 struct
 
-(** keywords **)
-
-val _ = Context.>> (Context.map_theory
-  (fold (fn name => (Keyword.define (name, NONE); Thy_Header.declare_keyword (name, NONE)))
-   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
-    "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
-    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
-    "advanced", "and", "assumes", "attach", "begin", "binder",
-    "constrains", "defines", "fixes", "for", "identifier", "if",
-    "imports", "in", "includes", "infix", "infixl", "infixr", "is", "keywords",
-    "notes", "obtains", "open", "output", "overloaded", "pervasive",
-    "shows", "structure", "unchecked", "uses", "where", "|"]));
-
-
-
-(** init and exit **)
-
-val _ =
-  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
-    (Thy_Header.args >> (fn header =>
-      Toplevel.print o
-        Toplevel.init_theory
-          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
-
-val _ =
-  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end context"
-    (Scan.succeed
-      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
-        Toplevel.end_proof (K Proof.end_notepad)));
-
-
-
 (** markup commands **)
 
 val _ =
@@ -109,13 +77,13 @@
 
 val _ =
   Outer_Syntax.command ("classes", Keyword.thy_decl) "declare type classes"
-    (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
+    (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<") |--
         Parse.!!! (Parse.list1 Parse.class)) [])
       >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
 
 val _ =
   Outer_Syntax.command ("classrel", Keyword.thy_decl) "state inclusion of type classes (axiomatic!)"
-    (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
+    (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<")
         |-- Parse.!!! Parse.class))
     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
 
@@ -158,8 +126,6 @@
   Outer_Syntax.command ("consts", Keyword.thy_decl) "declare constants"
     (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
 
-val opt_overloaded = Parse.opt_keyword "overloaded";
-
 val mode_spec =
   (Parse.$$$ "output" >> K ("", false)) ||
     Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
@@ -184,9 +150,9 @@
     -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =
-  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
-    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
-    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
+  ((Parse.$$$ "\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
+    (Parse.$$$ "\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
+    (Parse.$$$ "\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
 
 val trans_line =
   trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
@@ -466,7 +432,7 @@
 val _ =
   Outer_Syntax.command ("sublocale", Keyword.thy_schematic_goal)
     "prove sublocale relation between a locale and a locale expression"
-    (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
+    (Parse.position Parse.xname --| (Parse.$$$ "\<subseteq>" || Parse.$$$ "<") --
       parse_interpretation_arguments false
       >> (fn (loc, (expr, equations)) =>
           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
@@ -513,7 +479,7 @@
 val _ =
   Outer_Syntax.command ("instance", Keyword.thy_goal) "prove type arity or subclass relation"
   ((Parse.class --
-    ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
+    ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
     Parse.multi_arity >> Class.instance_arity_cmd)
     >> (Toplevel.print oo Toplevel.theory_to_proof) ||
     Scan.succeed
@@ -524,7 +490,7 @@
 
 val _ =
   Outer_Syntax.command ("overloading", Keyword.thy_decl) "overloaded definitions"
-   (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
+   (Scan.repeat1 (Parse.name --| (Parse.$$$ "\<equiv>" || Parse.$$$ "==") -- Parse.term --
       Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
       >> Parse.triple1) --| Parse.begin
    >> (fn operations => Toplevel.print o
@@ -639,7 +605,7 @@
     (Parse.and_list1
       (Parse_Spec.opt_thm_name ":" --
         ((Parse.binding -- Parse.opt_mixfix) --
-          ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
+          ((Parse.$$$ "\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
     >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
 
 val _ =
@@ -1041,5 +1007,15 @@
         (Context.set_thread_data (try Toplevel.generic_theory_of state);
           raise Runtime.TERMINATE))));
 
+
+
+(** end **)
+
+val _ =
+  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end context"
+    (Scan.succeed
+      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
+        Toplevel.end_proof (K Proof.end_notepad)));
+
 end;
 

--- a/src/Pure/Pure.thy	Wed Aug 01 22:12:29 2012 +0200
+++ b/src/Pure/Pure.thy	Wed Aug 01 23:33:26 2012 +0200
@@ -1,4 +1,87 @@
 theory Pure
+  keywords
+    "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="
+    "=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>"
+    "\<rightleftharpoons>" "\<subseteq>" "]" "advanced" "and" "assumes"
+    "attach" "begin" "binder" "constrains" "defines" "fixes" "for"
+    "identifier" "if" "imports" "in" "includes" "infix" "infixl"
+    "infixr" "is" "keywords" "notes" "obtains" "open" "output"
+    "overloaded" "pervasive" "shows" "structure" "unchecked" "uses"
+    "where" "|"
+  and "header" :: diag
+  and "chapter" :: thy_heading1
+  and "section" :: thy_heading2
+  and "subsection" :: thy_heading3
+  and "subsubsection" :: thy_heading4
+  and "text" "text_raw" :: thy_decl
+  and "sect" :: prf_heading2 % "proof"
+  and "subsect" :: prf_heading3 % "proof"
+  and "subsubsect" :: prf_heading4 % "proof"
+  and "txt" "txt_raw" :: prf_decl % "proof"
+  and "classes" "classrel" "default_sort" "typedecl" "type_synonym"
+    "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
+    "translations" "no_translations" "axioms" "defs" "definition"
+    "abbreviation" "type_notation" "no_type_notation" "notation"
+    "no_notation" "axiomatization" "theorems" "lemmas" "declare"
+    "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
+  and "use" "ML" :: thy_decl % "ML"
+  and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
+  and "ML_val" "ML_command" :: diag % "ML"
+  and "setup" "local_setup" "attribute_setup" "method_setup"
+    "declaration" "syntax_declaration" "simproc_setup"
+    "parse_ast_translation" "parse_translation" "print_translation"
+    "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
+  and "bundle" :: thy_decl
+  and "include" "including" :: prf_decl
+  and "print_bundles" :: diag
+  and "context" "locale" :: thy_decl
+  and "sublocale" "interpretation" :: thy_schematic_goal
+  and "interpret" :: prf_goal % "proof"  (* FIXME schematic? *)
+  and "class" :: thy_decl
+  and "subclass" :: thy_goal
+  and "instantiation" :: thy_decl
+  and "instance" :: thy_goal
+  and "overloading" :: thy_decl
+  and "code_datatype" :: thy_decl
+  and "theorem" "lemma" "corollary" :: thy_goal
+  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
+  and "notepad" :: thy_decl
+  and "have" "hence" :: prf_goal % "proof"
+  and "show" "thus" :: prf_asm_goal % "proof"
+  and "then" "from" "with" :: prf_chain % "proof"
+  and "note" "using" "unfolding" :: prf_decl % "proof"
+  and "fix" "assume" "presume" "def" :: prf_asm % "proof"
+  and "obtain" "guess" :: prf_asm_goal % "proof"
+  and "let" "write" :: prf_decl % "proof"
+  and "case" :: prf_asm % "proof"
+  and "{" :: prf_open % "proof"
+  and "}" :: prf_close % "proof"
+  and "next" :: prf_block % "proof"
+  and "qed" :: qed_block % "proof"
+  and "by" ".." "." "done" "sorry" :: "qed" % "proof"
+  and "oops" :: qed_global % "proof"
+  and "defer" "prefer" "apply" "apply_end" :: prf_script % "proof"
+  and "proof" :: prf_block % "proof"
+  and "also" "moreover" :: prf_decl % "proof"
+  and "finally" "ultimately" :: prf_chain % "proof"
+  and "back" :: prf_script % "proof"
+  and "Isabelle.command" :: control
+  and "pretty_setmargin" "help" "print_commands" "print_configs"
+    "print_context" "print_theory" "print_syntax" "print_abbrevs"
+    "print_theorems" "print_locales" "print_classes" "print_locale"
+    "print_interps" "print_dependencies" "print_attributes"
+    "print_simpset" "print_rules" "print_trans_rules" "print_methods"
+    "print_antiquotations" "thy_deps" "class_deps" "thm_deps"
+    "print_binds" "print_facts" "print_cases" "print_statement" "thm"
+    "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
+    :: diag
+  and "cd" :: control
+  and "pwd" :: diag
+  and "use_thy" "remove_thy" "kill_thy" :: control
+  and "display_drafts" "print_drafts" "pr" :: diag
+  and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
+  and "end" :: thy_end % "theory"
+  uses "Isar/isar_syn.ML"
 begin
 
 section {* Further content for the Pure theory *}

--- a/src/Pure/ROOT	Wed Aug 01 22:12:29 2012 +0200
+++ b/src/Pure/ROOT	Wed Aug 01 23:33:26 2012 +0200
@@ -105,7 +105,6 @@
     "Isar/expression.ML"
     "Isar/generic_target.ML"
     "Isar/isar_cmd.ML"
-    "Isar/isar_syn.ML"
     "Isar/keyword.ML"
     "Isar/local_defs.ML"
     "Isar/local_theory.ML"

--- a/src/Pure/ROOT.ML	Wed Aug 01 22:12:29 2012 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 01 23:33:26 2012 +0200
@@ -259,7 +259,6 @@
 use "Isar/rule_insts.ML";
 use "Thy/thm_deps.ML";
 use "Isar/isar_cmd.ML";
-use "Isar/isar_syn.ML";
 
 use "subgoal.ML";
 
@@ -302,11 +301,11 @@
 
 use "ProofGeneral/pgip_parser.ML";
 
-use "ProofGeneral/pgip_tests.ML";
-
 use "ProofGeneral/proof_general_pgip.ML";
 use "ProofGeneral/proof_general_emacs.ML";
 
 
 use "pure_setup.ML";
 
+use "ProofGeneral/pgip_tests.ML";
+

--- a/src/Pure/pure_setup.ML	Wed Aug 01 22:12:29 2012 +0200
+++ b/src/Pure/pure_setup.ML	Wed Aug 01 23:33:26 2012 +0200
@@ -14,6 +14,13 @@
 
 (* the Pure theory *)
 
+val _ =
+  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
+    (Thy_Header.args >> (fn header =>
+      Toplevel.print o
+        Toplevel.init_theory
+          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
+
 Unsynchronized.setmp Multithreading.max_threads 1
   use_thy "Pure";
 Context.set_thread_data NONE;