--- a/src/Pure/General/markup.scala Thu Sep 16 15:37:12 2010 +0200
+++ b/src/Pure/General/markup.scala Fri Sep 17 15:51:11 2010 +0200
@@ -90,7 +90,6 @@
Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
val POSITION = "position"
- val LOCATION = "location"
/* pretty printing */
@@ -236,7 +235,6 @@
val INIT = "init"
val STATUS = "status"
- val REPORT = "report"
val WRITELN = "writeln"
val TRACING = "tracing"
val WARNING = "warning"
@@ -249,6 +247,9 @@
val SIGNAL = "signal"
val EXIT = "exit"
+ val REPORT = "report"
+ val NO_REPORT = "no_report"
+
val BAD = "bad"
val Ready = Markup("ready", Nil)