# HG changeset patch
# User wenzelm
# Date 1459782154 -7200
# Node ID e4140efe699ecc9ae3eb15b16840393d3a290415
# Parent  1bd1d84929316e635a5db5302c5ef87cc9494f43
clarified bootstrap -- more uniform use of ML files;

diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -205,32 +205,4 @@
 val moreover = collect false;
 val ultimately = collect true;
 
-
-(* outer syntax *)
-
-val calc_args =
-  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
-
-val _ =
-  Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
-    (calc_args >> (Toplevel.proofs' o also_cmd));
-
-val _ =
-  Outer_Syntax.command @{command_keyword finally}
-    "combine calculation and current facts, exhibit result"
-    (calc_args >> (Toplevel.proofs' o finally_cmd));
-
-val _ =
-  Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
-    (Scan.succeed (Toplevel.proof' moreover));
-
-val _ =
-  Outer_Syntax.command @{command_keyword ultimately}
-    "augment calculation by current facts, exhibit result"
-    (Scan.succeed (Toplevel.proof' ultimately));
-
-val _ =
-  Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
-    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
-
 end;
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -148,6 +148,12 @@
       >> (fn (facts, fixes) =>
           #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
 
+val _ =
+  Outer_Syntax.local_theory @{command_keyword named_theorems}
+    "declare named collection of theorems"
+    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
+      fold (fn (b, descr) => snd o Named_Theorems.declare b descr));
+
 
 (* hide names *)
 
@@ -728,6 +734,34 @@
 end;
 
 
+(* calculation *)
+
+val calculation_args =
+  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse.xthms1 --| @{keyword ")"})));
+
+val _ =
+  Outer_Syntax.command @{command_keyword also} "combine calculation and current facts"
+    (calculation_args >> (Toplevel.proofs' o Calculation.also_cmd));
+
+val _ =
+  Outer_Syntax.command @{command_keyword finally}
+    "combine calculation and current facts, exhibit result"
+    (calculation_args >> (Toplevel.proofs' o Calculation.finally_cmd));
+
+val _ =
+  Outer_Syntax.command @{command_keyword moreover} "augment calculation by current facts"
+    (Scan.succeed (Toplevel.proof' Calculation.moreover));
+
+val _ =
+  Outer_Syntax.command @{command_keyword ultimately}
+    "augment calculation by current facts, exhibit result"
+    (Scan.succeed (Toplevel.proof' Calculation.ultimately));
+
+val _ =
+  Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
+    (Scan.succeed (Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
+
+
 (* proof navigation *)
 
 fun report_back () =
@@ -936,6 +970,96 @@
       Toplevel.keep (fn _ => ignore (Present.display_drafts (map Path.explode names)))));
 
 
+(* deps *)
+
+local
+  val theory_bounds =
+    Parse.position Parse.theory_xname >> single ||
+    (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
+in
+
+val _ =
+  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
+    (Scan.option theory_bounds -- Scan.option theory_bounds >>
+      (fn args => Toplevel.keep (fn st => Thy_Deps.thy_deps_cmd (Toplevel.context_of st) args)));
+
+end;
+
+local
+  val class_bounds =
+    Parse.sort >> single ||
+    (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
+in
+
+val _ =
+  Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
+    (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
+      Toplevel.keep (fn st => Class_Deps.class_deps_cmd (Toplevel.context_of st) args)));
+
+end;
+
+val _ =
+  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
+    (Parse.xthms1 >> (fn args =>
+      Toplevel.keep (fn st =>
+        Thm_Deps.thm_deps (Toplevel.theory_of st)
+          (Attrib.eval_thms (Toplevel.context_of st) args))));
+
+local
+  val thy_names =
+    Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
+in
+
+val _ =
+  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
+    (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
+        Toplevel.keep (fn st =>
+          let
+            val thy = Toplevel.theory_of st;
+            val ctxt = Toplevel.context_of st;
+            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
+            val check = Theory.check ctxt;
+          in
+            Thm_Deps.unused_thms
+              (case opt_range of
+                NONE => (Theory.parents_of thy, [thy])
+              | SOME (xs, NONE) => (map check xs, [thy])
+              | SOME (xs, SOME ys) => (map check xs, map check ys))
+            |> map pretty_thm |> Pretty.writeln_chunks
+          end)));
+
+end;
+
+
+(* find *)
+
+val _ =
+  Outer_Syntax.command @{command_keyword find_consts}
+    "find constants by name / type patterns"
+    (Find_Consts.query_parser >> (fn spec =>
+      Toplevel.keep (fn st =>
+        Pretty.writeln (Find_Consts.pretty_consts (Toplevel.context_of st) spec))));
+
+local
+  val options =
+    Scan.optional
+      (Parse.$$$ "(" |--
+        Parse.!!! (Scan.option Parse.nat --
+          Scan.optional (Parse.reserved "with_dups" >> K false) true --| Parse.$$$ ")"))
+      (NONE, true);
+in
+
+val _ =
+  Outer_Syntax.command @{command_keyword find_theorems}
+    "find theorems meeting specified criteria"
+    (options -- Find_Theorems.query_parser >> (fn ((opt_lim, rem_dups), spec) =>
+      Toplevel.keep (fn st =>
+        Pretty.writeln
+          (Find_Theorems.pretty_theorems (Find_Theorems.proof_state st) opt_lim rem_dups spec))));
+
+end;
+
+
 
 (** extraction of programs from proofs **)
 
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Pure.thy	Mon Apr 04 17:02:34 2016 +0200
@@ -93,23 +93,7 @@
   and "named_theorems" :: thy_decl
 begin
 
-ML_file "ML/ml_antiquotations.ML"
-ML_file "ML/ml_thms.ML"
-ML_file "Tools/print_operation.ML"
 ML_file "Isar/isar_syn.ML"
-ML_file "Isar/calculation.ML"
-ML_file "Tools/bibtex.ML"
-ML_file "Tools/rail.ML"
-ML_file "Tools/rule_insts.ML"
-ML_file "Tools/thm_deps.ML"
-ML_file "Tools/thy_deps.ML"
-ML_file "Tools/class_deps.ML"
-ML_file "Tools/find_theorems.ML"
-ML_file "Tools/find_consts.ML"
-ML_file "Tools/simplifier_trace.ML"
-ML_file_no_debug "Tools/debugger.ML"
-ML_file "Tools/named_theorems.ML"
-ML_file "Tools/jedit.ML"
 
 
 section \<open>Basic attributes\<close>
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/ROOT
--- a/src/Pure/ROOT	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/ROOT	Mon Apr 04 17:02:34 2016 +0200
@@ -61,6 +61,7 @@
     "Isar/attrib.ML"
     "Isar/auto_bind.ML"
     "Isar/bundle.ML"
+    "Isar/calculation.ML"
     "Isar/class.ML"
     "Isar/class_declaration.ML"
     "Isar/code.ML"
@@ -99,6 +100,7 @@
     "ML/exn_properties.ML"
     "ML/fixed_int_dummy.ML"
     "ML/ml_antiquotation.ML"
+    "ML/ml_antiquotations.ML"
     "ML/ml_compiler.ML"
     "ML/ml_compiler0.ML"
     "ML/ml_compiler1.ML"
@@ -112,13 +114,14 @@
     "ML/ml_lex.ML"
     "ML/ml_name_space.ML"
     "ML/ml_options.ML"
+    "ML/ml_pervasive.ML"
     "ML/ml_pp.ML"
-    "ML/ml_pervasive.ML"
     "ML/ml_pretty.ML"
     "ML/ml_profiling.ML"
     "ML/ml_statistics.ML"
     "ML/ml_syntax.ML"
     "ML/ml_system.ML"
+    "ML/ml_thms.ML"
     "PIDE/active.ML"
     "PIDE/command.ML"
     "PIDE/command_span.ML"
@@ -172,9 +175,22 @@
     "Thy/thy_info.ML"
     "Thy/thy_output.ML"
     "Thy/thy_syntax.ML"
+    "Tools/bibtex.ML"
     "Tools/build.ML"
+    "Tools/class_deps.ML"
+    "Tools/debugger.ML"
+    "Tools/find_consts.ML"
+    "Tools/find_theorems.ML"
+    "Tools/jedit.ML"
+    "Tools/named_theorems.ML"
     "Tools/named_thms.ML"
     "Tools/plugin.ML"
+    "Tools/print_operation.ML"
+    "Tools/rail.ML"
+    "Tools/rule_insts.ML"
+    "Tools/simplifier_trace.ML"
+    "Tools/thm_deps.ML"
+    "Tools/thy_deps.ML"
     "assumption.ML"
     "axclass.ML"
     "config.ML"
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/ROOT.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -241,6 +241,7 @@
 use "Isar/element.ML";
 use "Isar/obtain.ML";
 use "Isar/subgoal.ML";
+use "Isar/calculation.ML";
 
 (*local theories and targets*)
 use "Isar/locale.ML";
@@ -321,6 +322,23 @@
 use "Tools/named_thms.ML";
 use "ML/ml_pp.ML";
 use "ML/ml_file.ML";
+use "ML/ml_antiquotations.ML";
+use "ML/ml_thms.ML";
+use "Tools/print_operation.ML";
+
+use "Tools/bibtex.ML";
+use "Tools/rail.ML";
+use "Tools/rule_insts.ML";
+use "Tools/thm_deps.ML";
+use "Tools/thy_deps.ML";
+use "Tools/class_deps.ML";
+use "Tools/find_theorems.ML";
+use "Tools/find_consts.ML";
+use "Tools/simplifier_trace.ML";
+use_no_debug "Tools/debugger.ML";
+use "Tools/named_theorems.ML";
+use "Tools/jedit.ML";
+
 use_thy "Pure";
 
 
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Tools/class_deps.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -37,13 +37,4 @@
 val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of);
 val class_deps_cmd = Graph_Display.display_graph oo gen_class_deps Syntax.read_sort;
 
-val class_bounds =
-  Parse.sort >> single ||
-  (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
-
-val _ =
-  Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
-    (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
-      Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args)));
-
 end;
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Tools/find_consts.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -11,6 +11,8 @@
       Strict of string
     | Loose of string
     | Name of string
+  val pretty_consts: Proof.context -> (bool * criterion) list -> Pretty.T
+  val query_parser: (bool * criterion) list parser
   val read_query: Position.T -> string -> (bool * criterion) list
   val find_consts : Proof.context -> (bool * criterion) list -> unit
 end;
@@ -138,25 +140,18 @@
   Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.typ) >> Strict ||
   Parse.typ >> Loose;
 
-val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
-
 val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
 
 in
 
+val query_parser = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
+
 fun read_query pos str =
   Token.explode query_keywords pos str
   |> filter Token.is_proper
-  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
+  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query_parser --| Scan.ahead Parse.eof)))
   |> #1;
 
-val _ =
-  Outer_Syntax.command @{command_keyword find_consts}
-    "find constants by name / type patterns"
-    (query >> (fn spec =>
-      Toplevel.keep (fn st =>
-        Pretty.writeln (pretty_consts (Toplevel.context_of st) spec))));
-
 end;
 
 
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -15,12 +15,16 @@
     rem_dups: bool,
     criteria: (bool * 'term criterion) list
   }
+  val query_parser: (bool * string criterion) list parser
   val read_query: Position.T -> string -> (bool * string criterion) list
   val find_theorems: Proof.context -> thm option -> int option -> bool ->
     (bool * term criterion) list -> int option * (Facts.ref * thm) list
   val find_theorems_cmd: Proof.context -> thm option -> int option -> bool ->
     (bool * string criterion) list -> int option * (Facts.ref * thm) list
   val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
+  val pretty_theorems: Proof.state ->
+    int option -> bool -> (bool * string criterion) list -> Pretty.T
+  val proof_state: Toplevel.state -> Proof.state
 end;
 
 structure Find_Theorems: FIND_THEOREMS =
@@ -502,11 +506,6 @@
 
 (** Isar command syntax **)
 
-fun proof_state st =
-  (case try Toplevel.proof_of st of
-    SOME state => state
-  | NONE => Proof.init (Toplevel.context_of st));
-
 local
 
 val criterion =
@@ -518,37 +517,29 @@
   Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
   Parse.term >> Pattern;
 
-val options =
-  Scan.optional
-    (Parse.$$$ "(" |--
-      Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
-        --| Parse.$$$ ")")) (NONE, true);
-
-val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
-
 val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
 
 in
 
+val query_parser = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
+
 fun read_query pos str =
   Token.explode query_keywords pos str
   |> filter Token.is_proper
-  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
+  |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query_parser --| Scan.ahead Parse.eof)))
   |> #1;
 
-val _ =
-  Outer_Syntax.command @{command_keyword find_theorems}
-    "find theorems meeting specified criteria"
-    (options -- query >> (fn ((opt_lim, rem_dups), spec) =>
-      Toplevel.keep (fn st =>
-        Pretty.writeln (pretty_theorems (proof_state st) opt_lim rem_dups spec))));
-
 end;
 
 
 
 (** PIDE query operation **)
 
+fun proof_state st =
+  (case try Toplevel.proof_of st of
+    SOME state => state
+  | NONE => Proof.init (Toplevel.context_of st));
+
 val _ =
   Query_Operation.register {name = "find_theorems", pri = Task_Queue.urgent_pri}
     (fn {state = st, args, writeln_result, ...} =>
@@ -563,4 +554,3 @@
       else error "Unknown context");
 
 end;
-
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -93,12 +93,6 @@
       |> Attrib.local_setup binding (Attrib.add_del (add name) (del name)) description
   in (name, lthy') end;
 
-val _ =
-  Outer_Syntax.local_theory @{command_keyword named_theorems}
-    "declare named collection of theorems"
-    (Parse.and_list1 (Parse.binding -- Scan.optional Parse.text "") >>
-      fold (fn (b, descr) => snd o declare b descr));
-
 
 (* ML antiquotation *)
 
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -47,12 +47,6 @@
     |> Graph_Display.display_graph_old
   end;
 
-val _ =
-  Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
-    (Parse.xthms1 >> (fn args =>
-      Toplevel.keep (fn st =>
-        thm_deps (Toplevel.theory_of st) (Attrib.eval_thms (Toplevel.context_of st) args))));
-
 
 (* unused_thms *)
 
@@ -107,25 +101,4 @@
       else q) new_thms ([], Inttab.empty);
   in rev thms' end;
 
-val thy_names =
-  Scan.repeat1 (Scan.unless Parse.minus (Parse.position Parse.theory_xname));
-
-val _ =
-  Outer_Syntax.command @{command_keyword unused_thms} "find unused theorems"
-    (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
-        Toplevel.keep (fn st =>
-          let
-            val thy = Toplevel.theory_of st;
-            val ctxt = Toplevel.context_of st;
-            fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]);
-            val check = Theory.check ctxt;
-          in
-            unused_thms
-              (case opt_range of
-                NONE => (Theory.parents_of thy, [thy])
-              | SOME (xs, NONE) => (map check xs, [thy])
-              | SOME (xs, SOME ys) => (map check xs, map check ys))
-            |> map pretty_thm |> Pretty.writeln_chunks
-          end)));
-
 end;
diff -r 1bd1d8492931 -r e4140efe699e src/Pure/Tools/thy_deps.ML
--- a/src/Pure/Tools/thy_deps.ML	Mon Apr 04 16:14:22 2016 +0200
+++ b/src/Pure/Tools/thy_deps.ML	Mon Apr 04 17:02:34 2016 +0200
@@ -42,13 +42,4 @@
 
 val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Theory.check;
 
-val theory_bounds =
-  Parse.position Parse.theory_xname >> single ||
-  (@{keyword "("} |-- Parse.enum "|" (Parse.position Parse.theory_xname) --| @{keyword ")"});
-
-val _ =
-  Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
-    (Scan.option theory_bounds -- Scan.option theory_bounds >>
-      (fn args => Toplevel.keep (fn st => thy_deps_cmd (Toplevel.context_of st) args)));
-
 end;