equal
deleted
inserted
replaced
32 case XML.Elem(Markup(Markup.BROWSER, _), body) => |
32 case XML.Elem(Markup(Markup.BROWSER, _), body) => |
33 Future.fork { |
33 Future.fork { |
34 val graph_file = Isabelle_System.tmp_file("graph") |
34 val graph_file = Isabelle_System.tmp_file("graph") |
35 File.write(graph_file, XML.content(body)) |
35 File.write(graph_file, XML.content(body)) |
36 Isabelle_System.bash_env(null, |
36 Isabelle_System.bash_env(null, |
37 Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)), |
37 Map("GRAPH_FILE" -> File.standard_path(graph_file)), |
38 "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &") |
38 "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &") |
39 } |
39 } |
40 |
40 |
41 case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) => |
41 case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) => |
42 Future.fork { |
42 Future.fork { |