--- a/NEWS Thu Apr 16 17:52:12 2015 +0200
+++ b/NEWS Fri Apr 17 09:56:12 2015 +0200
@@ -74,10 +74,11 @@
* Less waste of vertical space via negative line spacing (see Global
Options / Text Area).
-* Improved graphview panel (with optional output of PNG or PDF)
-supersedes the old graph browser from 1996, but the latter remains
-available for some time as a fall-back. The old browser is still
-required for the massive graphs produced by 'thm_deps', for example.
+* Improved graphview panel with optional output of PNG or PDF, for
+display of 'thy_deps', 'locale_deps', 'class_deps' etc.
+
+* Command 'thy_deps' allows optional bounds, analogously to
+'class_deps'.
* Improved scheduling for asynchronous print commands (e.g. provers
managed by the Sledgehammer panel) wrt. ongoing document processing.
@@ -397,6 +398,9 @@
derivatives) instead, which is not affected by the change. Potential
INCOMPATIBILITY in rare applications of Name_Space.intern.
+* Subtle change of error semantics of Toplevel.proof_of: regular user
+ERROR instead of internal Toplevel.UNDEF.
+
* Basic combinators map, fold, fold_map, split_list, apply are available
as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
--- a/src/Doc/Implementation/Integration.thy Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Doc/Implementation/Integration.thy Fri Apr 17 09:56:12 2015 +0200
@@ -62,7 +62,7 @@
for an empty toplevel state.
\item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
- state if available, otherwise it raises @{ML Toplevel.UNDEF}.
+ state if available, otherwise it raises an error.
\end{description}
\<close>
--- a/src/Doc/Isar_Ref/Spec.thy Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Apr 17 09:56:12 2015 +0200
@@ -25,6 +25,7 @@
\begin{matharray}{rcl}
@{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
@{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
+ @{command_def "thy_deps"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow>"} \\
\end{matharray}
Isabelle/Isar theories are defined via theory files, which consist of an
@@ -64,6 +65,10 @@
;
keyword_decls: (@{syntax string} +)
('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
+ ;
+ @@{command thy_deps} (thy_bounds thy_bounds?)?
+ ;
+ thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')'
\<close>}
\begin{description}
@@ -104,6 +109,12 @@
@{keyword "begin"} that needs to be matched by @{command (local)
"end"}, according to the usual rules for nested blocks.
+ \item @{command thy_deps} visualizes the theory hierarchy as a directed
+ acyclic graph. By default, all imported theories are shown, taking the
+ base session as a starting point. Alternatively, it is possibly to
+ restrict the full theory graph by giving bounds, analogously to
+ @{command_ref class_deps}.
+
\end{description}
\<close>
@@ -948,8 +959,9 @@
;
@@{command subclass} @{syntax nameref}
;
- @@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline>
- ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )?
+ @@{command class_deps} (class_bounds class_bounds?)?
+ ;
+ class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
\<close>}
\begin{description}
@@ -1012,11 +1024,13 @@
\item @{command "print_classes"} prints all classes in the current
theory.
- \item @{command "class_deps"} visualizes all classes and their
- subclass relations as a Hasse diagram. An optional first argument
- constrains the set of classes to all subclasses of at least one given
- sort, an optional second rgument to all superclasses of at least one given
- sort.
+ \item @{command "class_deps"} visualizes classes and their subclass
+ relations as a directed acyclic graph. By default, all classes from the
+ current theory context are show. This may be restricted by optional bounds
+ as follows: @{command "class_deps"}~@{text upper} or @{command
+ "class_deps"}~@{text "upper lower"}. A class is visualized, iff it is a
+ subclass of some sort from @{text upper} and a superclass of some sort
+ from @{text lower}.
\item @{method intro_classes} repeatedly expands all class
introduction rules of this theory. Note that this method usually
--- a/src/HOL/Library/refute.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/HOL/Library/refute.ML Fri Apr 17 09:56:12 2015 +0200
@@ -2969,7 +2969,6 @@
"try to find a model that refutes a given subgoal"
(scan_parms -- Scan.optional Parse.nat 1 >>
(fn (parms, i) =>
- Toplevel.unknown_proof o
Toplevel.keep (fn state =>
let
val ctxt = Toplevel.context_of state;
--- a/src/HOL/Library/rewrite.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/HOL/Library/rewrite.ML Fri Apr 17 09:56:12 2015 +0200
@@ -130,8 +130,8 @@
in
-val ft_arg = ft_arg_gen arg_rewr_cconv
-val ft_imp = ft_arg_gen imp_rewr_cconv
+fun ft_arg ctxt = ft_arg_gen arg_rewr_cconv ctxt
+fun ft_imp ctxt = ft_arg_gen imp_rewr_cconv ctxt
end
--- a/src/HOL/Orderings.thy Thu Apr 16 17:52:12 2015 +0200
+++ b/src/HOL/Orderings.thy Fri Apr 17 09:56:12 2015 +0200
@@ -441,8 +441,7 @@
val _ =
Outer_Syntax.command @{command_keyword print_orders}
"print order structures available to transitivity reasoner"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (print_structures o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (print_structures o Toplevel.context_of)));
(* tactics *)
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Fri Apr 17 09:56:12 2015 +0200
@@ -377,7 +377,6 @@
Outer_Syntax.command @{command_keyword nitpick}
"try to find a counterexample for a given subgoal using Nitpick"
(parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
- Toplevel.unknown_proof o
Toplevel.keep (fn state =>
ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
(Toplevel.proof_of state)))))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Apr 17 09:56:12 2015 +0200
@@ -359,7 +359,6 @@
end
fun sledgehammer_trans (((subcommand, params), fact_override), opt_i) =
- Toplevel.unknown_proof o
Toplevel.keep (hammer_away params subcommand opt_i fact_override o Toplevel.proof_of)
fun string_of_raw_param (key, values) =
--- a/src/HOL/Tools/inductive.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Fri Apr 17 09:56:12 2015 +0200
@@ -1190,7 +1190,6 @@
val _ =
Outer_Syntax.command @{command_keyword print_inductives}
"print (co)inductive definitions and monotonicity rules"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
- Toplevel.keep (print_inductives b o Toplevel.context_of)));
+ (Parse.opt_bang >> (fn b => Toplevel.keep (print_inductives b o Toplevel.context_of)));
end;
--- a/src/HOL/Tools/try0.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/HOL/Tools/try0.ML Fri Apr 17 09:56:12 2015 +0200
@@ -154,7 +154,6 @@
fun try0 timeout_opt = fst oo generic_try0 Normal timeout_opt;
fun try0_trans quad =
- Toplevel.unknown_proof o
Toplevel.keep (K () o generic_try0 Normal (SOME default_timeout) quad o Toplevel.proof_of);
fun merge_attrs (s1, i1, e1, d1) (s2, i2, e2, d2) = (s1 @ s2, i1 @ i2, e1 @ e2, d1 @ d2);
--- a/src/Provers/classical.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Provers/classical.ML Fri Apr 17 09:56:12 2015 +0200
@@ -980,6 +980,6 @@
val _ =
Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner"
- (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (print_claset o Toplevel.context_of)));
end;
--- a/src/Pure/General/graph_display.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/General/graph_display.ML Fri Apr 17 09:56:12 2015 +0200
@@ -11,6 +11,7 @@
val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
type entry = (string * node) * string list
val display_graph: entry list -> unit
+ val display_graph_old: entry list -> unit
end;
structure Graph_Display: GRAPH_DISPLAY =
@@ -30,7 +31,9 @@
type entry = (string * node) * string list;
-(* encode graph *)
+(* display graph *)
+
+local
fun encode_node (Node {name, content, ...}) =
(name, content) |>
@@ -40,9 +43,22 @@
val encode_graph =
let open XML.Encode in list (pair (pair string encode_node) (list string)) end;
+in
+
+fun display_graph entries =
+ let
+ val ((bg1, bg2), en) =
+ YXML.output_markup_elem
+ (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
+ in writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en) end;
+
+end;
+
(* support for old browser *)
+local
+
structure Graph =
Graph(type key = string * string val ord = prod_ord string_ord string_ord);
@@ -71,23 +87,15 @@
path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
#> cat_lines;
+in
-(* display graph *)
-
-fun display_graph entries =
+fun display_graph_old entries =
let
val ((bg1, bg2), en) =
YXML.output_markup_elem
- (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
- val _ =
- writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en);
-
- (*old browser*)
- val ((bg1, bg2), en) =
- YXML.output_markup_elem
(Active.make_markup Markup.browserN {implicit = false, properties = []});
- val _ =
- writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "old graph" ^ en);
- in () end;
+ in writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "graph" ^ en) end;
end;
+
+end;
--- a/src/Pure/Isar/calculation.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Isar/calculation.ML Fri Apr 17 09:56:12 2015 +0200
@@ -230,6 +230,6 @@
val _ =
Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
- (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
end;
--- a/src/Pure/Isar/isar_cmd.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Apr 17 09:56:12 2015 +0200
@@ -35,8 +35,6 @@
val diag_state: Proof.context -> Toplevel.state
val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm}
val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
- val thy_deps: Toplevel.transition -> Toplevel.transition
- val locale_deps: Toplevel.transition -> Toplevel.transition
val print_stmts: string list * (Facts.ref * Token.src list) list
-> Toplevel.transition -> Toplevel.transition
val print_thms: string list * (Facts.ref * Token.src list) list
@@ -241,10 +239,7 @@
in ML_Context.eval_source_in opt_ctxt flags source end);
val diag_state = Diag_State.get;
-
-fun diag_goal ctxt =
- Proof.goal (Toplevel.proof_of (diag_state ctxt))
- handle Toplevel.UNDEF => error "No goal present";
+val diag_goal = Proof.goal o Toplevel.proof_of o diag_state;
val _ = Theory.setup
(ML_Antiquotation.value (Binding.qualify true "Isar" @{binding state})
@@ -268,26 +263,6 @@
in Proof_Display.pretty_theorems_diff verbose prev_thys thy end;
-(* display dependencies *)
-
-val thy_deps =
- Toplevel.unknown_theory o
- Toplevel.keep (fn st =>
- let
- val thy = Toplevel.theory_of st;
- val parent_session = Session.get_name ();
- val parent_loaded = is_some o Thy_Info.lookup_theory;
- in Graph_Display.display_graph (Present.session_graph parent_session parent_loaded thy) end);
-
-val locale_deps =
- Toplevel.unknown_theory o
- Toplevel.keep (Toplevel.theory_of #> (fn thy =>
- Locale.pretty_locale_deps thy
- |> map (fn {name, parents, body} =>
- ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
- |> Graph_Display.display_graph));
-
-
(* print theorems, terms, types etc. *)
local
--- a/src/Pure/Isar/isar_syn.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Apr 17 09:56:12 2015 +0200
@@ -350,8 +350,7 @@
val _ =
Outer_Syntax.command @{command_keyword print_bundles}
"print bundles of declarations"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
- Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
+ (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
(* local theories *)
@@ -693,8 +692,7 @@
val _ =
Outer_Syntax.command @{command_keyword print_options} "print configuration options"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
- Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
+ (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_context}
@@ -704,125 +702,116 @@
val _ =
Outer_Syntax.command @{command_keyword print_theory}
"print logical theory contents"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+ (Parse.opt_bang >> (fn b =>
Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
val _ =
Outer_Syntax.command @{command_keyword print_syntax}
"print inner syntax of context"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_defn_rules}
"print definitional rewrite rules of context"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_abbrevs}
"print constant abbreviations of context"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+ (Parse.opt_bang >> (fn b =>
Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_theorems}
"print theorems of local theory or proof context"
(Parse.opt_bang >> (fn b =>
- Toplevel.unknown_context o
Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
val _ =
Outer_Syntax.command @{command_keyword print_locales}
"print locales of this theory"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+ (Parse.opt_bang >> (fn b =>
Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
val _ =
Outer_Syntax.command @{command_keyword print_classes}
"print classes of this theory"
- (Scan.succeed (Toplevel.unknown_theory o
- Toplevel.keep (Class.print_classes o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_locale}
"print locale of this theory"
(Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
- Toplevel.unknown_theory o
Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
val _ =
Outer_Syntax.command @{command_keyword print_interps}
"print interpretations of locale for this theory or proof context"
(Parse.position Parse.xname >> (fn name =>
- Toplevel.unknown_context o
Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
val _ =
Outer_Syntax.command @{command_keyword print_dependencies}
"print dependencies of locale expression"
(Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
- Toplevel.unknown_context o
Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
val _ =
Outer_Syntax.command @{command_keyword print_attributes}
"print attributes of this theory"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
- Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
+ (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_simpset}
"print context of Simplifier"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+ (Parse.opt_bang >> (fn b =>
Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
- Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
+ (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_antiquotations}
"print document antiquotations"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+ (Parse.opt_bang >> (fn b =>
Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_ML_antiquotations}
"print ML antiquotations"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+ (Parse.opt_bang >> (fn b =>
Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
val _ =
- Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
- (Scan.succeed Isar_Cmd.thy_deps);
-
-val _ =
Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies"
- (Scan.succeed Isar_Cmd.locale_deps);
+ (Scan.succeed
+ (Toplevel.keep (Toplevel.theory_of #> (fn thy =>
+ Locale.pretty_locale_deps thy
+ |> map (fn {name, parents, body} =>
+ ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
+ |> Graph_Display.display_graph))));
val _ =
Outer_Syntax.command @{command_keyword print_term_bindings}
"print term bindings of proof context"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep
+ (Scan.succeed
+ (Toplevel.keep
(Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
- (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+ (Parse.opt_bang >> (fn b =>
Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
+ (Scan.succeed
+ (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword print_statement}
@@ -856,8 +845,7 @@
val _ =
Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
- (Scan.succeed (Toplevel.unknown_theory o
- Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
+ (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
val _ =
Outer_Syntax.command @{command_keyword print_state}
--- a/src/Pure/Isar/outer_syntax.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Fri Apr 17 09:56:12 2015 +0200
@@ -19,6 +19,7 @@
(bool -> local_theory -> Proof.state) parser -> unit
val local_theory_to_proof: command_keyword -> string ->
(local_theory -> Proof.state) parser -> unit
+ val bootstrap: bool Config.T
val parse: theory -> Position.T -> string -> Toplevel.transition list
val parse_tokens: theory -> Token.T list -> Toplevel.transition list
val parse_spans: Token.T list -> Command_Span.span list
@@ -160,6 +161,9 @@
(* parse commands *)
+val bootstrap =
+ Config.bool (Config.declare ("Outer_Syntax.bootstrap", @{here}) (K (Config.Bool true)));
+
local
val before_command =
@@ -177,7 +181,14 @@
| SOME (Command {command_parser = Limited_Parser parse, ...}) =>
before_command :|-- (fn limited =>
Parse.!!! (command_tags |-- parse limited)) >> (fn f => f tr0)
- | NONE => Scan.fail_with (fn _ => fn _ => err_command "Undefined command " name [pos]))
+ | NONE =>
+ Scan.fail_with (fn _ => fn _ =>
+ let
+ val msg =
+ if Config.get_global thy bootstrap
+ then "missing theory context for command "
+ else "undefined command ";
+ in msg ^ quote (Markup.markup Markup.keyword1 name) end))
end);
val parse_cmt = Parse.$$$ "--" -- Parse.!!! Parse.document_source;
--- a/src/Pure/Isar/proof.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Isar/proof.ML Fri Apr 17 09:56:12 2015 +0200
@@ -338,7 +338,7 @@
fun find i state =
(case try current_goal state of
SOME (ctxt, goal) => (ctxt, (i, goal))
- | NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present"));
+ | NONE => find (i + 1) (close_block state handle ERROR _ => error "No proof goal"));
in val find_goal = find 0 end;
fun get_goal state =
--- a/src/Pure/Isar/toplevel.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri Apr 17 09:56:12 2015 +0200
@@ -72,9 +72,6 @@
val skip_proof: (int -> int) -> transition -> transition
val skip_proof_to_theory: (int -> bool) -> transition -> transition
val exec_id: Document_ID.exec -> transition -> transition
- val unknown_theory: transition -> transition
- val unknown_proof: transition -> transition
- val unknown_context: transition -> transition
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
val add_hook: (transition -> state -> state -> unit) -> unit
val get_timing: transition -> Time.time option
@@ -164,12 +161,12 @@
val context_of = node_case Context.proof_of Proof.context_of;
val generic_theory_of = node_case I (Context.Proof o Proof.context_of);
val theory_of = node_case Context.theory_of Proof.theory_of;
-val proof_of = node_case (fn _ => raise UNDEF) I;
+val proof_of = node_case (fn _ => error "No proof state") I;
fun proof_position_of state =
(case node_of state of
Proof (prf, _) => Proof_Node.position prf
- | _ => raise UNDEF);
+ | _ => ~1);
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
| end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
@@ -356,10 +353,6 @@
fun malformed pos msg =
empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
-val unknown_theory = imperative (fn () => warning "Unknown theory context");
-val unknown_proof = imperative (fn () => warning "Unknown proof context");
-val unknown_context = imperative (fn () => warning "Unknown context");
-
(* theory transitions *)
--- a/src/Pure/ML/ml_antiquotations.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Fri Apr 17 09:56:12 2015 +0200
@@ -53,15 +53,13 @@
ML_Antiquotation.value @{binding theory}
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
- (Context_Position.report ctxt pos
- (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+ (Theory.check ctxt (name, pos);
"Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
ML_Antiquotation.value @{binding theory_context}
(Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
- (Context_Position.report ctxt pos
- (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+ (Theory.check ctxt (name, pos);
"Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))) #>
--- a/src/Pure/PIDE/command.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/PIDE/command.ML Fri Apr 17 09:56:12 2015 +0200
@@ -109,11 +109,10 @@
| NONE => toks)
| _ => toks);
-val bootstrap_thy = ML_Context.the_global_context ();
-
in
-fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
+fun read_thy st = Toplevel.theory_of st
+ handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy;
fun read keywords thy master_dir init blobs_info span =
let
--- a/src/Pure/Pure.thy Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Pure.thy Fri Apr 17 09:56:12 2015 +0200
@@ -98,6 +98,7 @@
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"
--- a/src/Pure/Thy/thy_output.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Apr 17 09:56:12 2015 +0200
@@ -540,11 +540,7 @@
fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
-fun pretty_theory ctxt (name, pos) =
- (case find_first (fn thy => Context.theory_name thy = name)
- (Theory.nodes_of (Proof_Context.theory_of ctxt)) of
- NONE => error ("No ancestor theory " ^ quote name ^ Position.here pos)
- | SOME thy => (Context_Position.report ctxt pos (Theory.get_markup thy); Pretty.str name));
+fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
(* default output *)
@@ -614,16 +610,12 @@
local
-fun proof_state state =
- (case try (Proof.goal o Toplevel.proof_of) state of
- SOME {goal, ...} => goal
- | _ => error "No proof state");
-
fun goal_state name main = antiquotation name (Scan.succeed ())
(fn {state, context = ctxt, ...} => fn () =>
output ctxt
[Goal_Display.pretty_goal
- (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
+ (Config.put Goal_Display.show_main_goal main ctxt)
+ (#goal (Proof.goal (Toplevel.proof_of state)))]);
in
--- a/src/Pure/Tools/class_deps.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML Fri Apr 17 09:56:12 2015 +0200
@@ -6,49 +6,44 @@
signature CLASS_DEPS =
sig
- val class_deps: Proof.context -> sort list option -> sort list option -> unit
- val class_deps_cmd: Proof.context -> string list option -> string list option -> unit
+ val class_deps: Proof.context -> sort list option * sort list option -> Graph_Display.entry list
+ val class_deps_cmd: Proof.context -> string list option * string list option -> unit
end;
structure Class_Deps: CLASS_DEPS =
struct
-fun gen_class_deps prep_sort ctxt raw_subs raw_supers =
+fun gen_class_deps prep_sort ctxt bounds =
let
- val thy = Proof_Context.theory_of ctxt;
- val some_subs = (Option.map o map) (prep_sort ctxt) raw_subs;
- val some_supers = (Option.map o map) (prep_sort ctxt) raw_supers;
- val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
- val sort_le = curry (Sorts.sort_le original_algebra);
- val le_sub = case some_subs of
- SOME subs => (fn class => exists (sort_le [class]) subs)
- | NONE => K true;
- val super_le = case some_supers of
- SOME supers => (fn class => exists (fn super => sort_le super [class]) supers)
- | NONE => K true
- val (_, algebra) =
- Sorts.subalgebra (Context.pretty ctxt)
- (le_sub andf super_le) (K NONE) original_algebra;
+ val (upper, lower) = apply2 ((Option.map o map) (prep_sort ctxt)) bounds;
+ val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
+ val rel = Sorts.sort_le algebra;
+ val pred =
+ (case upper of
+ SOME bs => (fn c => exists (fn b => rel ([c], b)) bs)
+ | NONE => K true) andf
+ (case lower of
+ SOME bs => (fn c => exists (fn b => rel (b, [c])) bs)
+ | NONE => K true);
fun node c =
Graph_Display.content_node (Name_Space.extern ctxt space c)
- (Class.pretty_specification thy c);
+ (Class.pretty_specification (Proof_Context.theory_of ctxt) c);
in
- Sorts.classes_of algebra
- |> Graph.dest
+ Sorts.subalgebra (Context.pretty ctxt) pred (K NONE) algebra
+ |> #2 |> Sorts.classes_of |> Graph.dest
|> map (fn ((c, _), ds) => ((c, node c), ds))
- |> Graph_Display.display_graph
end;
val class_deps = gen_class_deps (Type.cert_sort o Proof_Context.tsig_of);
-val class_deps_cmd = gen_class_deps Syntax.read_sort;
+val class_deps_cmd = Graph_Display.display_graph oo gen_class_deps Syntax.read_sort;
-val parse_sort_list = (Parse.sort >> single)
- || (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
+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 parse_sort_list -- Scan.option parse_sort_list) >> (fn (super, sub) =>
- (Toplevel.unknown_theory o
- Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
+ (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/thm_deps.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML Fri Apr 17 09:56:12 2015 +0200
@@ -44,14 +44,14 @@
else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
in
Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
- |> Graph_Display.display_graph
+ |> Graph_Display.display_graph_old
end;
val _ =
Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
(Parse.xthms1 >> (fn args =>
- Toplevel.unknown_theory o Toplevel.keep (fn state =>
- thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
+ Toplevel.keep (fn st =>
+ thm_deps (Toplevel.theory_of st) (Attrib.eval_thms (Toplevel.context_of st) args))));
(* unused_thms *)
@@ -104,22 +104,24 @@
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 ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
- Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> (fn opt_range =>
- Toplevel.keep (fn state =>
+ (Scan.option ((thy_names --| Parse.minus) -- Scan.option thy_names) >> (fn opt_range =>
+ Toplevel.keep (fn st =>
let
- val thy = Toplevel.theory_of state;
- val ctxt = Toplevel.context_of state;
+ 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 get_theory = Context.get_theory thy;
+ val check = Theory.check ctxt;
in
unused_thms
(case opt_range of
NONE => (Theory.parents_of thy, [thy])
- | SOME (xs, NONE) => (map get_theory xs, [thy])
- | SOME (xs, SOME ys) => (map get_theory xs, map get_theory ys))
+ | SOME (xs, NONE) => (map check xs, [thy])
+ | SOME (xs, SOME ys) => (map check xs, map check ys))
|> map pretty_thm |> Pretty.writeln_chunks
end)));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/thy_deps.ML Fri Apr 17 09:56:12 2015 +0200
@@ -0,0 +1,54 @@
+(* Title: Pure/Tools/thy_deps.ML
+ Author: Makarius
+
+Visualization of theory dependencies.
+*)
+
+signature THY_DEPS =
+sig
+ val thy_deps: Proof.context -> theory list option * theory list option -> Graph_Display.entry list
+ val thy_deps_cmd: Proof.context ->
+ (string * Position.T) list option * (string * Position.T) list option -> unit
+end;
+
+structure Thy_Deps: THY_DEPS =
+struct
+
+fun gen_thy_deps _ ctxt (NONE, NONE) =
+ let
+ val parent_session = Session.get_name ();
+ val parent_loaded = is_some o Thy_Info.lookup_theory;
+ in Present.session_graph parent_session parent_loaded (Proof_Context.theory_of ctxt) end
+ | gen_thy_deps prep_thy ctxt bounds =
+ let
+ val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
+ val rel = Theory.subthy o swap;
+ val pred =
+ (case upper of
+ SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
+ | NONE => K true) andf
+ (case lower of
+ SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
+ | NONE => K true);
+ fun node thy =
+ ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
+ map Context.theory_name (filter pred (Theory.parents_of thy)));
+ in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
+
+val thy_deps =
+ gen_thy_deps (fn ctxt => fn thy =>
+ let val thy0 = Proof_Context.theory_of ctxt
+ in if Theory.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
+
+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;
--- a/src/Pure/pure_syn.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/pure_syn.ML Fri Apr 17 09:56:12 2015 +0200
@@ -1,10 +1,16 @@
(* Title: Pure/pure_syn.ML
Author: Makarius
-Outer syntax for bootstrapping Isabelle/Pure.
+Outer syntax for bootstrapping: commands that are accessible outside a
+regular theory context.
*)
-structure Pure_Syn: sig end =
+signature PURE_SYN =
+sig
+ val bootstrap_thy: theory
+end;
+
+structure Pure_Syn: PURE_SYN =
struct
val _ =
@@ -44,5 +50,9 @@
(Thy_Header.args >>
(fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
+
+val bootstrap_thy = ML_Context.the_global_context ();
+
+val _ = Theory.setup (Config.put_global Outer_Syntax.bootstrap false);
+
end;
-
--- a/src/Pure/theory.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Pure/theory.ML Fri Apr 17 09:56:12 2015 +0200
@@ -16,6 +16,7 @@
val setup: (theory -> theory) -> unit
val local_setup: (Proof.context -> Proof.context) -> unit
val get_markup: theory -> Markup.T
+ val check: Proof.context -> string * Position.T -> theory
val axiom_table: theory -> term Name_Space.table
val axiom_space: theory -> Name_Space.T
val axioms_of: theory -> (string * term) list
@@ -128,6 +129,25 @@
let val {pos, id, ...} = rep_theory thy
in theory_markup false (Context.theory_name thy) id pos end;
+fun check ctxt (name, pos) =
+ let
+ val thy = Proof_Context.theory_of ctxt;
+ val thy' =
+ Context.get_theory thy name
+ handle ERROR msg =>
+ let
+ val completion =
+ Completion.make (name, pos)
+ (fn completed =>
+ map Context.theory_name (ancestors_of thy)
+ |> filter completed
+ |> sort_strings
+ |> map (fn a => (a, (Markup.theoryN, a))));
+ val report = Markup.markup_report (Completion.reported_text completion);
+ in error (msg ^ Position.here pos ^ report) end;
+ val _ = Context_Position.report ctxt pos (get_markup thy');
+ in thy' end;
+
(* basic operations *)
--- a/src/Tools/Code/code_preproc.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Apr 17 09:56:12 2015 +0200
@@ -589,6 +589,6 @@
val _ =
Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup"
- (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (print_codeproc o Toplevel.context_of)));
end; (*struct*)
--- a/src/Tools/Code/code_thingol.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML Fri Apr 17 09:56:12 2015 +0200
@@ -946,7 +946,7 @@
|> join_strong_conn
|> Graph.dest
|> map (fn ((c, cs), ds) => ((c, Graph_Display.content_node (namify cs) []), ds))
- |> Graph_Display.display_graph
+ |> Graph_Display.display_graph_old
end;
local
@@ -960,14 +960,12 @@
Outer_Syntax.command @{command_keyword code_thms}
"print system of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
- Toplevel.unknown_context o
- Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
+ Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs)));
val _ =
Outer_Syntax.command @{command_keyword code_deps}
"visualize dependencies of code equations for code"
(Scan.repeat1 Parse.term >> (fn cs =>
- Toplevel.unknown_context o
Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs)));
end;
--- a/src/Tools/induct.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Tools/induct.ML Fri Apr 17 09:56:12 2015 +0200
@@ -257,8 +257,7 @@
val _ =
Outer_Syntax.command @{command_keyword print_induct_rules}
"print induction and cases rules"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (print_rules o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
(* access rules *)
--- a/src/Tools/quickcheck.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Tools/quickcheck.ML Fri Apr 17 09:56:12 2015 +0200
@@ -533,8 +533,8 @@
val _ =
Outer_Syntax.command @{command_keyword quickcheck}
"try to find counterexample for subgoal"
- (parse_args -- Scan.optional Parse.nat 1 >> (fn (args, i) =>
- Toplevel.unknown_proof o Toplevel.keep (quickcheck_cmd args i)));
+ (parse_args -- Scan.optional Parse.nat 1 >>
+ (fn (args, i) => Toplevel.keep (quickcheck_cmd args i)));
(* automatic testing *)
--- a/src/Tools/solve_direct.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Tools/solve_direct.ML Fri Apr 17 09:56:12 2015 +0200
@@ -94,8 +94,7 @@
val _ =
Outer_Syntax.command @{command_keyword solve_direct}
"try to solve conjectures directly with existing theorems"
- (Scan.succeed (Toplevel.unknown_proof o
- Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+ (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
(* hook *)
--- a/src/Tools/try.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/Tools/try.ML Fri Apr 17 09:56:12 2015 +0200
@@ -77,7 +77,7 @@
val _ =
Outer_Syntax.command @{command_keyword try}
"try a combination of automatic proving and disproving tools"
- (Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
+ (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
(* automatic try (TTY) *)
--- a/src/ZF/Tools/typechk.ML Thu Apr 16 17:52:12 2015 +0200
+++ b/src/ZF/Tools/typechk.ML Fri Apr 17 09:56:12 2015 +0200
@@ -127,7 +127,6 @@
val _ =
Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"
- (Scan.succeed (Toplevel.unknown_context o
- Toplevel.keep (print_tcset o Toplevel.context_of)));
+ (Scan.succeed (Toplevel.keep (print_tcset o Toplevel.context_of)));
end;