separated class_deps command into separate file
authorhaftmann
Sun Sep 07 17:51:28 2014 +0200 (2014-09-07 ago)
changeset 582015bf56c758e02
parent 58200 d95055489fce
child 58202 be1d10595b7b
separated class_deps command into separate file
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Pure.thy
src/Pure/Tools/class_deps.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Sep 07 14:39:23 2014 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Sep 07 17:51:28 2014 +0200
     1.3 @@ -38,7 +38,6 @@
     1.4    val pretty_theorems: bool -> Toplevel.state -> Pretty.T list
     1.5    val thy_deps: Toplevel.transition -> Toplevel.transition
     1.6    val locale_deps: Toplevel.transition -> Toplevel.transition
     1.7 -  val class_deps: Toplevel.transition -> Toplevel.transition
     1.8    val print_stmts: string list * (Facts.ref * Token.src list) list
     1.9      -> Toplevel.transition -> Toplevel.transition
    1.10    val print_thms: string list * (Facts.ref * Token.src list) list
    1.11 @@ -298,19 +297,6 @@
    1.12        dir = "", unfold = true, path = "", content = [body]});
    1.13    in Graph_Display.display_graph gr end);
    1.14  
    1.15 -val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.16 -  let
    1.17 -    val ctxt = Toplevel.context_of state;
    1.18 -    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
    1.19 -    val classes = Sorts.classes_of algebra;
    1.20 -    fun entry (c, (i, (_, cs))) =
    1.21 -      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
    1.22 -            dir = "", unfold = true, path = "", content = []});
    1.23 -    val gr =
    1.24 -      Graph.fold (cons o entry) classes []
    1.25 -      |> sort (int_ord o pairself #1) |> map #2;
    1.26 -  in Graph_Display.display_graph gr end);
    1.27 -
    1.28  
    1.29  (* print theorems, terms, types etc. *)
    1.30  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Sep 07 14:39:23 2014 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Sep 07 17:51:28 2014 +0200
     2.3 @@ -890,10 +890,6 @@
     2.4      (Scan.succeed Isar_Cmd.locale_deps);
     2.5  
     2.6  val _ =
     2.7 -  Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
     2.8 -    (Scan.succeed Isar_Cmd.class_deps);
     2.9 -
    2.10 -val _ =
    2.11    Outer_Syntax.improper_command @{command_spec "print_binds"}
    2.12      "print term bindings of proof context -- Proof General legacy"
    2.13      (Scan.succeed (Toplevel.unknown_context o
     3.1 --- a/src/Pure/Pure.thy	Sun Sep 07 14:39:23 2014 +0200
     3.2 +++ b/src/Pure/Pure.thy	Sun Sep 07 17:51:28 2014 +0200
     3.3 @@ -113,6 +113,7 @@
     3.4  ML_file "Tools/rail.ML"
     3.5  ML_file "Tools/rule_insts.ML";
     3.6  ML_file "Tools/thm_deps.ML";
     3.7 +ML_file "Tools/class_deps.ML"
     3.8  ML_file "Tools/find_theorems.ML"
     3.9  ML_file "Tools/find_consts.ML"
    3.10  ML_file "Tools/proof_general_pure.ML"
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Tools/class_deps.ML	Sun Sep 07 17:51:28 2014 +0200
     4.3 @@ -0,0 +1,32 @@
     4.4 +(*  Title:      Pure/Tools/class_deps.ML
     4.5 +    Author:     Florian Haftmann, TU Muenchen
     4.6 +
     4.7 +Visualization of class dependencies.
     4.8 +*)
     4.9 +
    4.10 +signature CLASS_DEPS =
    4.11 +sig
    4.12 +  val class_deps: Toplevel.transition -> Toplevel.transition
    4.13 +end;
    4.14 +
    4.15 +structure Class_deps: CLASS_DEPS =
    4.16 +struct
    4.17 +
    4.18 +val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    4.19 +  let
    4.20 +    val ctxt = Toplevel.context_of state;
    4.21 +    val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
    4.22 +    val classes = Sorts.classes_of algebra;
    4.23 +    fun entry (c, (i, (_, cs))) =
    4.24 +      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
    4.25 +            dir = "", unfold = true, path = "", content = []});
    4.26 +    val gr =
    4.27 +      Graph.fold (cons o entry) classes []
    4.28 +      |> sort (int_ord o pairself #1) |> map #2;
    4.29 +  in Graph_Display.display_graph gr end);
    4.30 +
    4.31 +val _ =
    4.32 +  Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
    4.33 +    (Scan.succeed class_deps);
    4.34 +
    4.35 +end;