11 path: string, parents: string list, content: Pretty.T list} |
11 path: string, parents: string list, content: Pretty.T list} |
12 type graph = node list |
12 type graph = node list |
13 val write_graph_browser: Path.T -> graph -> unit |
13 val write_graph_browser: Path.T -> graph -> unit |
14 val browserN: string |
14 val browserN: string |
15 val graphviewN: string |
15 val graphviewN: string |
16 val graphview_reportN: string |
16 val active_graphN: string |
17 val display_graph: graph -> unit |
17 val display_graph: graph -> unit |
18 end; |
18 end; |
19 |
19 |
20 structure Graph_Display: GRAPH_DISPLAY = |
20 structure Graph_Display: GRAPH_DISPLAY = |
21 struct |
21 struct |
31 |
31 |
32 (* print modes *) |
32 (* print modes *) |
33 |
33 |
34 val browserN = "browser"; |
34 val browserN = "browser"; |
35 val graphviewN = "graphview"; |
35 val graphviewN = "graphview"; |
36 val graphview_reportN = "graphview_report"; |
36 val active_graphN = "active_graph"; |
37 |
37 |
38 fun write_graph_browser path (graph: graph) = |
38 fun is_browser () = |
39 File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} => |
39 (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of |
|
40 SOME m => m = browserN |
|
41 | NONE => true); |
|
42 |
|
43 |
|
44 (* encode graph *) |
|
45 |
|
46 fun encode_browser (graph: graph) = |
|
47 cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} => |
40 "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
48 "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
41 path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph)); |
49 path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph); |
|
50 |
|
51 fun write_graph_browser path graph = File.write path (encode_browser graph); |
42 |
52 |
43 |
53 |
44 val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks; |
54 val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks; |
45 |
55 |
46 fun encode_graphview (graph: graph) = |
56 fun encode_graphview (graph: graph) = |
54 |
64 |
55 |
65 |
56 (* display graph *) |
66 (* display graph *) |
57 |
67 |
58 fun display_graph graph = |
68 fun display_graph graph = |
59 if print_mode_active graphview_reportN then |
69 if print_mode_active active_graphN then |
60 let |
70 let |
61 val markup = Active.make_markup Markup.graphviewN {implicit = false, properties = []}; |
71 val (markup, body) = |
62 val ((bg1, bg2), en) = YXML.output_markup_elem markup; |
72 if is_browser () then (Markup.browserN, encode_browser graph) |
63 val graph_yxml = YXML.string_of_body (encode_graphview graph); |
73 else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph)); |
64 in writeln ("See " ^ bg1 ^ graph_yxml ^ bg2 ^ "graphview" ^ en) end |
74 val ((bg1, bg2), en) = |
|
75 YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []}); |
|
76 in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end |
65 else |
77 else |
66 let |
78 let |
67 val browser = |
|
68 (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of |
|
69 SOME m => m = browserN |
|
70 | NONE => true); |
|
71 val (write, tool) = |
79 val (write, tool) = |
72 if browser then (write_graph_browser, "browser") |
80 if is_browser () then (write_graph_browser, "browser") |
73 else (write_graph_graphview, "graphview"); |
81 else (write_graph_graphview, "graphview"); |
74 |
82 |
75 val _ = writeln "Displaying graph ..."; |
83 val _ = writeln "Displaying graph ..."; |
76 val path = Isabelle_System.create_tmp_path "graph" ""; |
84 val path = Isabelle_System.create_tmp_path "graph" ""; |
77 val _ = write path graph; |
85 val _ = write path graph; |