# HG changeset patch
# User wenzelm
# Date 1375974242 -7200
# Node ID 038458a4d11b2d5e62d87e4efe84f8c4ae25f25f
# Parent  66cc4ed9a1f2d7259fd405930f0722fba42bd12f
proper low-level comparison -- heed warning by Scala compiler;

diff -r 66cc4ed9a1f2 -r 038458a4d11b 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)] =