clarified 'thm_deps' command;

--- a/NEWS	Fri Aug 23 13:32:27 2019 +0200
+++ b/NEWS	Fri Aug 23 14:32:51 2019 +0200
@@ -23,6 +23,10 @@
 * Command 'thm_oracles' prints all oracles used in given theorems,
 covering the full graph of transitive dependencies.
 
+* Command 'thm_deps' prints immediate theorem dependencies of the given
+facts. The former graph visualization has been discontinued, because it
+was hardly usable.
+
 
 *** Isar ***
 

--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Aug 23 13:32:27 2019 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Aug 23 14:32:51 2019 +0200
@@ -589,8 +589,9 @@
   matches against subtypes. The criterion \<open>name: p\<close> and the prefix ``\<open>-\<close>''
   function as described for @{command "find_theorems"}.
 
-  \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close> visualizes dependencies of facts, using
-  Isabelle's graph browser tool (see also @{cite "isabelle-system"}).
+  \<^descr> @{command "thm_deps"}~\<open>thms\<close> prints immediate theorem dependencies, i.e.\
+  the union of all theorems that are used directly to prove the argument
+  facts, without going deeper into the dependency graph.
 
   \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close> displays all theorems
   that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close> or their parents but not in \<open>A\<^sub>1 \<dots>

--- a/src/Pure/Pure.thy	Fri Aug 23 13:32:27 2019 +0200
+++ b/src/Pure/Pure.thy	Fri Aug 23 14:32:51 2019 +0200
@@ -1301,13 +1301,14 @@
 
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>thm_deps\<close> "visualize theorem dependencies"
+  Outer_Syntax.command \<^command_keyword>\<open>thm_deps\<close>
+    "print theorem dependencies (immediate non-transitive)"
     (Parse.thms1 >> (fn args =>
       Toplevel.keep (fn st =>
         let
           val thy = Toplevel.theory_of st;
           val ctxt = Toplevel.context_of st;
-        in Thm_Deps.thm_deps_cmd thy (Attrib.eval_thms ctxt args) end)));
+        in Pretty.writeln (Thm_Deps.pretty_thm_deps thy (Attrib.eval_thms ctxt args)) end)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>thm_oracles\<close>

--- a/src/Pure/Thy/export_theory.ML	Fri Aug 23 13:32:27 2019 +0200
+++ b/src/Pure/Thy/export_theory.ML	Fri Aug 23 14:32:51 2019 +0200
@@ -259,7 +259,7 @@
 
     fun encode_thm raw_thm =
       let
-        val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy raw_thm);
+        val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]);
         val thm = clean_thm raw_thm;
         val raw_proof =
           if Proofterm.export_enabled () then Thm.reconstruct_proof_of thm else Proofterm.MinProof;

--- a/src/Pure/Thy/thm_deps.ML	Fri Aug 23 13:32:27 2019 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Fri Aug 23 14:32:51 2019 +0200
@@ -10,8 +10,8 @@
   val all_oracles: thm list -> Proofterm.oracle list
   val has_skip_proof: thm list -> bool
   val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T
-  val thm_deps: theory -> thm -> (Proofterm.thm_id * Thm_Name.T) list
-  val thm_deps_cmd: theory -> thm list -> unit
+  val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list
+  val pretty_thm_deps: theory -> thm list -> Pretty.T
   val unused_thms_cmd: theory list * theory list -> (string * thm) list
 end;
 
@@ -62,45 +62,21 @@
               |> fold deps (Proofterm.thm_node_thms thm_node))
         end;
   in
-    fn thm =>
-      (fold deps (Thm.thm_deps (Thm.transfer thy thm)) Inttab.empty, [])
+    fn thms =>
+      (fold (fold deps o Thm.thm_deps o Thm.transfer thy) thms Inttab.empty, [])
       |-> Inttab.fold_rev (fn (_, SOME entry) => cons entry | _ => I)
   end;
 
-
-(* thm_deps_cmd *)
-
-fun thm_deps_cmd thy thms =
+fun pretty_thm_deps thy thms =
   let
-    fun make_node name directory =
-      Graph_Display.session_node
-       {name = Long_Name.base_name name, directory = directory, unfold = false, path = ""};
-    fun add_dep {name = "", ...} = I
-      | add_dep {name = name, body = PBody {thms = thms', ...}, ...} =
-          let
-            val prefix = #1 (split_last (Long_Name.explode name));
-            val session =
-              (case prefix of
-                a :: _ =>
-                  (case try (Context.get_theory {long = false} thy) a of
-                    SOME thy =>
-                      (case Present.theory_qualifier thy of
-                        "" => []
-                      | session => [session])
-                  | NONE => [])
-              | _ => ["global"]);
-            val node = make_node name (space_implode "/" (session @ prefix));
-            val deps = filter_out (fn s => s = "") (map (Proofterm.thm_node_name o #2) thms');
-          in Symtab.update (name, (node, deps)) end;
-    val entries0 = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) Symtab.empty;
-    val entries1 =
-      Symtab.fold (fn (_, (_, deps)) => deps |> fold (fn d => fn tab =>
-        if Symtab.defined tab d then tab
-        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_old
-  end;
+    val ctxt = Proof_Context.init_global thy;
+    val items =
+      map #2 (thm_deps thy thms)
+      |> map (fn (name, i) => (Proof_Context.markup_extern_fact ctxt name, i))
+      |> sort_by (#2 o #1)
+      |> map (fn ((marks, xname), i) =>
+          Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]);
+  in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end;
 
 
 (* unused_thms_cmd *)