restrictive options for class dependencies

--- a/NEWS	Sun Sep 07 17:51:28 2014 +0200
+++ b/NEWS	Sun Sep 07 17:51:32 2014 +0200
@@ -15,6 +15,12 @@
 semantics due to external visual order vs. internal reverse order.
 
 
+*** Pure ***
+
+* Command "class_deps" takes optional sort arguments constraining
+the search space.
+
+
 *** HOL ***
 
 * Command and antiquotation "value" provide different evaluation slots (again),

--- a/src/Doc/Classes/Classes.thy	Sun Sep 07 17:51:28 2014 +0200
+++ b/src/Doc/Classes/Classes.thy	Sun Sep 07 17:51:32 2014 +0200
@@ -627,7 +627,9 @@
       together with associated operations etc.
 
     \item[@{command "class_deps"}] visualizes the subclass relation
-      between all classes as a Hasse diagram.
+      between all classes as a Hasse diagram.  An optional first sort argument
+      constrains the set of classes to all subclasses of this sort,
+      an optional second sort argument to all superclasses of this sort.
 
   \end{description}
 *}

--- a/src/Doc/Isar_Ref/Spec.thy	Sun Sep 07 17:51:28 2014 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sun Sep 07 17:51:32 2014 +0200
@@ -832,6 +832,8 @@
       @{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} )
     ;
     @@{command subclass} @{syntax target}? @{syntax nameref}
+    ;
+    @@{command class_deps} @{syntax sort}? @{syntax sort}?
   \<close>}
 
   \begin{description}
@@ -895,7 +897,9 @@
   theory.
 
   \item @{command "class_deps"} visualizes all classes and their
-  subclass relations as a Hasse diagram.
+  subclass relations as a Hasse diagram.  An optional first sort argument
+  constrains the set of classes to all subclasses of this sort,
+  an optional second sort argument to all superclasses of this sort.
 
   \item @{method intro_classes} repeatedly expands all class
   introduction rules of this theory.  Note that this method usually

--- a/src/Pure/Tools/class_deps.ML	Sun Sep 07 17:51:28 2014 +0200
+++ b/src/Pure/Tools/class_deps.ML	Sun Sep 07 17:51:32 2014 +0200
@@ -6,16 +6,24 @@
 
 signature CLASS_DEPS =
 sig
-  val class_deps: Toplevel.transition -> Toplevel.transition
+  val visualize: Proof.context -> sort -> sort option -> unit
+  val visualize_cmd: Proof.context -> string -> string option -> unit
 end;
 
 structure Class_deps: CLASS_DEPS =
 struct
 
-val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+fun gen_visualize prep_sort ctxt raw_super raw_sub =
   let
-    val ctxt = Toplevel.context_of state;
-    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
+    val super = prep_sort ctxt raw_super;
+    val sub = Option.map (prep_sort ctxt) raw_sub;
+    val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
+    fun le_super class = Sorts.sort_le original_algebra ([class], super);
+    val sub_le = case sub of
+      NONE => K true |
+      SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]);
+    val (_, algebra) = Sorts.subalgebra (Context.pretty ctxt)
+      (le_super andf sub_le) (K NONE) original_algebra;
     val classes = Sorts.classes_of algebra;
     fun entry (c, (i, (_, cs))) =
       (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
@@ -23,10 +31,14 @@
     val gr =
       Graph.fold (cons o entry) classes []
       |> sort (int_ord o pairself #1) |> map #2;
-  in Graph_Display.display_graph gr end);
+  in Graph_Display.display_graph gr end;
+
+val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
+val visualize_cmd = gen_visualize Syntax.read_sort;
 
 val _ =
   Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
-    (Scan.succeed class_deps);
+    ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
+      ((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
 
 end;