# HG changeset patch # User wenzelm # Date 1392911811 -3600 # Node ID ce575c2212fca29392abd028305f9dfe3c012953 # Parent 8d69c15b6fb992104dae66252831730fed15dac1 clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context; diff -r 8d69c15b6fb9 -r ce575c2212fc NEWS --- a/NEWS Thu Feb 20 16:08:39 2014 +0100 +++ b/NEWS Thu Feb 20 16:56:51 2014 +0100 @@ -340,6 +340,15 @@ intervals. +*** Scala *** + +* The signature and semantics of Document.Snapshot.cumulate_markup / +select_markup have been clarified. Markup is now traversed in the +order of reports given by the prover: later markup is usually more +specific and may override results accumulated so far. The elements +guard is mandatory and checked precisely. Subtle INCOMPATIBILITY. + + *** ML *** * Proper context discipline for read_instantiate and instantiate_tac: diff -r 8d69c15b6fb9 -r ce575c2212fc src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Feb 20 16:08:39 2014 +0100 +++ b/src/Pure/PIDE/command.scala Thu Feb 20 16:56:51 2014 +0100 @@ -90,8 +90,7 @@ (this /: msgs)((state, msg) => msg match { case elem @ XML.Elem(markup, Nil) => - state.add_status(markup) - .add_markup("", Text.Info(command.proper_range, elem)) // FIXME cumulation order!? + state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem)) case _ => System.err.println("Ignored status message: " + msg) diff -r 8d69c15b6fb9 -r ce575c2212fc src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Thu Feb 20 16:08:39 2014 +0100 +++ b/src/Pure/PIDE/markup_tree.scala Thu Feb 20 16:56:51 2014 +0100 @@ -230,7 +230,7 @@ var y = x var changed = false for { - elem <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?) + elem <- entry.markup if elements(elem.name) y1 <- result(y, Text.Info(entry.range, elem)) } { y = y1; changed = true } diff -r 8d69c15b6fb9 -r ce575c2212fc src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Thu Feb 20 16:08:39 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Thu Feb 20 16:56:51 2014 +0100 @@ -298,18 +298,18 @@ def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] = { - snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]]( - range, Nil, hyperlink_elements, _ => + snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]]( + range, Vector.empty, hyperlink_elements, _ => { case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) if Path.is_ok(name) => val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name)) val link = PIDE.editor.hyperlink_file(jedit_file) - Some(Text.Info(snapshot.convert(info_range), link) :: links) + Some(links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) => val link = PIDE.editor.hyperlink_url(name) - Some(Text.Info(snapshot.convert(info_range), link) :: links) + Some(links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) if !props.exists( @@ -323,7 +323,7 @@ case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset) case _ => None } - opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) + opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => val opt_link = @@ -332,15 +332,15 @@ case Position.Id_Offset(id, offset) => hyperlink_command(id, offset) case _ => None } - opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links)) + opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link))) case _ => None - }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None } + }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } } private val active_elements = - Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE) + Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE) def active(range: Text.Range): Option[Text.Info[XML.Elem]] = snapshot.select_markup(range, active_elements, command_state => @@ -348,6 +348,7 @@ case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _)) if !command_state.results.defined(serial) => Some(Text.Info(snapshot.convert(info_range), elem)) + case Text.Info(info_range, elem) => if (elem.name == Markup.BROWSER || elem.name == Markup.GRAPHVIEW || @@ -420,17 +421,19 @@ def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] = { - def add(prev: Text.Info[(Timing, List[(Boolean, XML.Tree)])], - r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, List[(Boolean, XML.Tree)])] = + def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])], + r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] = { val r = snapshot.convert(r0) val (t, info) = prev.info - if (prev.range == r) Text.Info(r, (t, p :: info)) else Text.Info(r, (t, List(p))) + if (prev.range == r) + Text.Info(r, (t, info :+ p)) + else Text.Info(r, (t, Vector(p))) } val results = - snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]]( - range, Text.Info(range, (Timing.zero, Nil)), tooltip_elements, _ => + snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]]( + range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ => { case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) => Some(Text.Info(r, (t1 + t2, info))) @@ -462,7 +465,7 @@ else None }).map(_.info) - results.map(_.info).flatMap(_._2) match { + results.map(_.info).flatMap(res => res._2.toList) match { case Nil => None case tips => val r = Text.Range(results.head.range.start, results.last.range.stop)