diff -r 67c20ce71d22 -r b9d69001824e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Sep 19 20:47:11 2015 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Sep 19 21:07:37 2015 +0200
@@ -150,12 +150,6 @@
       else Some(new State(other_command, Nil, Results.empty, markups1))
     }
 
-    def eq_content(other: State): Boolean =
-      command.source == other.command.source &&
-      status == other.status &&
-      results == other.results &&
-      markups == other.markups
-
     private def add_status(st: Markup): State =
       copy(status = st :: status)