src/Pure/PIDE/document.ML
changeset 44202 44c4ae5c5ce2
parent 44201 6429ab1b6883
child 44222 9d5ef6cd4ee1
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 15 21:05:30 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 15 21:54:32 2011 +0200
     1.3 @@ -87,7 +87,8 @@
     1.4  
     1.5  fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
     1.6  fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes;
     1.7 -fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f;
     1.8 +fun default_node name = Graph.default_node (name, empty_node);
     1.9 +fun update_node name f = default_node name #> Graph.map_node name f;
    1.10  
    1.11  
    1.12  (* node edits and associated executions *)
    1.13 @@ -126,27 +127,36 @@
    1.14  
    1.15  fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names);
    1.16  
    1.17 +fun touch_descendants name nodes =
    1.18 +  fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE)))
    1.19 +    (Graph.all_succs nodes [name]) nodes;
    1.20 +
    1.21  fun edit_nodes (name, node_edit) (Version nodes) =
    1.22    Version
    1.23 -    (case node_edit of
    1.24 -      Clear => update_node name clear_node nodes
    1.25 -    | Edits edits => update_node name (edit_node edits) nodes
    1.26 -    | Header header =>
    1.27 -        let
    1.28 -          val node = get_node nodes name;
    1.29 -          val nodes' = Graph.new_node (name, node) (remove_node name nodes);
    1.30 -          val parents =
    1.31 -            (case header of Exn.Res (_, parents, _) => parents | _ => [])
    1.32 -            |> filter (can (Graph.get_node nodes'));
    1.33 -          val (header', nodes'') =
    1.34 -            (header, Graph.add_deps_acyclic (name, parents) nodes')
    1.35 -              handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes');
    1.36 -        in Graph.map_node name (set_header header') nodes'' end);
    1.37 +    (touch_descendants name
    1.38 +      (case node_edit of
    1.39 +        Clear => update_node name clear_node nodes
    1.40 +      | Edits edits =>
    1.41 +          nodes
    1.42 +          |> update_node name (edit_node edits)
    1.43 +      | Header header =>
    1.44 +          let
    1.45 +            val node = get_node nodes name;
    1.46 +            val nodes' = Graph.new_node (name, node) (remove_node name nodes);
    1.47 +            val parents =
    1.48 +              (case header of Exn.Res (_, parents, _) => parents | _ => [])
    1.49 +              |> filter (can (Graph.get_node nodes'));
    1.50 +            val (header', nodes'') =
    1.51 +              (header, Graph.add_deps_acyclic (name, parents) nodes')
    1.52 +                handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes')
    1.53 +                  | Graph.UNDEF d => (Exn.Exn (ERROR ("Undefined theory entry: " ^ quote d)), nodes')
    1.54 +          in
    1.55 +            nodes''
    1.56 +            |> Graph.map_node name (set_header header')
    1.57 +          end));
    1.58  
    1.59 -fun put_node (name, node) (Version nodes) =
    1.60 -  Version (nodes
    1.61 -    |> Graph.default_node (name, empty_node)
    1.62 -    |> Graph.map_node name (K node));
    1.63 +fun def_node name (Version nodes) = Version (default_node name nodes);
    1.64 +fun put_node (name, node) (Version nodes) = Version (update_node name (K node) nodes);
    1.65  
    1.66  end;
    1.67  
    1.68 @@ -321,7 +331,10 @@
    1.69    let
    1.70      val old_version = the_version state old_id;
    1.71      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
    1.72 -    val new_version = fold edit_nodes edits old_version;
    1.73 +    val new_version =
    1.74 +      old_version
    1.75 +      |> fold (def_node o #1) edits
    1.76 +      |> fold edit_nodes edits;
    1.77  
    1.78      val updates =
    1.79        nodes_of new_version |> Graph.schedule