# HG changeset patch # User wenzelm # Date 1429197528 -7200 # Node ID 73c2603427041657fdc2933f5ee2a0472d43a746 # Parent 3c66b0a9d7b0f625ce3391d334c8e8e3ce8947d8 formal Theory.check, with markup and completion; diff -r 3c66b0a9d7b0 -r 73c260342704 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Thu Apr 16 16:19:39 2015 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Thu Apr 16 17:18:48 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))) #> diff -r 3c66b0a9d7b0 -r 73c260342704 src/Pure/Tools/thy_deps.ML --- a/src/Pure/Tools/thy_deps.ML Thu Apr 16 16:19:39 2015 +0200 +++ b/src/Pure/Tools/thy_deps.ML Thu Apr 16 17:18:48 2015 +0200 @@ -6,21 +6,22 @@ signature THY_DEPS = sig - val thy_deps: theory -> theory list option * theory list option -> Graph_Display.entry list - val thy_deps_cmd: theory -> string list option * string list option -> unit + 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 _ thy0 (NONE, NONE) = +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 thy0 end - | gen_thy_deps prep_thy thy0 bounds = + 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 thy0)) bounds; + val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds; val rel = Theory.subthy o swap; val pred = (case upper of @@ -32,18 +33,22 @@ 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 Theory.nodes_of thy0 |> filter pred |> map node end; + in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end; -val thy_deps = gen_thy_deps (K I); -val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Context.get_theory; +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.theory_xname >> single || - (@{keyword "("} |-- Parse.enum "|" Parse.theory_xname --| @{keyword ")"}); + 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.theory_of st) args))); + (fn args => Toplevel.keep (fn st => thy_deps_cmd (Toplevel.context_of st) args))); end; diff -r 3c66b0a9d7b0 -r 73c260342704 src/Pure/theory.ML --- a/src/Pure/theory.ML Thu Apr 16 16:19:39 2015 +0200 +++ b/src/Pure/theory.ML Thu Apr 16 17:18:48 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 *)