src/Pure/PIDE/document.ML
changeset 50862 5fc8b83322f5
parent 50201 c26369c9eda6
child 51268 fcc4b89a600d
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Jan 13 15:04:55 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Jan 13 19:45:32 2013 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4    perspective: perspective,  (*visible commands, last*)
     1.5    entries: (exec_id * exec) option Entries.T * bool,  (*command entries with excecutions, stable*)
     1.6    result: exec option}  (*result of last execution*)
     1.7 -and version = Version of node Graph.T  (*development graph wrt. static imports*)
     1.8 +and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
     1.9  with
    1.10  
    1.11  fun make_node (header, perspective, entries, result) =
    1.12 @@ -134,9 +134,10 @@
    1.13  fun set_result result =
    1.14    map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
    1.15  
    1.16 -fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    1.17 -fun default_node name = Graph.default_node (name, empty_node);
    1.18 -fun update_node name f = default_node name #> Graph.map_node name f;
    1.19 +fun get_node nodes name = String_Graph.get_node nodes name
    1.20 +  handle String_Graph.UNDEF _ => empty_node;
    1.21 +fun default_node name = String_Graph.default_node (name, empty_node);
    1.22 +fun update_node name f = default_node name #> String_Graph.map_node name f;
    1.23  
    1.24  
    1.25  (* node edits and associated executions *)
    1.26 @@ -182,7 +183,7 @@
    1.27  
    1.28  (* version operations *)
    1.29  
    1.30 -val empty_version = Version Graph.empty;
    1.31 +val empty_version = Version String_Graph.empty;
    1.32  
    1.33  fun nodes_of (Version nodes) = nodes;
    1.34  val node_of = get_node o nodes_of;
    1.35 @@ -204,12 +205,12 @@
    1.36              |> default_node name
    1.37              |> fold default_node imports;
    1.38            val nodes2 = nodes1
    1.39 -            |> Graph.Keys.fold
    1.40 -                (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    1.41 +            |> String_Graph.Keys.fold
    1.42 +                (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name);
    1.43            val (nodes3, errors2) =
    1.44 -            (Graph.add_deps_acyclic (name, imports) nodes2, errors1)
    1.45 -              handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
    1.46 -        in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
    1.47 +            (String_Graph.add_deps_acyclic (name, imports) nodes2, errors1)
    1.48 +              handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
    1.49 +        in String_Graph.map_node name (set_header (master, header, errors2)) nodes3 end
    1.50      | Perspective perspective => update_node name (set_perspective perspective) nodes);
    1.51  
    1.52  fun put_node (name, node) (Version nodes) =
    1.53 @@ -294,7 +295,7 @@
    1.54      val commands' =
    1.55        (versions', Inttab.empty) |->
    1.56          Inttab.fold (fn (_, version) => nodes_of version |>
    1.57 -          Graph.fold (fn (_, (node, _)) => node |>
    1.58 +          String_Graph.fold (fn (_, (node, _)) => node |>
    1.59              iterate_entries (fn ((_, id), _) =>
    1.60                SOME o Inttab.insert (K true) (id, the_command state id))));
    1.61    in (versions', commands', execution) end);
    1.62 @@ -339,7 +340,7 @@
    1.63          {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
    1.64          (fn () =>
    1.65           (OS.Process.sleep (seconds 0.02);
    1.66 -          nodes_of (the_version state version_id) |> Graph.schedule
    1.67 +          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.68              (fn deps => fn (name, node) =>
    1.69                if not (visible_node node) andalso finished_theory node then
    1.70                  Future.value ()
    1.71 @@ -366,13 +367,13 @@
    1.72  fun make_required nodes =
    1.73    let
    1.74      val all_visible =
    1.75 -      Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
    1.76 -      |> Graph.all_preds nodes
    1.77 +      String_Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
    1.78 +      |> String_Graph.all_preds nodes
    1.79        |> map (rpair ()) |> Symtab.make;
    1.80  
    1.81      val required =
    1.82        Symtab.fold (fn (a, ()) =>
    1.83 -        exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ?
    1.84 +        exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
    1.85            Symtab.update (a, ())) all_visible Symtab.empty;
    1.86    in Symtab.defined required end;
    1.87  
    1.88 @@ -476,7 +477,7 @@
    1.89  
    1.90      val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state);
    1.91      val updated = timeit "Document.update" (fn () =>
    1.92 -      nodes |> Graph.schedule
    1.93 +      nodes |> String_Graph.schedule
    1.94          (fn deps => fn (name, node) =>
    1.95            (singleton o Future.forks)
    1.96              {name = "Document.update", group = NONE,