touch descendants of edited nodes;
authorwenzelm
Mon Aug 15 21:54:32 2011 +0200 (2011-08-15)
changeset 4420244c4ae5c5ce2
parent 44201 6429ab1b6883
child 44203 77881904ee91
touch descendants of edited nodes;
more precise handling of Graph exceptions;
src/Pure/General/graph.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/General/graph.ML	Mon Aug 15 21:05:30 2011 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Mon Aug 15 21:54:32 2011 +0200
     1.3 @@ -35,19 +35,19 @@
     1.4    val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
     1.5    val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
     1.6    val is_edge: 'a T -> key * key -> bool
     1.7 -  val add_edge: key * key -> 'a T -> 'a T
     1.8 -  val del_edge: key * key -> 'a T -> 'a T
     1.9 +  val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    1.10 +  val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
    1.11    val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
    1.12    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
    1.13      'a T * 'a T -> 'a T                                               (*exception DUP*)
    1.14    val irreducible_paths: 'a T -> key * key -> key list list
    1.15    val all_paths: 'a T -> key * key -> key list list
    1.16    exception CYCLES of key list list
    1.17 -  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
    1.18 -  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
    1.19 +  val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
    1.20 +  val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
    1.21    val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
    1.22    val topological_order: 'a T -> key list
    1.23 -  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
    1.24 +  val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
    1.25    val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
    1.26    exception DEP of key * key
    1.27    val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
     2.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 15 21:05:30 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 21:54:32 2011 +0200
     2.3 @@ -87,7 +87,8 @@
     2.4  
     2.5  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
     2.6  fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
     2.7 -fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f;
     2.8 +fun default_node name = Graph.default_node (name, empty_node);
     2.9 +fun update_node name f = default_node name #> Graph.map_node name f;
    2.10  
    2.11  
    2.12  (* node edits and associated executions *)
    2.13 @@ -126,27 +127,36 @@
    2.14  
    2.15  fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
    2.16  
    2.17 +fun touch_descendants name nodes =
    2.18 +  fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE)))
    2.19 +    (Graph.all_succs nodes [name]) nodes;
    2.20 +
    2.21  fun edit_nodes (name, node_edit) (Version nodes) =
    2.22    Version
    2.23 -    (case node_edit of
    2.24 -      Clear => update_node name clear_node nodes
    2.25 -    | Edits edits => update_node name (edit_node edits) nodes
    2.26 -    | Header header =>
    2.27 -        let
    2.28 -          val node = get_node nodes name;
    2.29 -          val nodes' = Graph.new_node (name, node) (remove_node name nodes);
    2.30 -          val parents =
    2.31 -            (case header of Exn.Res (_, parents, _) => parents | _ => [])
    2.32 -            |> filter (can (Graph.get_node nodes'));
    2.33 -          val (header', nodes'') =
    2.34 -            (header, Graph.add_deps_acyclic (name, parents) nodes')
    2.35 -              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
    2.36 -        in Graph.map_node name (set_header header') nodes'' end);
    2.37 +    (touch_descendants name
    2.38 +      (case node_edit of
    2.39 +        Clear => update_node name clear_node nodes
    2.40 +      | Edits edits =>
    2.41 +          nodes
    2.42 +          |> update_node name (edit_node edits)
    2.43 +      | Header header =>
    2.44 +          let
    2.45 +            val node = get_node nodes name;
    2.46 +            val nodes' = Graph.new_node (name, node) (remove_node name nodes);
    2.47 +            val parents =
    2.48 +              (case header of Exn.Res (_, parents, _) => parents | _ => [])
    2.49 +              |> filter (can (Graph.get_node nodes'));
    2.50 +            val (header', nodes'') =
    2.51 +              (header, Graph.add_deps_acyclic (name, parents) nodes')
    2.52 +                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes')
    2.53 +                  | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes')
    2.54 +          in
    2.55 +            nodes''
    2.56 +            |> Graph.map_node name (set_header header')
    2.57 +          end));
    2.58  
    2.59 -fun put_node (name, node) (Version nodes) =
    2.60 -  Version (nodes
    2.61 -    |> Graph.default_node (name, empty_node)
    2.62 -    |> Graph.map_node name (K node));
    2.63 +fun def_node name (Version nodes) = Version (default_node name nodes);
    2.64 +fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes);
    2.65  
    2.66  end;
    2.67  
    2.68 @@ -321,7 +331,10 @@
    2.69    let
    2.70      val old_version = the_version state old_id;
    2.71      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
    2.72 -    val new_version = fold edit_nodes edits old_version;
    2.73 +    val new_version =
    2.74 +      old_version
    2.75 +      |> fold (def_node o #1) edits
    2.76 +      |> fold edit_nodes edits;
    2.77  
    2.78      val updates =
    2.79        nodes_of new_version |> Graph.schedule