# HG changeset patch
# User wenzelm
# Date 1274821393 -7200
# Node ID 8e51fc35d59f2e7b7b8158f77ed9b76ec9277795
# Parent  5df087c6ce94962144b0a34e6df4a7c765cfe30f
eliminated obsolete priority message from Isabelle_Process protocol;

diff -r 5df087c6ce94 -r 8e51fc35d59f src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Tue May 25 22:21:31 2010 +0200
+++ b/src/Pure/General/markup.scala	Tue May 25 23:03:13 2010 +0200
@@ -193,7 +193,6 @@
   val INIT = "init"
   val STATUS = "status"
   val WRITELN = "writeln"
-  val PRIORITY = "priority"
   val TRACING = "tracing"
   val WARNING = "warning"
   val ERROR = "error"
diff -r 5df087c6ce94 -r 8e51fc35d59f src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue May 25 22:21:31 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue May 25 23:03:13 2010 +0200
@@ -73,11 +73,11 @@
   in
     Output.status_fn   := standard_message out_stream "B";
     Output.writeln_fn  := standard_message out_stream "C";
-    Output.priority_fn := standard_message out_stream "D";
-    Output.tracing_fn  := standard_message out_stream "E";
-    Output.warning_fn  := standard_message out_stream "F";
-    Output.error_fn    := standard_message out_stream "G";
-    Output.debug_fn    := standard_message out_stream "H";
+    Output.tracing_fn  := standard_message out_stream "D";
+    Output.warning_fn  := standard_message out_stream "E";
+    Output.error_fn    := standard_message out_stream "F";
+    Output.debug_fn    := standard_message out_stream "G";
+    Output.priority_fn := ! Output.writeln_fn;
     Output.prompt_fn   := ignore;
     out_stream
   end;
diff -r 5df087c6ce94 -r 8e51fc35d59f src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue May 25 22:21:31 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Tue May 25 23:03:13 2010 +0200
@@ -32,7 +32,6 @@
     val INIT = Value("INIT")
     val STATUS = Value("STATUS")
     val WRITELN = Value("WRITELN")
-    val PRIORITY = Value("PRIORITY")
     val TRACING = Value("TRACING")
     val WARNING = Value("WARNING")
     val ERROR = Value("ERROR")
@@ -42,11 +41,10 @@
       ('A' : Int) -> Kind.INIT,
       ('B' : Int) -> Kind.STATUS,
       ('C' : Int) -> Kind.WRITELN,
-      ('D' : Int) -> Kind.PRIORITY,
-      ('E' : Int) -> Kind.TRACING,
-      ('F' : Int) -> Kind.WARNING,
-      ('G' : Int) -> Kind.ERROR,
-      ('H' : Int) -> Kind.DEBUG,
+      ('D' : Int) -> Kind.TRACING,
+      ('E' : Int) -> Kind.WARNING,
+      ('F' : Int) -> Kind.ERROR,
+      ('G' : Int) -> Kind.DEBUG,
       ('0' : Int) -> Kind.SYSTEM,
       ('1' : Int) -> Kind.STDIN,
       ('2' : Int) -> Kind.STDOUT,
@@ -57,7 +55,6 @@
       Kind.INIT -> Markup.INIT,
       Kind.STATUS -> Markup.STATUS,
       Kind.WRITELN -> Markup.WRITELN,
-      Kind.PRIORITY -> Markup.PRIORITY,
       Kind.TRACING -> Markup.TRACING,
       Kind.WARNING -> Markup.WARNING,
       Kind.ERROR -> Markup.ERROR,
diff -r 5df087c6ce94 -r 8e51fc35d59f src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Tue May 25 22:21:31 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Tue May 25 23:03:13 2010 +0200
@@ -3,7 +3,6 @@
 .message { margin-top: 0.3ex; background-color: #F0F0F0; }
 
 .writeln { }
-.priority { }
 .tracing { background-color: #EAF8FF; }
 .warning { background-color: #EEE8AA; }
 .error { background-color: #FFC1C1; }