equal
deleted
inserted
replaced
41 case None => |
41 case None => |
42 } |
42 } |
43 } |
43 } |
44 |
44 |
45 if (!snapshot.is_outdated) { |
45 if (!snapshot.is_outdated) { |
|
46 // FIXME avoid hard-wired stuff |
|
47 |
46 elem match { |
48 elem match { |
47 case XML.Elem(Markup(Markup.GRAPHVIEW, Position.Id(exec_id)), body) => |
49 case XML.Elem(Markup(Markup.BROWSER, _), body) => |
|
50 default_thread_pool.submit(() => |
|
51 { |
|
52 val graph_file = File.tmp_file("graph") |
|
53 File.write(graph_file, XML.content(body)) |
|
54 Isabelle_System.bash_env(null, |
|
55 Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)), |
|
56 "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &") |
|
57 }) |
|
58 |
|
59 case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) => |
48 default_thread_pool.submit(() => |
60 default_thread_pool.submit(() => |
49 { |
61 { |
50 val graph = |
62 val graph = |
51 Exn.capture { |
63 Exn.capture { |
52 isabelle.graphview.Model.decode_graph(body) |
64 isabelle.graphview.Model.decode_graph(body) |