more precise treatment of deleted nodes;
authorwenzelm
Thu Nov 11 19:58:07 2010 +0100 (2010-11-11)
changeset 40481da2c56aaaa68
parent 40480 d695d258dfbc
child 40482 dc0d4d4a1aa1
more precise treatment of deleted nodes;
src/Pure/PIDE/document.ML
src/Tools/jEdit/src/jedit/document_model.scala
     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  
     2.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Nov 11 18:55:17 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Nov 11 19:58:07 2010 +0100
     2.3 @@ -122,8 +122,10 @@
     2.4        val edits = snapshot()
     2.5        pending.clear
     2.6  
     2.7 -      if (!edits.isEmpty || !more_edits.isEmpty)
     2.8 -        session.edit_version((Some(edits) :: more_edits.toList).map((thy_name, _)))
     2.9 +      val all_edits =
    2.10 +        if (edits.isEmpty) more_edits.toList
    2.11 +        else Some(edits) :: more_edits.toList
    2.12 +      if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
    2.13      }
    2.14  
    2.15      def init()