--- 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;
--- 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()