28 |
28 |
29 if (!snapshot.is_outdated) { |
29 if (!snapshot.is_outdated) { |
30 // FIXME avoid hard-wired stuff |
30 // FIXME avoid hard-wired stuff |
31 elem match { |
31 elem match { |
32 case XML.Elem(Markup(Markup.BROWSER, _), body) => |
32 case XML.Elem(Markup(Markup.BROWSER, _), body) => |
33 default_thread_pool.submit(() => |
33 Future.fork { |
34 { |
34 val graph_file = Isabelle_System.tmp_file("graph") |
35 val graph_file = Isabelle_System.tmp_file("graph") |
35 File.write(graph_file, XML.content(body)) |
36 File.write(graph_file, XML.content(body)) |
36 Isabelle_System.bash_env(null, |
37 Isabelle_System.bash_env(null, |
37 Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)), |
38 Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)), |
38 "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &") |
39 "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &") |
39 } |
40 }) |
|
41 |
40 |
42 case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) => |
41 case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) => |
43 default_thread_pool.submit(() => |
42 Future.fork { |
44 { |
43 val graph = |
45 val graph = |
44 Exn.capture { |
46 Exn.capture { |
45 isabelle.graphview.Model.decode_graph(body) |
47 isabelle.graphview.Model.decode_graph(body) |
46 .transitive_reduction_acyclic |
48 .transitive_reduction_acyclic |
47 } |
49 } |
48 Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) } |
50 Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) } |
49 } |
51 }) |
|
52 |
50 |
53 case XML.Elem(Markup(Markup.SENDBACK, props), _) => |
51 case XML.Elem(Markup(Markup.SENDBACK, props), _) => |
54 props match { |
52 props match { |
55 case Position.Id(id) => |
53 case Position.Id(id) => |
56 Isabelle.edit_command(snapshot, buffer, |
54 Isabelle.edit_command(snapshot, buffer, |