let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
authorwenzelm
Thu Apr 16 11:22:36 2015 +0200 (2015-04-16)
changeset 600898bd5999133d4
parent 60087 bc57cb0c5001
child 60090 75ec8fd5d2bf
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
NEWS
src/Pure/General/graph_display.ML
src/Pure/Tools/thm_deps.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/NEWS	Wed Apr 15 22:27:31 2015 +0200
     1.2 +++ b/NEWS	Thu Apr 16 11:22:36 2015 +0200
     1.3 @@ -74,10 +74,8 @@
     1.4  * Less waste of vertical space via negative line spacing (see Global
     1.5  Options / Text Area).
     1.6  
     1.7 -* Improved graphview panel (with optional output of PNG or PDF)
     1.8 -supersedes the old graph browser from 1996, but the latter remains
     1.9 -available for some time as a fall-back. The old browser is still
    1.10 -required for the massive graphs produced by 'thm_deps', for example.
    1.11 +* Improved graphview panel with optional output of PNG or PDF, for
    1.12 +display of 'thy_deps', 'locale_deps', 'class_deps' etc.
    1.13  
    1.14  * Improved scheduling for asynchronous print commands (e.g. provers
    1.15  managed by the Sledgehammer panel) wrt. ongoing document processing.
     2.1 --- a/src/Pure/General/graph_display.ML	Wed Apr 15 22:27:31 2015 +0200
     2.2 +++ b/src/Pure/General/graph_display.ML	Thu Apr 16 11:22:36 2015 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4    val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
     2.5    type entry = (string * node) * string list
     2.6    val display_graph: entry list -> unit
     2.7 +  val display_graph_old: entry list -> unit
     2.8  end;
     2.9  
    2.10  structure Graph_Display: GRAPH_DISPLAY =
    2.11 @@ -30,7 +31,9 @@
    2.12  type entry = (string * node) * string list;
    2.13  
    2.14  
    2.15 -(* encode graph *)
    2.16 +(* display graph *)
    2.17 +
    2.18 +local
    2.19  
    2.20  fun encode_node (Node {name, content, ...}) =
    2.21    (name, content) |>
    2.22 @@ -40,9 +43,22 @@
    2.23  val encode_graph =
    2.24    let open XML.Encode in list (pair (pair string encode_node) (list string)) end;
    2.25  
    2.26 +in
    2.27 +
    2.28 +fun display_graph entries =
    2.29 +  let
    2.30 +    val ((bg1, bg2), en) =
    2.31 +      YXML.output_markup_elem
    2.32 +        (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
    2.33 +  in writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en) end;
    2.34 +
    2.35 +end;
    2.36 +
    2.37  
    2.38  (* support for old browser *)
    2.39  
    2.40 +local
    2.41 +
    2.42  structure Graph =
    2.43    Graph(type key = string * string val ord = prod_ord string_ord string_ord);
    2.44  
    2.45 @@ -71,23 +87,15 @@
    2.46      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
    2.47    #> cat_lines;
    2.48  
    2.49 +in
    2.50  
    2.51 -(* display graph *)
    2.52 -
    2.53 -fun display_graph entries =
    2.54 +fun display_graph_old entries =
    2.55    let
    2.56      val ((bg1, bg2), en) =
    2.57        YXML.output_markup_elem
    2.58 -        (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
    2.59 -    val _ =
    2.60 -      writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en);
    2.61 -
    2.62 -    (*old browser*)
    2.63 -    val ((bg1, bg2), en) =
    2.64 -      YXML.output_markup_elem
    2.65          (Active.make_markup Markup.browserN {implicit = false, properties = []});
    2.66 -    val _ =
    2.67 -      writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "old graph" ^ en);
    2.68 -  in () end;
    2.69 +  in writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "graph" ^ en) end;
    2.70  
    2.71  end;
    2.72 +
    2.73 +end;
     3.1 --- a/src/Pure/Tools/thm_deps.ML	Wed Apr 15 22:27:31 2015 +0200
     3.2 +++ b/src/Pure/Tools/thm_deps.ML	Thu Apr 16 11:22:36 2015 +0200
     3.3 @@ -44,7 +44,7 @@
     3.4          else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
     3.5    in
     3.6      Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
     3.7 -    |> Graph_Display.display_graph
     3.8 +    |> Graph_Display.display_graph_old
     3.9    end;
    3.10  
    3.11  val _ =
     4.1 --- a/src/Tools/Code/code_thingol.ML	Wed Apr 15 22:27:31 2015 +0200
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Apr 16 11:22:36 2015 +0200
     4.3 @@ -946,7 +946,7 @@
     4.4      |> join_strong_conn
     4.5      |> Graph.dest
     4.6      |> map (fn ((c, cs), ds) => ((c, Graph_Display.content_node (namify cs) []), ds))
     4.7 -    |> Graph_Display.display_graph
     4.8 +    |> Graph_Display.display_graph_old
     4.9    end;
    4.10  
    4.11  local