proper low-level comparison -- heed warning by Scala compiler;
authorwenzelm
Thu, 08 Aug 2013 17:04:02 +0200
changeset 52918 038458a4d11b
parent 52909 66cc4ed9a1f2
child 52919 a2659fbb3b13
proper low-level comparison -- heed warning by Scala compiler;
src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Aug 08 14:55:01 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 08 17:04:02 2013 +0200
@@ -196,7 +196,7 @@
     def commands: Linear_Set[Command] = _commands.commands
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
-      if (new_commands eq _commands) this
+      if (new_commands eq _commands.commands) this
       else new Node(header, perspective, Node.Commands(new_commands))
 
     def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =