clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
authorwenzelm
Thu Feb 20 16:56:51 2014 +0100 (2014-02-20)
changeset 55622ce575c2212fc
parent 55621 8d69c15b6fb9
child 55623 7aea773c5574
clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;
NEWS
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/NEWS	Thu Feb 20 16:08:39 2014 +0100
     1.2 +++ b/NEWS	Thu Feb 20 16:56:51 2014 +0100
     1.3 @@ -340,6 +340,15 @@
     1.4      intervals.
     1.5  
     1.6  
     1.7 +*** Scala ***
     1.8 +
     1.9 +* The signature and semantics of Document.Snapshot.cumulate_markup /
    1.10 +select_markup have been clarified.  Markup is now traversed in the
    1.11 +order of reports given by the prover: later markup is usually more
    1.12 +specific and may override results accumulated so far.  The elements
    1.13 +guard is mandatory and checked precisely.  Subtle INCOMPATIBILITY.
    1.14 +
    1.15 +
    1.16  *** ML ***
    1.17  
    1.18  * Proper context discipline for read_instantiate and instantiate_tac:
     2.1 --- a/src/Pure/PIDE/command.scala	Thu Feb 20 16:08:39 2014 +0100
     2.2 +++ b/src/Pure/PIDE/command.scala	Thu Feb 20 16:56:51 2014 +0100
     2.3 @@ -90,8 +90,7 @@
     2.4            (this /: msgs)((state, msg) =>
     2.5              msg match {
     2.6                case elem @ XML.Elem(markup, Nil) =>
     2.7 -                state.add_status(markup)
     2.8 -                  .add_markup("", Text.Info(command.proper_range, elem))  // FIXME cumulation order!?
     2.9 +                state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
    2.10  
    2.11                case _ =>
    2.12                  System.err.println("Ignored status message: " + msg)
     3.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:08:39 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Feb 20 16:56:51 2014 +0100
     3.3 @@ -230,7 +230,7 @@
     3.4        var y = x
     3.5        var changed = false
     3.6        for {
     3.7 -        elem <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
     3.8 +        elem <- entry.markup
     3.9          if elements(elem.name)
    3.10          y1 <- result(y, Text.Info(entry.range, elem))
    3.11        } { y = y1; changed = true }
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:08:39 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 16:56:51 2014 +0100
     4.3 @@ -298,18 +298,18 @@
     4.4  
     4.5    def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
     4.6    {
     4.7 -    snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
     4.8 -      range, Nil, hyperlink_elements, _ =>
     4.9 +    snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
    4.10 +      range, Vector.empty, hyperlink_elements, _ =>
    4.11          {
    4.12            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    4.13            if Path.is_ok(name) =>
    4.14              val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
    4.15              val link = PIDE.editor.hyperlink_file(jedit_file)
    4.16 -            Some(Text.Info(snapshot.convert(info_range), link) :: links)
    4.17 +            Some(links :+ Text.Info(snapshot.convert(info_range), link))
    4.18  
    4.19            case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
    4.20              val link = PIDE.editor.hyperlink_url(name)
    4.21 -            Some(Text.Info(snapshot.convert(info_range), link) :: links)
    4.22 +            Some(links :+ Text.Info(snapshot.convert(info_range), link))
    4.23  
    4.24            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
    4.25            if !props.exists(
    4.26 @@ -323,7 +323,7 @@
    4.27                  case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
    4.28                  case _ => None
    4.29                }
    4.30 -            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    4.31 +            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    4.32  
    4.33            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
    4.34              val opt_link =
    4.35 @@ -332,15 +332,15 @@
    4.36                  case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
    4.37                  case _ => None
    4.38                }
    4.39 -            opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
    4.40 +            opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
    4.41  
    4.42            case _ => None
    4.43 -        }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }
    4.44 +        }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
    4.45    }
    4.46  
    4.47  
    4.48    private val active_elements =
    4.49 -    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
    4.50 +    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE)
    4.51  
    4.52    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
    4.53      snapshot.select_markup(range, active_elements, command_state =>
    4.54 @@ -348,6 +348,7 @@
    4.55          case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
    4.56          if !command_state.results.defined(serial) =>
    4.57            Some(Text.Info(snapshot.convert(info_range), elem))
    4.58 +
    4.59          case Text.Info(info_range, elem) =>
    4.60            if (elem.name == Markup.BROWSER ||
    4.61                elem.name == Markup.GRAPHVIEW ||
    4.62 @@ -420,17 +421,19 @@
    4.63  
    4.64    def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    4.65    {
    4.66 -    def add(prev: Text.Info[(Timing, List[(Boolean, XML.Tree)])],
    4.67 -      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, List[(Boolean, XML.Tree)])] =
    4.68 +    def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
    4.69 +      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
    4.70      {
    4.71        val r = snapshot.convert(r0)
    4.72        val (t, info) = prev.info
    4.73 -      if (prev.range == r) Text.Info(r, (t, p :: info)) else Text.Info(r, (t, List(p)))
    4.74 +      if (prev.range == r)
    4.75 +        Text.Info(r, (t, info :+ p))
    4.76 +      else Text.Info(r, (t, Vector(p)))
    4.77      }
    4.78  
    4.79      val results =
    4.80 -      snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]](
    4.81 -        range, Text.Info(range, (Timing.zero, Nil)), tooltip_elements, _ =>
    4.82 +      snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
    4.83 +        range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
    4.84          {
    4.85            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    4.86              Some(Text.Info(r, (t1 + t2, info)))
    4.87 @@ -462,7 +465,7 @@
    4.88              else None
    4.89          }).map(_.info)
    4.90  
    4.91 -    results.map(_.info).flatMap(_._2) match {
    4.92 +    results.map(_.info).flatMap(res => res._2.toList) match {
    4.93        case Nil => None
    4.94        case tips =>
    4.95          val r = Text.Range(results.head.range.start, results.last.range.stop)