--- 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"
--- 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;
--- 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,
--- 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; }