src/Pure/PIDE/command.scala

     {
       val markups1 = markups.redirect(other_command.id)
       if (markups1.is_empty) None
       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)
 
     private def add_markup(