# HG changeset patch
# User wenzelm
# Date 1420452930 -3600
# Node ID d0d0953e063f48f283f4c42fe00317c69f35900b
# Parent  962ad3942ea7656c0f124f42cd336dad85a3abe8
eliminated print modes: offer new and old graph;

diff -r 962ad3942ea7 -r d0d0953e063f src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Mon Jan 05 00:07:01 2015 +0100
+++ b/src/Pure/General/graph_display.ML	Mon Jan 05 11:15:30 2015 +0100
@@ -13,8 +13,6 @@
   val eq_entry: entry * entry -> bool
   val sort_graph: entry list -> entry list
   val write_graph_browser: Path.T -> entry list -> unit
-  val browserN: string
-  val graphviewN: string
   val display_graph: entry list -> unit
 end;
 
@@ -60,17 +58,6 @@
     in ((#2 key, node), map #2 (Graph.Keys.dest preds)) end));
 
 
-(* print modes *)
-
-val browserN = "browser";
-val graphviewN = "graphview";
-
-fun is_browser () =
-  (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
-    SOME m => m = browserN
-  | NONE => true);
-
-
 (* encode graph *)
 
 val encode_browser =
@@ -97,11 +84,18 @@
 val display_graph =
   sort_graph #> (fn entries =>
     let
-      val (markup, body) =
-        if is_browser () then (Markup.browserN, encode_browser entries)
-        else (Markup.graphviewN, YXML.string_of_body (encode_graph entries));
+      val ((bg1, bg2), en) =
+        YXML.output_markup_elem
+          (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
+      val _ =
+        writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "new graph" ^ en);
+
       val ((bg1, bg2), en) =
-        YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
-    in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end);
+        YXML.output_markup_elem
+          (Active.make_markup Markup.browserN {implicit = false, properties = []});
+      val _ =
+        writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "old graph" ^ en);
+  in () end);
+
 
 end;