src/Pure/General/graph_display.ML
changeset 50715 8cfd585b9162
parent 50450 358b6020f8b6
child 57032 cf570f3ecdc1
     1.1 --- a/src/Pure/General/graph_display.ML	Fri Jan 04 11:21:31 2013 +0100
     1.2 +++ b/src/Pure/General/graph_display.ML	Fri Jan 04 12:33:25 2013 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4    val write_graph_browser: Path.T -> graph -> unit
     1.5    val browserN: string
     1.6    val graphviewN: string
     1.7 -  val graphview_reportN: string
     1.8 +  val active_graphN: string
     1.9    val display_graph: graph -> unit
    1.10  end;
    1.11  
    1.12 @@ -33,12 +33,22 @@
    1.13  
    1.14  val browserN = "browser";
    1.15  val graphviewN = "graphview";
    1.16 -val graphview_reportN = "graphview_report";
    1.17 +val active_graphN = "active_graph";
    1.18 +
    1.19 +fun is_browser () =
    1.20 +  (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
    1.21 +    SOME m => m = browserN
    1.22 +  | NONE => true);
    1.23 +
    1.24  
    1.25 -fun write_graph_browser path (graph: graph) =
    1.26 -  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    1.27 +(* encode graph *)
    1.28 +
    1.29 +fun encode_browser (graph: graph) =
    1.30 +  cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    1.31      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.32 -    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph));
    1.33 +    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
    1.34 +
    1.35 +fun write_graph_browser path graph = File.write path (encode_browser graph);
    1.36  
    1.37  
    1.38  val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
    1.39 @@ -56,20 +66,18 @@
    1.40  (* display graph *)
    1.41  
    1.42  fun display_graph graph =
    1.43 -  if print_mode_active graphview_reportN then
    1.44 +  if print_mode_active active_graphN then
    1.45      let
    1.46 -      val markup = Active.make_markup Markup.graphviewN {implicit = false, properties = []};
    1.47 -      val ((bg1, bg2), en) = YXML.output_markup_elem markup;
    1.48 -      val graph_yxml = YXML.string_of_body (encode_graphview graph);
    1.49 -    in writeln ("See " ^ bg1 ^ graph_yxml ^ bg2 ^ "graphview" ^ en) end
    1.50 +      val (markup, body) =
    1.51 +        if is_browser () then (Markup.browserN, encode_browser graph)
    1.52 +        else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph));
    1.53 +      val ((bg1, bg2), en) =
    1.54 +        YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
    1.55 +    in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
    1.56    else
    1.57      let
    1.58 -      val browser =
    1.59 -        (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
    1.60 -          SOME m => m = browserN
    1.61 -        | NONE => true);
    1.62        val (write, tool) =
    1.63 -        if browser then (write_graph_browser, "browser")
    1.64 +        if is_browser () then (write_graph_browser, "browser")
    1.65          else (write_graph_graphview, "graphview");
    1.66  
    1.67        val _ = writeln "Displaying graph ...";