# HG changeset patch # User wenzelm # Date 1282572793 -7200 # Node ID 03b27bd0505edcefb2834c3adb1bb76de9184836 # Parent b7647ca7de5ac1486530bfb91b615b5383b698d0 tuned; diff -r b7647ca7de5a -r 03b27bd0505e src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon Aug 23 16:07:18 2010 +0200 +++ b/src/Pure/PIDE/command.scala Mon Aug 23 16:13:13 2010 +0200 @@ -8,10 +8,6 @@ package isabelle -import scala.actors.Actor, Actor._ -import scala.collection.mutable - - object Command { /** accumulated results from prover **/ @@ -40,7 +36,7 @@ def accumulate(message: XML.Tree): Command.State = message match { - case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit checks!? + case XML.Elem(Markup(Markup.STATUS, _), body) => // FIXME explicit body check!? copy(status = (for (XML.Elem(markup, _) <- body) yield markup) ::: status) case XML.Elem(Markup(Markup.REPORT, _), msgs) => diff -r b7647ca7de5a -r 03b27bd0505e src/Tools/jEdit/src/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 16:07:18 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_model.scala Mon Aug 23 16:13:13 2010 +0200 @@ -10,7 +10,6 @@ import isabelle._ -import scala.actors.Actor, Actor._ import scala.collection.mutable import org.gjt.sp.jedit.Buffer