1(*  Title:      Pure/General/graph_display.ML
2    Author:     Makarius
3
4Support for graph display.
5*)
6
7signature GRAPH_DISPLAY =
8sig
9  type node
10  val content_node: string -> Pretty.T list -> node
11  val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
12  type entry = (string * node) * string list
13  val display_graph: entry list -> unit
14  val display_graph_old: entry list -> unit
15end;
16
17structure Graph_Display: GRAPH_DISPLAY =
18struct
19
20(* graph entries *)
21
22datatype node =
23  Node of {name: string, content: Pretty.T list, unfold: bool, directory: string, path: string};
24
25fun content_node name content =
26  Node {name = name, content = content, unfold = true, directory = "", path = ""};
27
28fun session_node {name, unfold, directory, path} =
29  Node {name = name, content = [], unfold = unfold, directory = directory, path = path};
30
31type entry = (string * node) * string list;
32
33
34(* display graph *)
35
36local
37
38fun encode_node (Node {name, content, ...}) =
39  (name, content) |>
40    let open XML.Encode
41    in pair string (YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks) end;
42
43val encode_graph =
44  let open XML.Encode in list (pair (pair string encode_node) (list string)) end;
45
46in
47
48fun display_graph entries =
49  let
50    val ((bg1, bg2), en) =
51      YXML.output_markup_elem
52        (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
53  in writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en) end;
54
55end;
56
57
58(* support for old browser *)
59
60local
61
62structure Graph =
63  Graph(type key = string * string val ord = prod_ord string_ord string_ord);
64
65fun build_graph entries =
66  let
67    val ident_names =
68      fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident)))
69        entries Symtab.empty;
70    val the_key = the o Symtab.lookup ident_names;
71  in
72    Graph.empty
73    |> fold (fn ((ident, node), _) => Graph.new_node (the_key ident, node)) entries
74    |> fold (fn ((ident, _), parents) =>
75        fold (fn parent => Graph.add_edge (the_key parent, the_key ident)) parents) entries
76  end;
77
78val sort_graph = build_graph #> (fn graph =>
79  Graph.topological_order graph |> map (fn key =>
80    let val (_, (node, (preds, _))) = Graph.get_entry graph key
81    in ((#2 key, node), map #2 (Graph.Keys.dest preds)) end));
82
83val encode_browser =
84  sort_graph
85  #> map (fn ((key, Node {name, unfold, content = _, directory, path}), parents) =>
86    "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
87    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
88  #> cat_lines;
89
90in
91
92fun display_graph_old entries =
93  let
94    val ((bg1, bg2), en) =
95      YXML.output_markup_elem
96        (Active.make_markup Markup.browserN {implicit = false, properties = []});
97  in writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "graph" ^ en) end;
98
99end;
100
101end;
102