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