--- a/src/Pure/PIDE/command.scala Sat May 29 20:34:28 2010 +0200
+++ b/src/Pure/PIDE/command.scala Sat May 29 20:49:04 2010 +0200
@@ -80,7 +80,7 @@
assigned = true // single assignment
reply(())
- case bad => System.err.println("command accumulator: ignoring bad message " + bad)
+ case bad => System.err.println("Command accumulator: ignoring bad message " + bad)
}
}
}
--- a/src/Pure/PIDE/markup_node.scala Sat May 29 20:34:28 2010 +0200
+++ b/src/Pure/PIDE/markup_node.scala Sat May 29 20:49:04 2010 +0200
@@ -48,7 +48,7 @@
else copy(branches = new_branches)
}
else {
- System.err.println("ignored nonfitting markup: " + new_node)
+ System.err.println("Ignored nonfitting markup: " + new_node)
this
}
}
--- a/src/Pure/PIDE/state.scala Sat May 29 20:34:28 2010 +0200
+++ b/src/Pure/PIDE/state.scala Sat May 29 20:49:04 2010 +0200
@@ -112,7 +112,7 @@
case _ => state
}
case _ =>
- System.err.println("ignored status report: " + elem)
+ System.err.println("Ignored status report: " + elem)
state
})
case _ => add_result(message)