src/Pure/General/graph_display.ML
changeset 59207 6b030dc97a4f
parent 57032 cf570f3ecdc1
child 59208 2486d625878b
     1.1 --- a/src/Pure/General/graph_display.ML	Wed Dec 31 14:08:50 2014 +0100
     1.2 +++ b/src/Pure/General/graph_display.ML	Wed Dec 31 14:13:11 2014 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature GRAPH_DISPLAY =
     1.5  sig
     1.6    type node =
     1.7 -   {name: string, ID: string, dir: string, unfold: bool,
     1.8 +   {name: string, ident: string, directory: string, unfold: bool,
     1.9      path: string, parents: string list, content: Pretty.T list}
    1.10    type graph = node list
    1.11    val write_graph_browser: Path.T -> graph -> unit
    1.12 @@ -23,7 +23,7 @@
    1.13  (* external graph representation *)
    1.14  
    1.15  type node =
    1.16 - {name: string, ID: string, dir: string, unfold: bool,
    1.17 + {name: string, ident: string, directory: string, unfold: bool,
    1.18    path: string, parents: string list, content: Pretty.T list};
    1.19  
    1.20  type graph = node list;
    1.21 @@ -44,8 +44,8 @@
    1.22  (* encode graph *)
    1.23  
    1.24  fun encode_browser (graph: graph) =
    1.25 -  cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    1.26 -    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.27 +  cat_lines (map (fn {name, ident, directory, unfold, path, parents, ...} =>
    1.28 +    "\"" ^ name ^ "\" \"" ^ ident ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
    1.29      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
    1.30  
    1.31  fun write_graph_browser path graph = File.write path (encode_browser graph);
    1.32 @@ -55,8 +55,8 @@
    1.33  
    1.34  fun encode_graphview (graph: graph) =
    1.35    Graph.empty
    1.36 -  |> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph
    1.37 -  |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
    1.38 +  |> fold (fn {ident, name, content, ...} => Graph.new_node (ident, (name, content))) graph
    1.39 +  |> fold (fn {ident = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
    1.40    |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
    1.41  
    1.42