src/Pure/General/graph_display.ML

clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
tuned;

(*  Title:      Pure/General/graph_display.ML
    Author:     Makarius

Generic graph display, with browser and graphview backends.
*)

signature GRAPH_DISPLAY =
sig
  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 eq_entry: entry * entry -> bool
  type graph = entry list
  val sort_graph: graph -> graph
  val write_graph_browser: Path.T -> graph -> unit
  val browserN: string
  val graphviewN: string
  val active_graphN: string
  val display_graph: graph -> unit
end;

structure Graph_Display: GRAPH_DISPLAY =
struct

(* type node *)

datatype node =
  Node of {name: string, content: Pretty.T list, unfold: bool, directory: string, path: string};

fun content_node name content =
  Node {name = name, content = content, unfold = true, directory = "", path = ""};

fun session_node {name, unfold, directory, path} =
  Node {name = name, content = [], unfold = unfold, directory = directory, path = path};


(* type graph *)

type entry = (string * node) * string list;
val eq_entry: entry * entry -> bool = op = o apply2 (#1 o #1);

type graph = entry list;

structure Aux_Graph =
  Graph(type key = string * string val ord = prod_ord string_ord string_ord);

fun sort_graph (graph: graph) =
  let
    val ident_names =
      fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident)))
        graph Symtab.empty;
    val the_key = the o Symtab.lookup ident_names;
    val G =
      Aux_Graph.empty
      |> fold (fn ((ident, node), _) => Aux_Graph.new_node (the_key ident, node)) graph
      |> fold (fn ((ident, _), parents) =>
          fold (fn parent => Aux_Graph.add_edge (the_key parent, the_key ident)) parents) graph
  in
    Aux_Graph.topological_order G |> map (fn key =>
      let val (_, (node, (preds, _))) = Aux_Graph.get_entry G key
      in ((#2 key, node), map #2 (Aux_Graph.Keys.dest preds)) end)
  end;


(* print modes *)

val browserN = "browser";
val graphviewN = "graphview";
val active_graphN = "active_graph";

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 =
  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;

fun write_graph_browser path graph =
  File.write path (encode_browser graph);


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;


(* display graph *)

val display_graph =
  sort_graph #> (fn graph =>
    if print_mode_active active_graphN then
      let
        val (markup, body) =
          if is_browser () then (Markup.browserN, encode_browser graph)
          else (Markup.graphviewN, YXML.string_of_body (encode_graph graph));
        val ((bg1, bg2), en) =
          YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
      in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
    else
      let
        val _ = writeln "Displaying graph ...";
        val path = Isabelle_System.create_tmp_path "graph" "";
        val _ = write_graph_browser path graph;
        val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
      in () end);

end;