more standard bootstrapping of Pure outer syntax;
authorwenzelm
Wed Aug 01 23:33:26 2012 +0200 (2012-08-01)
changeset 4864192b48b8abfe4
parent 48640 053cc8dfde35
child 48642 1737bdb896bb
more standard bootstrapping of Pure outer syntax;
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 01 22:12:29 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 01 23:33:26 2012 +0200
     1.3 @@ -7,38 +7,6 @@
     1.4  structure Isar_Syn: sig end =
     1.5  struct
     1.6  
     1.7 -(** keywords **)
     1.8 -
     1.9 -val _ = Context.>> (Context.map_theory
    1.10 -  (fold (fn name => (Keyword.define (name, NONE); Thy_Header.declare_keyword (name, NONE)))
    1.11 -   ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
    1.12 -    "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
    1.13 -    "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
    1.14 -    "advanced", "and", "assumes", "attach", "begin", "binder",
    1.15 -    "constrains", "defines", "fixes", "for", "identifier", "if",
    1.16 -    "imports", "in", "includes", "infix", "infixl", "infixr", "is", "keywords",
    1.17 -    "notes", "obtains", "open", "output", "overloaded", "pervasive",
    1.18 -    "shows", "structure", "unchecked", "uses", "where", "|"]));
    1.19 -
    1.20 -
    1.21 -
    1.22 -(** init and exit **)
    1.23 -
    1.24 -val _ =
    1.25 -  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
    1.26 -    (Thy_Header.args >> (fn header =>
    1.27 -      Toplevel.print o
    1.28 -        Toplevel.init_theory
    1.29 -          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
    1.30 -
    1.31 -val _ =
    1.32 -  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end context"
    1.33 -    (Scan.succeed
    1.34 -      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
    1.35 -        Toplevel.end_proof (K Proof.end_notepad)));
    1.36 -
    1.37 -
    1.38 -
    1.39  (** markup commands **)
    1.40  
    1.41  val _ =
    1.42 @@ -109,13 +77,13 @@
    1.43  
    1.44  val _ =
    1.45    Outer_Syntax.command ("classes", Keyword.thy_decl) "declare type classes"
    1.46 -    (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
    1.47 +    (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<") |--
    1.48          Parse.!!! (Parse.list1 Parse.class)) [])
    1.49        >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
    1.50  
    1.51  val _ =
    1.52    Outer_Syntax.command ("classrel", Keyword.thy_decl) "state inclusion of type classes (axiomatic!)"
    1.53 -    (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
    1.54 +    (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<")
    1.55          |-- Parse.!!! Parse.class))
    1.56      >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
    1.57  
    1.58 @@ -158,8 +126,6 @@
    1.59    Outer_Syntax.command ("consts", Keyword.thy_decl) "declare constants"
    1.60      (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
    1.61  
    1.62 -val opt_overloaded = Parse.opt_keyword "overloaded";
    1.63 -
    1.64  val mode_spec =
    1.65    (Parse.$$$ "output" >> K ("", false)) ||
    1.66      Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
    1.67 @@ -184,9 +150,9 @@
    1.68      -- Parse.inner_syntax Parse.string;
    1.69  
    1.70  fun trans_arrow toks =
    1.71 -  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
    1.72 -    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
    1.73 -    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
    1.74 +  ((Parse.$$$ "\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
    1.75 +    (Parse.$$$ "\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||
    1.76 +    (Parse.$$$ "\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;
    1.77  
    1.78  val trans_line =
    1.79    trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
    1.80 @@ -466,7 +432,7 @@
    1.81  val _ =
    1.82    Outer_Syntax.command ("sublocale", Keyword.thy_schematic_goal)
    1.83      "prove sublocale relation between a locale and a locale expression"
    1.84 -    (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
    1.85 +    (Parse.position Parse.xname --| (Parse.$$$ "\<subseteq>" || Parse.$$$ "<") --
    1.86        parse_interpretation_arguments false
    1.87        >> (fn (loc, (expr, equations)) =>
    1.88            Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
    1.89 @@ -513,7 +479,7 @@
    1.90  val _ =
    1.91    Outer_Syntax.command ("instance", Keyword.thy_goal) "prove type arity or subclass relation"
    1.92    ((Parse.class --
    1.93 -    ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
    1.94 +    ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
    1.95      Parse.multi_arity >> Class.instance_arity_cmd)
    1.96      >> (Toplevel.print oo Toplevel.theory_to_proof) ||
    1.97      Scan.succeed
    1.98 @@ -524,7 +490,7 @@
    1.99  
   1.100  val _ =
   1.101    Outer_Syntax.command ("overloading", Keyword.thy_decl) "overloaded definitions"
   1.102 -   (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
   1.103 +   (Scan.repeat1 (Parse.name --| (Parse.$$$ "\<equiv>" || Parse.$$$ "==") -- Parse.term --
   1.104        Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
   1.105        >> Parse.triple1) --| Parse.begin
   1.106     >> (fn operations => Toplevel.print o
   1.107 @@ -639,7 +605,7 @@
   1.108      (Parse.and_list1
   1.109        (Parse_Spec.opt_thm_name ":" --
   1.110          ((Parse.binding -- Parse.opt_mixfix) --
   1.111 -          ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
   1.112 +          ((Parse.$$$ "\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
   1.113      >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
   1.114  
   1.115  val _ =
   1.116 @@ -1041,5 +1007,15 @@
   1.117          (Context.set_thread_data (try Toplevel.generic_theory_of state);
   1.118            raise Runtime.TERMINATE))));
   1.119  
   1.120 +
   1.121 +
   1.122 +(** end **)
   1.123 +
   1.124 +val _ =
   1.125 +  Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end context"
   1.126 +    (Scan.succeed
   1.127 +      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
   1.128 +        Toplevel.end_proof (K Proof.end_notepad)));
   1.129 +
   1.130  end;
   1.131  
     2.1 --- a/src/Pure/Pure.thy	Wed Aug 01 22:12:29 2012 +0200
     2.2 +++ b/src/Pure/Pure.thy	Wed Aug 01 23:33:26 2012 +0200
     2.3 @@ -1,4 +1,87 @@
     2.4  theory Pure
     2.5 +  keywords
     2.6 +    "!!" "!" "%" "(" ")" "+" "," "--" ":" "::" ";" "<" "<=" "=" "=="
     2.7 +    "=>" "?" "[" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>"
     2.8 +    "\<rightleftharpoons>" "\<subseteq>" "]" "advanced" "and" "assumes"
     2.9 +    "attach" "begin" "binder" "constrains" "defines" "fixes" "for"
    2.10 +    "identifier" "if" "imports" "in" "includes" "infix" "infixl"
    2.11 +    "infixr" "is" "keywords" "notes" "obtains" "open" "output"
    2.12 +    "overloaded" "pervasive" "shows" "structure" "unchecked" "uses"
    2.13 +    "where" "|"
    2.14 +  and "header" :: diag
    2.15 +  and "chapter" :: thy_heading1
    2.16 +  and "section" :: thy_heading2
    2.17 +  and "subsection" :: thy_heading3
    2.18 +  and "subsubsection" :: thy_heading4
    2.19 +  and "text" "text_raw" :: thy_decl
    2.20 +  and "sect" :: prf_heading2 % "proof"
    2.21 +  and "subsect" :: prf_heading3 % "proof"
    2.22 +  and "subsubsect" :: prf_heading4 % "proof"
    2.23 +  and "txt" "txt_raw" :: prf_decl % "proof"
    2.24 +  and "classes" "classrel" "default_sort" "typedecl" "type_synonym"
    2.25 +    "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
    2.26 +    "translations" "no_translations" "axioms" "defs" "definition"
    2.27 +    "abbreviation" "type_notation" "no_type_notation" "notation"
    2.28 +    "no_notation" "axiomatization" "theorems" "lemmas" "declare"
    2.29 +    "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    2.30 +  and "use" "ML" :: thy_decl % "ML"
    2.31 +  and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    2.32 +  and "ML_val" "ML_command" :: diag % "ML"
    2.33 +  and "setup" "local_setup" "attribute_setup" "method_setup"
    2.34 +    "declaration" "syntax_declaration" "simproc_setup"
    2.35 +    "parse_ast_translation" "parse_translation" "print_translation"
    2.36 +    "typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
    2.37 +  and "bundle" :: thy_decl
    2.38 +  and "include" "including" :: prf_decl
    2.39 +  and "print_bundles" :: diag
    2.40 +  and "context" "locale" :: thy_decl
    2.41 +  and "sublocale" "interpretation" :: thy_schematic_goal
    2.42 +  and "interpret" :: prf_goal % "proof"  (* FIXME schematic? *)
    2.43 +  and "class" :: thy_decl
    2.44 +  and "subclass" :: thy_goal
    2.45 +  and "instantiation" :: thy_decl
    2.46 +  and "instance" :: thy_goal
    2.47 +  and "overloading" :: thy_decl
    2.48 +  and "code_datatype" :: thy_decl
    2.49 +  and "theorem" "lemma" "corollary" :: thy_goal
    2.50 +  and "schematic_theorem" "schematic_lemma" "schematic_corollary" :: thy_schematic_goal
    2.51 +  and "notepad" :: thy_decl
    2.52 +  and "have" "hence" :: prf_goal % "proof"
    2.53 +  and "show" "thus" :: prf_asm_goal % "proof"
    2.54 +  and "then" "from" "with" :: prf_chain % "proof"
    2.55 +  and "note" "using" "unfolding" :: prf_decl % "proof"
    2.56 +  and "fix" "assume" "presume" "def" :: prf_asm % "proof"
    2.57 +  and "obtain" "guess" :: prf_asm_goal % "proof"
    2.58 +  and "let" "write" :: prf_decl % "proof"
    2.59 +  and "case" :: prf_asm % "proof"
    2.60 +  and "{" :: prf_open % "proof"
    2.61 +  and "}" :: prf_close % "proof"
    2.62 +  and "next" :: prf_block % "proof"
    2.63 +  and "qed" :: qed_block % "proof"
    2.64 +  and "by" ".." "." "done" "sorry" :: "qed" % "proof"
    2.65 +  and "oops" :: qed_global % "proof"
    2.66 +  and "defer" "prefer" "apply" "apply_end" :: prf_script % "proof"
    2.67 +  and "proof" :: prf_block % "proof"
    2.68 +  and "also" "moreover" :: prf_decl % "proof"
    2.69 +  and "finally" "ultimately" :: prf_chain % "proof"
    2.70 +  and "back" :: prf_script % "proof"
    2.71 +  and "Isabelle.command" :: control
    2.72 +  and "pretty_setmargin" "help" "print_commands" "print_configs"
    2.73 +    "print_context" "print_theory" "print_syntax" "print_abbrevs"
    2.74 +    "print_theorems" "print_locales" "print_classes" "print_locale"
    2.75 +    "print_interps" "print_dependencies" "print_attributes"
    2.76 +    "print_simpset" "print_rules" "print_trans_rules" "print_methods"
    2.77 +    "print_antiquotations" "thy_deps" "class_deps" "thm_deps"
    2.78 +    "print_binds" "print_facts" "print_cases" "print_statement" "thm"
    2.79 +    "prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
    2.80 +    :: diag
    2.81 +  and "cd" :: control
    2.82 +  and "pwd" :: diag
    2.83 +  and "use_thy" "remove_thy" "kill_thy" :: control
    2.84 +  and "display_drafts" "print_drafts" "pr" :: diag
    2.85 +  and "disable_pr" "enable_pr" "commit" "quit" "exit" :: control
    2.86 +  and "end" :: thy_end % "theory"
    2.87 +  uses "Isar/isar_syn.ML"
    2.88  begin
    2.89  
    2.90  section {* Further content for the Pure theory *}
     3.1 --- a/src/Pure/ROOT	Wed Aug 01 22:12:29 2012 +0200
     3.2 +++ b/src/Pure/ROOT	Wed Aug 01 23:33:26 2012 +0200
     3.3 @@ -105,7 +105,6 @@
     3.4      "Isar/expression.ML"
     3.5      "Isar/generic_target.ML"
     3.6      "Isar/isar_cmd.ML"
     3.7 -    "Isar/isar_syn.ML"
     3.8      "Isar/keyword.ML"
     3.9      "Isar/local_defs.ML"
    3.10      "Isar/local_theory.ML"
     4.1 --- a/src/Pure/ROOT.ML	Wed Aug 01 22:12:29 2012 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Wed Aug 01 23:33:26 2012 +0200
     4.3 @@ -259,7 +259,6 @@
     4.4  use "Isar/rule_insts.ML";
     4.5  use "Thy/thm_deps.ML";
     4.6  use "Isar/isar_cmd.ML";
     4.7 -use "Isar/isar_syn.ML";
     4.8  
     4.9  use "subgoal.ML";
    4.10  
    4.11 @@ -302,11 +301,11 @@
    4.12  
    4.13  use "ProofGeneral/pgip_parser.ML";
    4.14  
    4.15 -use "ProofGeneral/pgip_tests.ML";
    4.16 -
    4.17  use "ProofGeneral/proof_general_pgip.ML";
    4.18  use "ProofGeneral/proof_general_emacs.ML";
    4.19  
    4.20  
    4.21  use "pure_setup.ML";
    4.22  
    4.23 +use "ProofGeneral/pgip_tests.ML";
    4.24 +
     5.1 --- a/src/Pure/pure_setup.ML	Wed Aug 01 22:12:29 2012 +0200
     5.2 +++ b/src/Pure/pure_setup.ML	Wed Aug 01 23:33:26 2012 +0200
     5.3 @@ -14,6 +14,13 @@
     5.4  
     5.5  (* the Pure theory *)
     5.6  
     5.7 +val _ =
     5.8 +  Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory context"
     5.9 +    (Thy_Header.args >> (fn header =>
    5.10 +      Toplevel.print o
    5.11 +        Toplevel.init_theory
    5.12 +          (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
    5.13 +
    5.14  Unsynchronized.setmp Multithreading.max_threads 1
    5.15    use_thy "Pure";
    5.16  Context.set_thread_data NONE;