# HG changeset patch
# User wenzelm
# Date 1284731471 -7200
# Node ID 1c294d150ded9fea8ee467a7c871ce0156e27ba9
# Parent  c5ece2a7a86eee42f377176babb6c4672355593c
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;

diff -r c5ece2a7a86e -r 1c294d150ded src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Sep 16 15:37:12 2010 +0200
+++ b/src/Pure/General/markup.ML	Fri Sep 17 15:51:11 2010 +0200
@@ -30,7 +30,6 @@
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
-  val locationN: string val location: T
   val indentN: string
   val blockN: string val block: int -> T
   val widthN: string
@@ -120,6 +119,7 @@
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val reportN: string val report: T
+  val no_reportN: string val no_report: T
   val badN: string val bad: T
   val no_output: output * output
   val default_output: T -> output * output
@@ -194,7 +194,6 @@
 val position_properties = [lineN, columnN, offsetN] @ position_properties';
 
 val (positionN, position) = markup_elem "position";
-val (locationN, location) = markup_elem "location";
 
 
 (* pretty printing *)
@@ -348,6 +347,7 @@
 val (readyN, ready) = markup_elem "ready";
 
 val (reportN, report) = markup_elem "report";
+val (no_reportN, no_report) = markup_elem "no_report";
 
 val (badN, bad) = markup_elem "bad";
 
diff -r c5ece2a7a86e -r 1c294d150ded src/Pure/General/markup.scala
--- 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)
diff -r c5ece2a7a86e -r 1c294d150ded src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Thu Sep 16 15:37:12 2010 +0200
+++ b/src/Pure/Isar/runtime.ML	Fri Sep 17 15:51:11 2010 +0200
@@ -61,7 +61,7 @@
           Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
         | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
         | EXCURSION_FAIL (exn, loc) =>
-            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
+            map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
         | TERMINATE => ["Exit"]
         | TimeLimit.TimeOut => ["Timeout"]
         | TOPLEVEL_ERROR => ["Error"]
diff -r c5ece2a7a86e -r 1c294d150ded src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Sep 16 15:37:12 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 15:51:11 2010 +0200
@@ -121,7 +121,7 @@
     fun message {message = msg, hard, location = loc, context = _} =
       let
         val txt =
-          Markup.markup Markup.location
+          Markup.markup Markup.no_report
             ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
           Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
           Markup.markup (Position.report_markup (offset_position_of loc)) "";
diff -r c5ece2a7a86e -r 1c294d150ded src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Thu Sep 16 15:37:12 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 17 15:51:11 2010 +0200
@@ -56,10 +56,16 @@
   }
 
 
+  /* messages */
+
+  def clean_message(body: XML.Body): XML.Body =
+    body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
+      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
+
+
   /* reported positions */
 
   private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
-  private val exclude_pos = Set(Markup.LOCATION)
 
   private def is_state(msg: XML.Tree): Boolean =
     msg match {
@@ -75,8 +81,7 @@
         if include_pos(name) && id == command.id =>
           val range = command.decode(raw_range).restrict(command.range)
           body.foldLeft(if (range.is_singularity) set else set + range)(reported)
-        case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
-          body.foldLeft(set)(reported)
+        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(reported)
         case _ => set
       }
     val set = reported(Set.empty, message)
diff -r c5ece2a7a86e -r 1c294d150ded src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Sep 16 15:37:12 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Fri Sep 17 15:51:11 2010 +0200
@@ -100,7 +100,8 @@
     if (pid.isEmpty && kind == Markup.INIT)
       pid = props.find(_._1 == Markup.PID).map(_._1)
 
-    xml_cache.cache_tree(XML.Elem(Markup(kind, props), body))((message: XML.Tree) =>
+    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
+    xml_cache.cache_tree(msg)((message: XML.Tree) =>
       receiver ! new Result(message.asInstanceOf[XML.Elem]))
   }
 
diff -r c5ece2a7a86e -r 1c294d150ded src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
--- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Thu Sep 16 15:37:12 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 15:51:11 2010 +0200
@@ -8,8 +8,6 @@
 .error { background-color: #FFC1C1; }
 .debug { background-color: #FFE4E1; }
 
-.location { display: none; }
-
 .hilite { background-color: #FFFACD; }
 
 .keyword { font-weight: bold; color: #009966; }