src/Pure/General/graph_display.ML
author wenzelm
Wed May 21 12:03:46 2014 +0200 (2014-05-21)
changeset 57032 cf570f3ecdc1
parent 50715 8cfd585b9162
child 59207 6b030dc97a4f
permissions -rw-r--r--
incorporate isabelle.graphview into Pure.jar, which saves 20..30s build time;
discontinued pointless "isabelle graphview" command-line tool (Proof General legacy);
     1 (*  Title:      Pure/General/graph_display.ML
     2     Author:     Makarius
     3 
     4 Generic graph display, with browser and graphview backends.
     5 *)
     6 
     7 signature GRAPH_DISPLAY =
     8 sig
     9   type node =
    10    {name: string, ID: string, dir: string, unfold: bool,
    11     path: string, parents: string list, content: Pretty.T list}
    12   type graph = node list
    13   val write_graph_browser: Path.T -> graph -> unit
    14   val browserN: string
    15   val graphviewN: string
    16   val active_graphN: string
    17   val display_graph: graph -> unit
    18 end;
    19 
    20 structure Graph_Display: GRAPH_DISPLAY =
    21 struct
    22 
    23 (* external graph representation *)
    24 
    25 type node =
    26  {name: string, ID: string, dir: string, unfold: bool,
    27   path: string, parents: string list, content: Pretty.T list};
    28 
    29 type graph = node list;
    30 
    31 
    32 (* print modes *)
    33 
    34 val browserN = "browser";
    35 val graphviewN = "graphview";
    36 val active_graphN = "active_graph";
    37 
    38 fun is_browser () =
    39   (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
    40     SOME m => m = browserN
    41   | NONE => true);
    42 
    43 
    44 (* encode graph *)
    45 
    46 fun encode_browser (graph: graph) =
    47   cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    48     "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    49     path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
    50 
    51 fun write_graph_browser path graph = File.write path (encode_browser graph);
    52 
    53 
    54 val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
    55 
    56 fun encode_graphview (graph: graph) =
    57   Graph.empty
    58   |> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph
    59   |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
    60   |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
    61 
    62 
    63 (* display graph *)
    64 
    65 fun display_graph graph =
    66   if print_mode_active active_graphN then
    67     let
    68       val (markup, body) =
    69         if is_browser () then (Markup.browserN, encode_browser graph)
    70         else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph));
    71       val ((bg1, bg2), en) =
    72         YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
    73     in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
    74   else
    75     let
    76       val _ = writeln "Displaying graph ...";
    77       val path = Isabelle_System.create_tmp_path "graph" "";
    78       val _ = write_graph_browser path graph;
    79       val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
    80     in () end;
    81 
    82 end;
    83