# HG changeset patch
# User wenzelm
# Date 1429180650 -7200
# Node ID 9feddd64183eb47e95614e47c28bce4edf1605e3
# Parent  75ec8fd5d2bf15e8490678124a7eed2d8fdd700f
tuned signature;

diff -r 75ec8fd5d2bf -r 9feddd64183e src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 16 12:03:43 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 16 12:37:30 2015 +0200
@@ -948,9 +948,9 @@
     ;
     @@{command subclass} @{syntax nameref}
     ;
-    @@{command class_deps} (sort_list sort_list?)?
+    @@{command class_deps} (class_bounds class_bounds?)?
     ;
-    sort_list: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
+    class_bounds: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
   \<close>}
 
   \begin{description}
diff -r 75ec8fd5d2bf -r 9feddd64183e src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Thu Apr 16 12:03:43 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML	Thu Apr 16 12:37:30 2015 +0200
@@ -6,7 +6,8 @@
 
 signature CLASS_DEPS =
 sig
-  val class_deps: Proof.context -> sort list option * sort 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;
 
@@ -32,20 +33,19 @@
     Sorts.subalgebra (Context.pretty ctxt) restrict (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 =
+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 bounds =>
+    (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
       (Toplevel.unknown_theory o
-       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) bounds))));
+       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args))));
 
 end;