tuned messages;
authorwenzelm
Sat, 29 May 2010 20:49:04 +0200
changeset 37189 2b4e52ecf6fc
parent 37188 b78ff6b4f4b3
child 37190 ea52509f4c42
child 37206 7f2a6f3143ad
tuned messages;
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_node.scala
src/Pure/PIDE/state.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)
       }
     }
   }
--- 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)