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;