--- a/src/Pure/Isar/class.ML Wed Jan 21 17:27:58 2015 +0100
+++ b/src/Pure/Isar/class.ML Wed Jan 21 18:40:00 2015 +0100
@@ -51,7 +51,7 @@
val default_intro_tac: Proof.context -> thm list -> tactic
(*diagnostics*)
- val pretty_specification: theory -> class -> Pretty.T list
+ val pretty_specification: theory -> class -> Pretty.T list * Pretty.T list
end;
structure Class: CLASS =
@@ -750,8 +750,8 @@
else
maps (Element.pretty_ctxt_no_attribs class_ctxt) (fixes @ assumes)
|> maps (fn prt => [Pretty.fbrk, prt]);
- in if null body then [] else [Pretty.block (header @ body)] end
- else [];
+ in (header, body) end
+ else ([], []);
end;
--- a/src/Pure/Tools/class_deps.ML Wed Jan 21 17:27:58 2015 +0100
+++ b/src/Pure/Tools/class_deps.ML Wed Jan 21 18:40:00 2015 +0100
@@ -6,6 +6,7 @@
signature CLASS_DEPS =
sig
+ val inlined_class_specs: bool Config.T
val class_deps: Proof.context -> sort -> sort option -> unit
val class_deps_cmd: Proof.context -> string -> string option -> unit
end;
@@ -13,6 +14,10 @@
structure Class_Deps: CLASS_DEPS =
struct
+val inlined_class_specs = Attrib.setup_config_bool @{binding "inlined_class_specs"} (K false);
+
+val stringify = XML.content_of o YXML.parse_body o Pretty.string_of;
+
fun gen_class_deps prep_sort ctxt raw_super raw_sub =
let
val thy = Proof_Context.theory_of ctxt;
@@ -27,9 +32,23 @@
val (_, algebra) =
Sorts.subalgebra (Context.pretty ctxt)
(le_super andf sub_le) (K NONE) original_algebra;
- fun node c =
- Graph_Display.content_node (Name_Space.extern ctxt space c)
- (Class.pretty_specification thy c);
+ val inlined = Config.get ctxt inlined_class_specs;
+ fun label_for c =
+ if inlined
+ then (stringify o Pretty.block o op @) (Class.pretty_specification thy c)
+ else Name_Space.extern ctxt space c;
+ fun tooltip_for c =
+ if inlined
+ then []
+ else
+ let
+ val pretty_spec = Class.pretty_specification thy c
+ in
+ if (null o snd) pretty_spec
+ then []
+ else [(Pretty.block o op @) pretty_spec]
+ end;
+ fun node c = Graph_Display.content_node (label_for c) (tooltip_for c);
in
Sorts.classes_of algebra
|> Graph.dest