src/Pure/Tools/thy_deps.ML
author wenzelm
Thu Jun 21 14:49:21 2018 +0200 (14 months ago)
changeset 68482 cb84beb84ca9
parent 65491 7fb81fa1d668
permissions -rw-r--r--
clarified signature;
     1 (*  Title:      Pure/Tools/thy_deps.ML
     2     Author:     Makarius
     3 
     4 Visualization of theory dependencies.
     5 *)
     6 
     7 signature THY_DEPS =
     8 sig
     9   val thy_deps: Proof.context -> theory list option * theory list option ->
    10     Graph_Display.entry list
    11   val thy_deps_cmd: Proof.context ->
    12     (string * Position.T) list option * (string * Position.T) list option -> unit
    13 end;
    14 
    15 structure Thy_Deps: THY_DEPS =
    16 struct
    17 
    18 fun gen_thy_deps prep_thy ctxt bounds =
    19   let
    20     val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
    21     val rel = Context.subthy o swap;
    22     val pred =
    23       (case upper of
    24         SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs)
    25       | NONE => K true) andf
    26       (case lower of
    27         SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs)
    28       | NONE => K true);
    29     fun node thy =
    30       ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []),
    31         map Context.theory_name (filter pred (Theory.parents_of thy)));
    32   in map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
    33 
    34 val thy_deps =
    35   gen_thy_deps (fn ctxt => fn thy =>
    36     let val thy0 = Proof_Context.theory_of ctxt
    37     in if Context.subthy (thy, thy0) then thy else raise THEORY ("Bad theory", [thy, thy0]) end);
    38 
    39 val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps (Theory.check {long = false});
    40 
    41 end;