--- a/src/Pure/PIDE/command.scala Wed Apr 02 11:55:37 2014 +0200
+++ b/src/Pure/PIDE/command.scala Wed Apr 02 12:26:11 2014 +0200
@@ -109,13 +109,11 @@
results: Results = Results.empty,
markups: Markups = Markups.empty)
{
- /* markup */
+ lazy val protocol_status: Protocol.Status = Protocol.Status.make(status.iterator)
def markup(index: Markup_Index): Markup_Tree = markups(index)
- /* content */
-
def eq_content(other: State): Boolean =
command.source == other.command.source &&
status == other.status &&