allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
authorwenzelm
Fri Sep 17 17:10:44 2010 +0200 (2010-09-17)
changeset 394414110cc1b8f9f
parent 39440 4c2547af5909
child 39442 73bcb12fdc69
allow embedded reports in regular prover messages, to avoid side-effects for errors for example;
src/Pure/Isar/proof_context.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/isar_document.scala
src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:09:31 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Sep 17 17:10:44 2010 +0200
     1.3 @@ -734,8 +734,8 @@
     1.4  local
     1.5  
     1.6  fun parse_failed ctxt pos msg kind =
     1.7 - (Context_Position.report ctxt Markup.bad pos;
     1.8 -  cat_error msg ("Failed to parse " ^ kind));
     1.9 +  cat_error msg ("Failed to parse " ^ kind ^
    1.10 +    Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos ""));
    1.11  
    1.12  fun parse_sort ctxt text =
    1.13    let
     2.1 --- a/src/Pure/PIDE/command.scala	Fri Sep 17 17:09:31 2010 +0200
     2.2 +++ b/src/Pure/PIDE/command.scala	Fri Sep 17 17:10:44 2010 +0200
     2.3 @@ -60,8 +60,10 @@
     2.4            atts match {
     2.5              case Markup.Serial(i) =>
     2.6                val result = XML.Elem(Markup(name, Position.purge(atts)), body)
     2.7 -              (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
     2.8 -                (st, range) => st.add_markup(Text.Info(range, result)))
     2.9 +              val st1 =
    2.10 +                (add_result(i, result) /: Isar_Document.message_positions(command, message))(
    2.11 +                  (st, range) => st.add_markup(Text.Info(range, result)))
    2.12 +              (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
    2.13              case _ => System.err.println("Ignored message without serial number: " + message); this
    2.14            }
    2.15        }
     3.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Sep 17 17:09:31 2010 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 17 17:10:44 2010 +0200
     3.3 @@ -56,35 +56,42 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* messages */
     3.8 +  /* result messages */
     3.9  
    3.10    def clean_message(body: XML.Body): XML.Body =
    3.11      body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
    3.12        { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
    3.13  
    3.14 +  def message_reports(msg: XML.Tree): List[XML.Elem] =
    3.15 +    msg match {
    3.16 +      case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
    3.17 +      case XML.Elem(_, body) => body.flatMap(message_reports)
    3.18 +      case XML.Text(_) => Nil
    3.19 +    }
    3.20 +
    3.21  
    3.22    /* reported positions */
    3.23  
    3.24 -  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    3.25 -
    3.26 -  private def is_state(msg: XML.Tree): Boolean =
    3.27 +  def is_state(msg: XML.Tree): Boolean =
    3.28      msg match {
    3.29        case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    3.30        case _ => false
    3.31      }
    3.32  
    3.33 -  def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
    3.34 +  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    3.35 +
    3.36 +  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
    3.37    {
    3.38 -    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    3.39 +    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    3.40        tree match {
    3.41          case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
    3.42          if include_pos(name) && id == command.id =>
    3.43            val range = command.decode(raw_range).restrict(command.range)
    3.44 -          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
    3.45 -        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(reported)
    3.46 +          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    3.47 +        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
    3.48          case _ => set
    3.49        }
    3.50 -    val set = reported(Set.empty, message)
    3.51 +    val set = positions(Set.empty, message)
    3.52      if (set.isEmpty && !is_state(message))
    3.53        set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
    3.54      else set
     4.1 --- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 17:09:31 2010 +0200
     4.2 +++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 17:10:44 2010 +0200
     4.3 @@ -8,6 +8,8 @@
     4.4  .error { background-color: #FFC1C1; }
     4.5  .debug { background-color: #FFE4E1; }
     4.6  
     4.7 +.report { display: none; }
     4.8 +
     4.9  .hilite { background-color: #FFFACD; }
    4.10  
    4.11  .keyword { font-weight: bold; color: #009966; }