7 signature GRAPH_DISPLAY = |
7 signature GRAPH_DISPLAY = |
8 sig |
8 sig |
9 type node |
9 type node |
10 val content_node: string -> Pretty.T list -> node |
10 val content_node: string -> Pretty.T list -> node |
11 val session_node: {name: string, unfold: bool, directory: string, path: string} -> node |
11 val session_node: {name: string, unfold: bool, directory: string, path: string} -> node |
12 type graph = string list * node Graph.T |
12 type entry = (string * node) * string list |
|
13 val eq_entry: entry * entry -> bool |
|
14 type graph = entry list |
|
15 val sort_graph: graph -> graph |
13 val write_graph_browser: Path.T -> graph -> unit |
16 val write_graph_browser: Path.T -> graph -> unit |
14 val browserN: string |
17 val browserN: string |
15 val graphviewN: string |
18 val graphviewN: string |
16 val active_graphN: string |
19 val active_graphN: string |
17 val display_graph: graph -> unit |
20 val display_graph: graph -> unit |
18 end; |
21 end; |
19 |
22 |
20 structure Graph_Display: GRAPH_DISPLAY = |
23 structure Graph_Display: GRAPH_DISPLAY = |
21 struct |
24 struct |
22 |
25 |
23 (* abstract graph representation *) |
26 (* type node *) |
24 |
27 |
25 type node = {name: string, content: Pretty.T list, |
28 datatype node = |
26 unfold: bool, directory: string, path: string}; |
29 Node of {name: string, content: Pretty.T list, unfold: bool, directory: string, path: string}; |
27 |
|
28 type graph = string list * node Graph.T; |
|
29 (*partial explicit order in left argument*) |
|
30 |
30 |
31 fun content_node name content = |
31 fun content_node name content = |
32 {name = name, content = content, unfold = true, directory = "", path = ""}; |
32 Node {name = name, content = content, unfold = true, directory = "", path = ""}; |
33 |
33 |
34 fun session_node {name: string, unfold: bool, directory: string, path: string} = |
34 fun session_node {name, unfold, directory, path} = |
35 {name = name, content = [], unfold = unfold, directory = directory, path = path}; |
35 Node {name = name, content = [], unfold = unfold, directory = directory, path = path}; |
|
36 |
|
37 |
|
38 (* type graph *) |
|
39 |
|
40 type entry = (string * node) * string list; |
|
41 val eq_entry: entry * entry -> bool = op = o apply2 (#1 o #1); |
|
42 |
|
43 type graph = entry list; |
|
44 |
|
45 structure Aux_Graph = |
|
46 Graph(type key = string * string val ord = prod_ord string_ord string_ord); |
|
47 |
|
48 fun sort_graph (graph: graph) = |
|
49 let |
|
50 val ident_names = |
|
51 fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident))) |
|
52 graph Symtab.empty; |
|
53 val the_key = the o Symtab.lookup ident_names; |
|
54 val G = |
|
55 Aux_Graph.empty |
|
56 |> fold (fn ((ident, node), _) => Aux_Graph.new_node (the_key ident, node)) graph |
|
57 |> fold (fn ((ident, _), parents) => |
|
58 fold (fn parent => Aux_Graph.add_edge (the_key parent, the_key ident)) parents) graph |
|
59 in |
|
60 Aux_Graph.topological_order G |> map (fn key => |
|
61 let val (_, (node, (preds, _))) = Aux_Graph.get_entry G key |
|
62 in ((#2 key, node), map #2 (Aux_Graph.Keys.dest preds)) end) |
|
63 end; |
36 |
64 |
37 |
65 |
38 (* print modes *) |
66 (* print modes *) |
39 |
67 |
40 val browserN = "browser"; |
68 val browserN = "browser"; |
47 | NONE => true); |
75 | NONE => true); |
48 |
76 |
49 |
77 |
50 (* encode graph *) |
78 (* encode graph *) |
51 |
79 |
52 fun encode_browser ((keys, gr) : graph) = |
80 val encode_browser = |
53 fold_rev (update (op =)) (Graph.keys gr) keys |
81 map (fn ((key, Node {name, unfold, content, directory, path}), parents) => |
54 |> map (fn key => case Graph.get_node gr key of {name, unfold, content, directory, path} => |
|
55 "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^ |
82 "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^ |
56 path ^ "\" > " ^ space_implode " " (map quote (Graph.immediate_succs gr key)) ^ " ;") |
83 path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") |
57 |> cat_lines; |
84 #> cat_lines; |
58 |
85 |
59 fun write_graph_browser path graph = File.write path (encode_browser graph); |
86 fun write_graph_browser path graph = |
|
87 File.write path (encode_browser graph); |
60 |
88 |
61 |
89 |
62 val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks; |
90 fun encode_node (Node {name, content, ...}) = |
|
91 (name, content) |> |
|
92 let open XML.Encode |
|
93 in pair string (YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks) end; |
63 |
94 |
64 fun encode_graphview ((_, gr): graph) = |
95 val encode_graph = |
65 gr |
96 let open XML.Encode in list (pair (pair string encode_node) (list string)) end; |
66 |> Graph.map (fn _ => fn {name, content, ...} => (name, content)) |
|
67 |> let open XML.Encode in Graph.encode string (pair string encode_content) end; |
|
68 |
97 |
69 |
98 |
70 (* display graph *) |
99 (* display graph *) |
71 |
100 |
72 fun display_graph graph = |
101 val display_graph = |
73 if print_mode_active active_graphN then |
102 sort_graph #> (fn graph => |
74 let |
103 if print_mode_active active_graphN then |
75 val (markup, body) = |
104 let |
76 if is_browser () then (Markup.browserN, encode_browser graph) |
105 val (markup, body) = |
77 else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph)); |
106 if is_browser () then (Markup.browserN, encode_browser graph) |
78 val ((bg1, bg2), en) = |
107 else (Markup.graphviewN, YXML.string_of_body (encode_graph graph)); |
79 YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []}); |
108 val ((bg1, bg2), en) = |
80 in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end |
109 YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []}); |
81 else |
110 in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end |
82 let |
111 else |
83 val _ = writeln "Displaying graph ..."; |
112 let |
84 val path = Isabelle_System.create_tmp_path "graph" ""; |
113 val _ = writeln "Displaying graph ..."; |
85 val _ = write_graph_browser path graph; |
114 val path = Isabelle_System.create_tmp_path "graph" ""; |
86 val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &"); |
115 val _ = write_graph_browser path graph; |
87 in () end; |
116 val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &"); |
|
117 in () end); |
88 |
118 |
89 end; |
119 end; |