--- a/src/Pure/General/graph_display.ML Wed Dec 31 20:42:45 2014 +0100
+++ b/src/Pure/General/graph_display.ML Wed Dec 31 20:55:11 2014 +0100
@@ -16,7 +16,6 @@
val write_graph_browser: Path.T -> graph -> unit
val browserN: string
val graphviewN: string
- val active_graphN: string
val display_graph: graph -> unit
end;
@@ -67,7 +66,6 @@
val browserN = "browser";
val graphviewN = "graphview";
-val active_graphN = "active_graph";
fun is_browser () =
(case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
@@ -100,20 +98,12 @@
val display_graph =
sort_graph #> (fn graph =>
- if print_mode_active active_graphN then
- let
- val (markup, body) =
- if is_browser () then (Markup.browserN, encode_browser graph)
- else (Markup.graphviewN, YXML.string_of_body (encode_graph graph));
- val ((bg1, bg2), en) =
- YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
- in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
- else
- let
- val _ = writeln "Displaying graph ...";
- val path = Isabelle_System.create_tmp_path "graph" "";
- val _ = write_graph_browser path graph;
- val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
- in () end);
+ let
+ val (markup, body) =
+ if is_browser () then (Markup.browserN, encode_browser graph)
+ else (Markup.graphviewN, YXML.string_of_body (encode_graph graph));
+ val ((bg1, bg2), en) =
+ YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
+ in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end);
end;
--- a/src/Pure/System/isabelle_process.ML Wed Dec 31 20:42:45 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML Wed Dec 31 20:55:11 2014 +0100
@@ -186,8 +186,7 @@
(* init *)
-val default_modes1 =
- [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN, Graph_Display.active_graphN];
+val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
val init = uninterruptible (fn _ => fn rendezvous =>