tuned;
authorwenzelm
Sat, 02 Jul 2011 20:22:02 +0200
changeset 43642 9ef5479da29f
parent 43641 081e009549dc
child 43643 474745a899ea
tuned;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Jul 02 19:22:06 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Jul 02 20:22:02 2011 +0200
@@ -80,10 +80,10 @@
     NONE => entries
   | SOME next => Entries.update (next, NONE) entries);
 
-fun edit_node (hook, SOME id2) (Node entries) =
-      Node (Entries.insert_after hook (id2, NONE) entries)
-  | edit_node (hook, NONE) (Node entries) =
-      Node (entries |> Entries.delete_after hook |> reset_after hook);
+fun edit_node (id, SOME id2) (Node entries) =
+      Node (Entries.insert_after id (id2, NONE) entries)
+  | edit_node (id, NONE) (Node entries) =
+      Node (entries |> Entries.delete_after id |> reset_after id);
 
 
 (* version operations *)