# HG changeset patch # User wenzelm # Date 1420055711 -3600 # Node ID 7b74e84087117c7568b82f0146d2fed799c48e13 # Parent 8658b4290aedd593ba11495afb6ac12c77098c2f eliminated TTY/PG legacy; diff -r 8658b4290aed -r 7b74e8408711 src/Pure/General/graph_display.ML --- 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; diff -r 8658b4290aed -r 7b74e8408711 src/Pure/System/isabelle_process.ML --- 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 =>