src/Pure/Isar/isar_cmd.ML
changeset 59208 2486d625878b
parent 59207 6b030dc97a4f
child 59210 8658b4290aed
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:13:11 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:15:52 2014 +0100
     1.3 @@ -275,25 +275,26 @@
     1.4      val thy = Toplevel.theory_of state;
     1.5      val thy_session = Present.session_name thy;
     1.6  
     1.7 -    val graph = rev (Theory.nodes_of thy) |> map (fn node =>
     1.8 +    val gr_nodes = rev (Theory.nodes_of thy) |> map (fn node =>
     1.9        let
    1.10          val name = Context.theory_name node;
    1.11          val parents = map Context.theory_name (Theory.parents_of node);
    1.12          val session = Present.session_name node;
    1.13          val unfold = (session = thy_session);
    1.14        in
    1.15 -       {name = name, ident = name, parents = parents, directory = session,
    1.16 -        unfold = unfold, path = "", content = []}
    1.17 +       ((name, Graph_Display.session_node
    1.18 +         {name = name, directory = session, unfold = unfold, path = ""}), parents)
    1.19        end);
    1.20 -  in Graph_Display.display_graph graph end);
    1.21 +  in Graph_Display.display_graph (map (fst o fst) gr_nodes, Graph.make gr_nodes) end);
    1.22  
    1.23  val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.24    let
    1.25      val thy = Toplevel.theory_of state;
    1.26 -    val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
    1.27 -     {name = Locale.extern thy name, ident = name, parents = parents,
    1.28 -      directory = "", unfold = true, path = "", content = [body]});
    1.29 -  in Graph_Display.display_graph graph end);
    1.30 +    val gr = Locale.pretty_locale_deps thy
    1.31 +      |> map (fn {name, parents, body} => ((name,
    1.32 +          Graph_Display.content_node (Locale.extern thy name) [body]), parents))
    1.33 +      |> Graph.make;
    1.34 +  in Graph_Display.display_graph ([], gr) end);
    1.35  
    1.36  
    1.37  (* print theorems, terms, types etc. *)