src/Pure/PIDE/document.ML
changeset 40481 da2c56aaaa68
parent 40449 9c390868d255
child 40520 77a7b0a7d4b1
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Nov 11 18:55:17 2010 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Nov 11 19:58:07 2010 +0100
     1.3 @@ -98,10 +98,12 @@
     1.4          |> Graph.default_node (name, empty_node)
     1.5          |> Graph.map_node name (fold edit_node edits))
     1.6    | edit_nodes (name, NONE) (Version nodes) =
     1.7 -      Version (Graph.del_node name nodes);
     1.8 +      Version (perhaps (try (Graph.del_node name)) nodes);
     1.9  
    1.10  fun put_node name node (Version nodes) =
    1.11 -  Version (Graph.map_node name (K node) nodes);
    1.12 +  Version (nodes
    1.13 +    |> Graph.default_node (name, empty_node)
    1.14 +    |> Graph.map_node name (K node));
    1.15  
    1.16  end;
    1.17