src/Pure/General/graph_display.ML
author wenzelm
Tue Sep 25 22:36:06 2012 +0200 (2012-09-25 ago)
changeset 49566 66cbf8bb4693
parent 49565 ea4308b7ef0f
child 49570 2265456f6131
permissions -rw-r--r--
basic integration of graphview into document model;
added Graph_Dockable;
updated Isabelle/jEdit authors and dependencies etc.;
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@49566
    16
  val graphview_reportN: 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@49566
    36
val graphview_reportN = "graphview_report";
wenzelm@49565
    37
wenzelm@49565
    38
fun write_graph_browser path (graph: graph) =
wenzelm@49561
    39
  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
wenzelm@49561
    40
    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
wenzelm@49561
    41
    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph));
wenzelm@49561
    42
wenzelm@49561
    43
wenzelm@49565
    44
val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
wenzelm@49565
    45
wenzelm@49565
    46
fun encode_graphview (graph: graph) =
wenzelm@49565
    47
  Graph.empty
wenzelm@49565
    48
  |> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph
wenzelm@49565
    49
  |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
wenzelm@49565
    50
  |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
wenzelm@49565
    51
wenzelm@49565
    52
fun write_graph_graphview path graph =
wenzelm@49565
    53
  File.write path (YXML.string_of_body (encode_graphview graph));
wenzelm@49565
    54
wenzelm@49565
    55
wenzelm@49561
    56
(* display graph *)
wenzelm@49561
    57
wenzelm@49561
    58
fun display_graph graph =
wenzelm@49566
    59
  if print_mode_active graphview_reportN then
wenzelm@49566
    60
    Output.report
wenzelm@49566
    61
      (YXML.string_of (XML.Elem ((Isabelle_Markup.graphviewN, []), encode_graphview graph)))
wenzelm@49566
    62
  else
wenzelm@49566
    63
    let
wenzelm@49566
    64
      val browser =
wenzelm@49566
    65
        (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
wenzelm@49566
    66
          SOME m => m = browserN
wenzelm@49566
    67
        | NONE => true);
wenzelm@49566
    68
      val (write, tool) =
wenzelm@49566
    69
        if browser then (write_graph_browser, "browser")
wenzelm@49566
    70
        else (write_graph_graphview, "graphview");
wenzelm@49565
    71
wenzelm@49566
    72
      val _ = writeln "Displaying graph ...";
wenzelm@49566
    73
      val path = Isabelle_System.create_tmp_path "graph" "";
wenzelm@49566
    74
      val _ = write path graph;
wenzelm@49566
    75
      val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
wenzelm@49566
    76
    in () end;
wenzelm@49561
    77
wenzelm@49561
    78
end;
wenzelm@49561
    79