src/Pure/General/graph_display.ML

for graph display, prefer graph data structure over list with dependencies;
pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes

(*  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 graph = string list * node Graph.T
  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

(* abstract graph representation *)

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

type graph = string list * node Graph.T;
  (*partial explicit order in left argument*)

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

fun session_node {name: string, unfold: bool, directory: string, path: string} =
  {name = name, content = [], unfold = unfold, directory = directory, path = path};


(* 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 *)

fun encode_browser ((keys, gr) : graph) =
  fold_rev (update (op =)) (Graph.keys gr) keys
  |> map (fn key => case Graph.get_node gr key of {name, unfold, content, directory, path} =>
    "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
    path ^ "\" > " ^ space_implode " " (map quote (Graph.immediate_succs gr key)) ^ " ;")
  |> cat_lines;

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


val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;

fun encode_graphview ((_, gr): graph) =
  gr
  |> Graph.map (fn _ => fn {name, content, ...} => (name, content))
  |> let open XML.Encode in Graph.encode string (pair string encode_content) end;


(* display graph *)

fun display_graph 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_graphview 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;