# HG changeset patch
# User wenzelm
# Date 1283290101 -7200
# Node ID 1261481ef5e5ed598952bb1dc518a5311463a389
# Parent  9210cf2b486909cbd42615a369074309fa62d1d7
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
Position.Id_Range convenience;

diff -r 9210cf2b4869 -r 1261481ef5e5 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/General/markup.ML	Tue Aug 31 23:28:21 2010 +0200
@@ -14,8 +14,8 @@
   val properties: Properties.T -> T -> T
   val nameN: string
   val name: string -> T -> T
+  val kindN: string
   val bindingN: string val binding: string -> T
-  val kindN: string
   val entityN: string val entity: string -> T
   val defN: string
   val refN: string
@@ -118,6 +118,7 @@
   val serialN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
+  val reportN: string val report: T
   val no_output: output * output
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
@@ -164,13 +165,12 @@
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
-val (bindingN, binding) = markup_string "binding" nameN;
-
 val kindN = "kind";
 
 
 (* formal entities *)
 
+val (bindingN, binding) = markup_string "binding" nameN;
 val (entityN, entity) = markup_string "entity" nameN;
 
 val defN = "def";
@@ -343,6 +343,8 @@
 val (promptN, prompt) = markup_elem "prompt";
 val (readyN, ready) = markup_elem "ready";
 
+val (reportN, report) = markup_elem "report";
+
 
 
 (** print mode operations **)
diff -r 9210cf2b4869 -r 1261481ef5e5 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/General/markup.scala	Tue Aug 31 23:28:21 2010 +0200
@@ -69,6 +69,7 @@
 
   /* formal entities */
 
+  val BINDING = "binding"
   val ENTITY = "entity"
   val DEF = "def"
   val REF = "ref"
diff -r 9210cf2b4869 -r 1261481ef5e5 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/General/position.ML	Tue Aug 31 23:28:21 2010 +0200
@@ -27,6 +27,7 @@
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
   val default_properties: T -> Properties.T -> Properties.T
+  val report_markup: T -> Markup.T
   val report_text: Markup.T -> T -> string -> unit
   val report: Markup.T -> T -> unit
   val str_of: T -> string
@@ -125,6 +126,8 @@
   if exists (member (op =) Markup.position_properties o #1) props then props
   else properties_of default @ props;
 
+fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
+
 fun report_text markup (pos as Pos (count, _)) txt =
   if invalid_count count then ()
   else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
diff -r 9210cf2b4869 -r 1261481ef5e5 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/General/position.scala	Tue Aug 31 23:28:21 2010 +0200
@@ -29,5 +29,14 @@
       }
   }
 
+  object Id_Range
+  {
+    def unapply(pos: T): Option[(Long, Text.Range)] =
+      (pos, pos) match {
+        case (Id(id), Range(range)) => Some((id, range))
+        case _ => None
+      }
+  }
+
   def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
 }
diff -r 9210cf2b4869 -r 1261481ef5e5 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 31 23:28:21 2010 +0200
@@ -48,8 +48,8 @@
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
-              case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
-              if Position.Id.unapply(atts) == Some(command.id) =>
+              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
+              if id == command.id =>
                 val props = Position.purge(atts)
                 val info =
                   Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
@@ -59,7 +59,9 @@
         case XML.Elem(Markup(name, atts), body) =>
           atts match {
             case Markup.Serial(i) =>
-              add_result(i, XML.Elem(Markup(name, Position.purge(atts)), body))
+              val result = XML.Elem(Markup(name, Position.purge(atts)), body)
+              (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
+                (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }
diff -r 9210cf2b4869 -r 1261481ef5e5 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Tue Aug 31 22:03:55 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Tue Aug 31 23:28:21 2010 +0200
@@ -54,6 +54,22 @@
     else if (markup.exists(_.name == Markup.FINISHED)) Finished
     else Unprocessed
   }
+
+
+  /* reported positions */
+
+  def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
+  {
+    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
+      tree match {
+        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
+        if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
+          id == command_id => body.foldLeft(set + range)(reported)
+        case XML.Elem(_, body) => body.foldLeft(set)(reported)
+        case XML.Text(_) => set
+      }
+    reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
+  }
 }