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