author | wenzelm |
Mon, 10 Mar 2014 13:55:03 +0100 | |
changeset 56025 | d74fed45fa8b |
parent 50715 | 8cfd585b9162 |
child 57032 | cf570f3ecdc1 |
permissions | -rw-r--r-- |
49561 | 1 |
(* Title: Pure/General/graph_display.ML |
2 |
Author: Makarius |
|
3 |
||
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
4 |
Generic graph display, with browser and graphview backends. |
49561 | 5 |
*) |
6 |
||
7 |
signature GRAPH_DISPLAY = |
|
8 |
sig |
|
9 |
type node = |
|
10 |
{name: string, ID: string, dir: string, unfold: bool, |
|
11 |
path: string, parents: string list, content: Pretty.T list} |
|
12 |
type graph = node list |
|
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
13 |
val write_graph_browser: Path.T -> graph -> unit |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
14 |
val browserN: string |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
15 |
val graphviewN: string |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
16 |
val active_graphN: string |
49561 | 17 |
val display_graph: graph -> unit |
18 |
end; |
|
19 |
||
20 |
structure Graph_Display: GRAPH_DISPLAY = |
|
21 |
struct |
|
22 |
||
23 |
(* external graph representation *) |
|
24 |
||
25 |
type node = |
|
26 |
{name: string, ID: string, dir: string, unfold: bool, |
|
27 |
path: string, parents: string list, content: Pretty.T list}; |
|
28 |
||
29 |
type graph = node list; |
|
30 |
||
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
31 |
|
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
32 |
(* print modes *) |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
33 |
|
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
34 |
val browserN = "browser"; |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
35 |
val graphviewN = "graphview"; |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
36 |
val active_graphN = "active_graph"; |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
37 |
|
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
38 |
fun is_browser () = |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
39 |
(case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
40 |
SOME m => m = browserN |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
41 |
| NONE => true); |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
42 |
|
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
43 |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
44 |
(* encode graph *) |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
45 |
|
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
46 |
fun encode_browser (graph: graph) = |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
47 |
cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} => |
49561 | 48 |
"\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
49 |
path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph); |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
50 |
|
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
51 |
fun write_graph_browser path graph = File.write path (encode_browser graph); |
49561 | 52 |
|
53 |
||
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
54 |
val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks; |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
55 |
|
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
56 |
fun encode_graphview (graph: graph) = |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
57 |
Graph.empty |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
58 |
|> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
59 |
|> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
60 |
|> let open XML.Encode in Graph.encode string (pair string encode_content) end; |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
61 |
|
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
62 |
fun write_graph_graphview path graph = |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
63 |
File.write path (YXML.string_of_body (encode_graphview graph)); |
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
64 |
|
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
65 |
|
49561 | 66 |
(* display graph *) |
67 |
||
68 |
fun display_graph graph = |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
69 |
if print_mode_active active_graphN then |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50201
diff
changeset
|
70 |
let |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
71 |
val (markup, body) = |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
72 |
if is_browser () then (Markup.browserN, encode_browser graph) |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
73 |
else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph)); |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
74 |
val ((bg1, bg2), en) = |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
75 |
YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []}); |
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
76 |
in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
77 |
else |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
78 |
let |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
79 |
val (write, tool) = |
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50450
diff
changeset
|
80 |
if is_browser () then (write_graph_browser, "browser") |
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
81 |
else (write_graph_graphview, "graphview"); |
49565
ea4308b7ef0f
ML support for generic graph display, with browser and graphview backends (via print modes);
wenzelm
parents:
49561
diff
changeset
|
82 |
|
49566
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
83 |
val _ = writeln "Displaying graph ..."; |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
84 |
val path = Isabelle_System.create_tmp_path "graph" ""; |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
85 |
val _ = write path graph; |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
86 |
val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &"); |
66cbf8bb4693
basic integration of graphview into document model;
wenzelm
parents:
49565
diff
changeset
|
87 |
in () end; |
49561 | 88 |
|
89 |
end; |
|
90 |