formal Theory.check, with markup and completion;

--- 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))) #>
 

--- 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;

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