Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
authorwenzelm
Tue Aug 31 23:28:21 2010 +0200 (2010-08-31)
changeset 388871261481ef5e5
parent 38886 9210cf2b4869
child 38888 8248cda328de
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
Position.Id_Range convenience;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/General/position.ML
src/Pure/General/position.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/isar_document.scala
     1.1 --- a/src/Pure/General/markup.ML	Tue Aug 31 22:03:55 2010 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Tue Aug 31 23:28:21 2010 +0200
     1.3 @@ -14,8 +14,8 @@
     1.4    val properties: Properties.T -> T -> T
     1.5    val nameN: string
     1.6    val name: string -> T -> T
     1.7 +  val kindN: string
     1.8    val bindingN: string val binding: string -> T
     1.9 -  val kindN: string
    1.10    val entityN: string val entity: string -> T
    1.11    val defN: string
    1.12    val refN: string
    1.13 @@ -118,6 +118,7 @@
    1.14    val serialN: string
    1.15    val promptN: string val prompt: T
    1.16    val readyN: string val ready: T
    1.17 +  val reportN: string val report: T
    1.18    val no_output: output * output
    1.19    val default_output: T -> output * output
    1.20    val add_mode: string -> (T -> output * output) -> unit
    1.21 @@ -164,13 +165,12 @@
    1.22  val nameN = "name";
    1.23  fun name a = properties [(nameN, a)];
    1.24  
    1.25 -val (bindingN, binding) = markup_string "binding" nameN;
    1.26 -
    1.27  val kindN = "kind";
    1.28  
    1.29  
    1.30  (* formal entities *)
    1.31  
    1.32 +val (bindingN, binding) = markup_string "binding" nameN;
    1.33  val (entityN, entity) = markup_string "entity" nameN;
    1.34  
    1.35  val defN = "def";
    1.36 @@ -343,6 +343,8 @@
    1.37  val (promptN, prompt) = markup_elem "prompt";
    1.38  val (readyN, ready) = markup_elem "ready";
    1.39  
    1.40 +val (reportN, report) = markup_elem "report";
    1.41 +
    1.42  
    1.43  
    1.44  (** print mode operations **)
     2.1 --- a/src/Pure/General/markup.scala	Tue Aug 31 22:03:55 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Tue Aug 31 23:28:21 2010 +0200
     2.3 @@ -69,6 +69,7 @@
     2.4  
     2.5    /* formal entities */
     2.6  
     2.7 +  val BINDING = "binding"
     2.8    val ENTITY = "entity"
     2.9    val DEF = "def"
    2.10    val REF = "ref"
     3.1 --- a/src/Pure/General/position.ML	Tue Aug 31 22:03:55 2010 +0200
     3.2 +++ b/src/Pure/General/position.ML	Tue Aug 31 23:28:21 2010 +0200
     3.3 @@ -27,6 +27,7 @@
     3.4    val of_properties: Properties.T -> T
     3.5    val properties_of: T -> Properties.T
     3.6    val default_properties: T -> Properties.T -> Properties.T
     3.7 +  val report_markup: T -> Markup.T
     3.8    val report_text: Markup.T -> T -> string -> unit
     3.9    val report: Markup.T -> T -> unit
    3.10    val str_of: T -> string
    3.11 @@ -125,6 +126,8 @@
    3.12    if exists (member (op =) Markup.position_properties o #1) props then props
    3.13    else properties_of default @ props;
    3.14  
    3.15 +fun report_markup pos = Markup.properties (properties_of pos) Markup.report;
    3.16 +
    3.17  fun report_text markup (pos as Pos (count, _)) txt =
    3.18    if invalid_count count then ()
    3.19    else Output.report (Markup.markup (Markup.properties (properties_of pos) markup) txt);
     4.1 --- a/src/Pure/General/position.scala	Tue Aug 31 22:03:55 2010 +0200
     4.2 +++ b/src/Pure/General/position.scala	Tue Aug 31 23:28:21 2010 +0200
     4.3 @@ -29,5 +29,14 @@
     4.4        }
     4.5    }
     4.6  
     4.7 +  object Id_Range
     4.8 +  {
     4.9 +    def unapply(pos: T): Option[(Long, Text.Range)] =
    4.10 +      (pos, pos) match {
    4.11 +        case (Id(id), Range(range)) => Some((id, range))
    4.12 +        case _ => None
    4.13 +      }
    4.14 +  }
    4.15 +
    4.16    def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
    4.17  }
     5.1 --- a/src/Pure/PIDE/command.scala	Tue Aug 31 22:03:55 2010 +0200
     5.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 31 23:28:21 2010 +0200
     5.3 @@ -48,8 +48,8 @@
     5.4          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
     5.5            (this /: msgs)((state, msg) =>
     5.6              msg match {
     5.7 -              case XML.Elem(Markup(name, atts @ Position.Range(range)), args)
     5.8 -              if Position.Id.unapply(atts) == Some(command.id) =>
     5.9 +              case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
    5.10 +              if id == command.id =>
    5.11                  val props = Position.purge(atts)
    5.12                  val info =
    5.13                    Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
    5.14 @@ -59,7 +59,9 @@
    5.15          case XML.Elem(Markup(name, atts), body) =>
    5.16            atts match {
    5.17              case Markup.Serial(i) =>
    5.18 -              add_result(i, XML.Elem(Markup(name, Position.purge(atts)), body))
    5.19 +              val result = XML.Elem(Markup(name, Position.purge(atts)), body)
    5.20 +              (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
    5.21 +                (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
    5.22              case _ => System.err.println("Ignored message without serial number: " + message); this
    5.23            }
    5.24        }
     6.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Aug 31 22:03:55 2010 +0200
     6.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Aug 31 23:28:21 2010 +0200
     6.3 @@ -54,6 +54,22 @@
     6.4      else if (markup.exists(_.name == Markup.FINISHED)) Finished
     6.5      else Unprocessed
     6.6    }
     6.7 +
     6.8 +
     6.9 +  /* reported positions */
    6.10 +
    6.11 +  def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
    6.12 +  {
    6.13 +    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    6.14 +      tree match {
    6.15 +        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    6.16 +        if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
    6.17 +          id == command_id => body.foldLeft(set + range)(reported)
    6.18 +        case XML.Elem(_, body) => body.foldLeft(set)(reported)
    6.19 +        case XML.Text(_) => set
    6.20 +      }
    6.21 +    reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
    6.22 +  }
    6.23  }
    6.24  
    6.25