# HG changeset patch
# User wenzelm
# Date 1429178623 -7200
# Node ID 75ec8fd5d2bf15e8490678124a7eed2d8fdd700f
# Parent  8bd5999133d4776926ddd71d4556fca06b2530dd
misc tuning and clarification;

diff -r 8bd5999133d4 -r 75ec8fd5d2bf src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Thu Apr 16 11:22:36 2015 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Thu Apr 16 12:03:43 2015 +0200
@@ -948,8 +948,9 @@
     ;
     @@{command subclass} @{syntax nameref}
     ;
-    @@{command class_deps} ( ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) ) \<newline>
-      ( @{syntax sort} | ( '(' ( @{syntax sort} + @'|' ) ')' ) )? )?
+    @@{command class_deps} (sort_list sort_list?)?
+    ;
+    sort_list: @{syntax sort} | '(' (@{syntax sort} + @'|') ')'
   \<close>}
 
   \begin{description}
@@ -1012,11 +1013,13 @@
   \item @{command "print_classes"} prints all classes in the current
   theory.
 
-  \item @{command "class_deps"} visualizes all classes and their
-  subclass relations as a Hasse diagram.  An optional first argument
-  constrains the set of classes to all subclasses of at least one given
-  sort, an optional second rgument to all superclasses of at least one given
-  sort.
+  \item @{command "class_deps"} visualizes classes and their subclass
+  relations as a directed acyclic graph. By default, all classes from the
+  current theory context are show. This may be restricted by optional bounds
+  as follows: @{command "class_deps"}~@{text upper} or @{command
+  "class_deps"}~@{text "upper lower"}. A class is visualized, iff it is a
+  subclass of some sort from @{text upper} and a superclass of some sort
+  from @{text lower}.
 
   \item @{method intro_classes} repeatedly expands all class
   introduction rules of this theory.  Note that this method usually
diff -r 8bd5999133d4 -r 75ec8fd5d2bf src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Thu Apr 16 11:22:36 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML	Thu Apr 16 12:03:43 2015 +0200
@@ -6,35 +6,31 @@
 
 signature CLASS_DEPS =
 sig
-  val class_deps: Proof.context -> sort list option -> sort list option -> unit
-  val class_deps_cmd: Proof.context -> string list option -> string list option -> unit
+  val class_deps: Proof.context -> sort list option * sort list option -> unit
+  val class_deps_cmd: Proof.context -> string list option * string list option -> unit
 end;
 
 structure Class_Deps: CLASS_DEPS =
 struct
 
-fun gen_class_deps prep_sort ctxt raw_subs raw_supers =
+fun gen_class_deps prep_sort ctxt raw_bounds =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val some_subs = (Option.map o map) (prep_sort ctxt) raw_subs;
-    val some_supers = (Option.map o map) (prep_sort ctxt) raw_supers;
-    val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
-    val sort_le = curry (Sorts.sort_le original_algebra);
-    val le_sub = case some_subs of
-      SOME subs => (fn class => exists (sort_le [class]) subs)
-    | NONE => K true;
-    val super_le = case some_supers of
-      SOME supers => (fn class => exists (fn super => sort_le super [class]) supers)
-    | NONE => K true
-    val (_, algebra) =
-      Sorts.subalgebra (Context.pretty ctxt)
-        (le_sub andf super_le) (K NONE) original_algebra;
+    val (upper, lower) = apply2 ((Option.map o map) (prep_sort ctxt)) raw_bounds;
+    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
+    val sort_le = curry (Sorts.sort_le algebra);
+    val restrict =
+      (case upper of
+        SOME bs => (fn c => exists (fn b => sort_le [c] b) bs)
+      | NONE => K true) andf
+      (case lower of
+        SOME bs => (fn c => exists (fn b => sort_le b [c]) bs)
+      | NONE => K true);
     fun node c =
       Graph_Display.content_node (Name_Space.extern ctxt space c)
-        (Class.pretty_specification thy c);
+        (Class.pretty_specification (Proof_Context.theory_of ctxt) c);
   in
-    Sorts.classes_of algebra
-    |> Graph.dest
+    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;
@@ -42,13 +38,14 @@
 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 parse_sort_list = (Parse.sort >> single)
-  || (@{keyword "("} |-- Parse.enum "|" Parse.sort --| @{keyword ")"});
+val parse_sort_list =
+  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 (super, sub) =>
+    ((Scan.option parse_sort_list -- Scan.option parse_sort_list) >> (fn bounds =>
       (Toplevel.unknown_theory o
-       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
+       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) bounds))));
 
 end;