# HG changeset patch
# User wenzelm
# Date 1396366187 -7200
# Node ID ecbdfe30bf7f625d0b63ec1d1e0349cc1f8860d0
# Parent  abdc524db8b42f41e67bd73c523f56bbd9fe725f
unused;

diff -r abdc524db8b4 -r ecbdfe30bf7f src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 01 17:26:32 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Apr 01 17:29:47 2014 +0200
@@ -48,10 +48,6 @@
     forks: Int,
     runs: Int)
   {
-    def + (that: Status): Status =
-      Status(touched || that.touched, accepted || that.accepted, failed || that.failed,
-        forks + that.forks, runs + that.runs)
-
     def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
     def is_running: Boolean = runs != 0
     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0