src/Pure/Isar/isar_cmd.ML
changeset 49569 7b6aaf446496
parent 49561 26fc70e983c2
child 49866 619acbd72664
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Sep 26 14:13:07 2012 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Sep 26 14:23:33 2012 +0200
     1.3 @@ -60,8 +60,9 @@
     1.4    val print_trans_rules: Toplevel.transition -> Toplevel.transition
     1.5    val print_methods: Toplevel.transition -> Toplevel.transition
     1.6    val print_antiquotations: Toplevel.transition -> Toplevel.transition
     1.7 +  val thy_deps: Toplevel.transition -> Toplevel.transition
     1.8 +  val locale_deps: Toplevel.transition -> Toplevel.transition
     1.9    val class_deps: Toplevel.transition -> Toplevel.transition
    1.10 -  val thy_deps: Toplevel.transition -> Toplevel.transition
    1.11    val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    1.12    val unused_thms: (string list * string list option) option ->
    1.13      Toplevel.transition -> Toplevel.transition
    1.14 @@ -409,6 +410,14 @@
    1.15        end);
    1.16    in Graph_Display.display_graph gr end);
    1.17  
    1.18 +val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.19 +  let
    1.20 +    val thy = Toplevel.theory_of state;
    1.21 +    val gr = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
    1.22 +     {name = Locale.extern thy name, ID = name, parents = parents,
    1.23 +      dir = "", unfold = true, path = "", content = [body]});
    1.24 +  in Graph_Display.display_graph gr end);
    1.25 +
    1.26  val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.27    let
    1.28      val ctxt = Toplevel.context_of state;