--- 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;
--- 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 **)
--- 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>
--- 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"
--- 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";
--- 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;
--- 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;
--- 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;
-
--- 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 *)
--- 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;
--- 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;