# HG changeset patch
# User wenzelm
# Date 1275158944 -7200
# Node ID 2b4e52ecf6fcfdf9fc59aabd25401cd034900ddc
# Parent  b78ff6b4f4b3060611f91d007a600dae71e1bcf7
tuned messages;

diff -r b78ff6b4f4b3 -r 2b4e52ecf6fc src/Pure/PIDE/command.scala
--- 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)
       }
     }
   }
diff -r b78ff6b4f4b3 -r 2b4e52ecf6fc src/Pure/PIDE/markup_node.scala
--- 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
     }
   }
diff -r b78ff6b4f4b3 -r 2b4e52ecf6fc src/Pure/PIDE/state.scala
--- 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)