# HG changeset patch
# User wenzelm
# Date 1373533763 -7200
# Node ID 067f1f950dc89ca0efe2ab71857d45ffbf7c5ce4
# Parent  7a0935571a23bf82a78c9f88f264913c609e01e0
tuned -- refrain from odd optimization;

diff -r 7a0935571a23 -r 067f1f950dc8 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jul 11 10:43:53 2013 +0200
+++ b/src/Pure/PIDE/document.ML	Thu Jul 11 11:09:23 2013 +0200
@@ -217,7 +217,7 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version id -> document content*)
-  commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named span*)
+  commands: (string * Token.T list lazy) Inttab.table,  (*command id -> named command span*)
   execution: execution}  (*current execution process*)
 with
 
@@ -517,8 +517,7 @@
                       |> assign_update_apply assigned_execs
                       |> entries_stable (assign_update_null updated_execs)
                       |> set_result result;
-                    val assigned_node =
-                      if assign_update_null assigned_execs then NONE else SOME (name, node');
+                    val assigned_node = SOME (name, node');
                     val result_changed = changed_result node0 node';
                   in
                     ((assign_update_result assigned_execs, assigned_node, result_changed), node')