src/Pure/General/graph_display.ML

   type node
   val content_node: string -> Pretty.T list -> node
   val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
   type entry = (string * node) * string list
   val display_graph: entry list -> unit
+  val display_graph_old: entry list -> unit
 end;
 
 structure Graph_Display: GRAPH_DISPLAY =
 struct
 

   Node {name = name, content = [], unfold = unfold, directory = directory, path = path};
 
 type entry = (string * node) * string list;
 
 
-(* encode graph *)
+(* display graph *)
+
+local
 
 fun encode_node (Node {name, content, ...}) =
   (name, content) |>
     let open XML.Encode
     in pair string (YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks) end;
 
 val encode_graph =
   let open XML.Encode in list (pair (pair string encode_node) (list string)) end;
 
+in
+
+fun display_graph entries =
+  let
+    val ((bg1, bg2), en) =
+      YXML.output_markup_elem
+        (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
+  in writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en) end;
+
+end;
+
 
 (* support for old browser *)
+
+local
 
 structure Graph =
   Graph(type key = string * string val ord = prod_ord string_ord string_ord);
 
 fun build_graph entries =

   #> map (fn ((key, Node {name, unfold, content = _, directory, path}), parents) =>
     "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
     path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
   #> cat_lines;
 
+in
 
-(* display graph *)
-
-fun display_graph entries =
+fun display_graph_old entries =
   let
     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 ^ "graph" ^ en);
-
-    (*old browser*)
-    val ((bg1, bg2), en) =
-      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;
+  in writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "graph" ^ en) end;
 
 end;
+
+end;