# HG changeset patch
# User wenzelm
# Date 1289501887 -3600
# Node ID da2c56aaaa68b4f8c8826662d592c419c5dc8fda
# Parent  d695d258dfbcffdea2f3581a5a1783d60abecce5
more precise treatment of deleted nodes;

diff -r d695d258dfbc -r da2c56aaaa68 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Nov 11 18:55:17 2010 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Nov 11 19:58:07 2010 +0100
@@ -98,10 +98,12 @@
         |> Graph.default_node (name, empty_node)
         |> Graph.map_node name (fold edit_node edits))
   | edit_nodes (name, NONE) (Version nodes) =
-      Version (Graph.del_node name nodes);
+      Version (perhaps (try (Graph.del_node name)) nodes);
 
 fun put_node name node (Version nodes) =
-  Version (Graph.map_node name (K node) nodes);
+  Version (nodes
+    |> Graph.default_node (name, empty_node)
+    |> Graph.map_node name (K node));
 
 end;
 
diff -r d695d258dfbc -r da2c56aaaa68 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Nov 11 18:55:17 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Nov 11 19:58:07 2010 +0100
@@ -122,8 +122,10 @@
       val edits = snapshot()
       pending.clear
 
-      if (!edits.isEmpty || !more_edits.isEmpty)
-        session.edit_version((Some(edits) :: more_edits.toList).map((thy_name, _)))
+      val all_edits =
+        if (edits.isEmpty) more_edits.toList
+        else Some(edits) :: more_edits.toList
+      if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
     }
 
     def init()