# HG changeset patch # User wenzelm # Date 1321123496 -3600 # Node ID f793dd5d84b23a64aa996e5ec19c1cf9d6ba996d # Parent 66395afbd915e2e84c298903437962caf5e50691 index markup elements for more efficient cumulate/select operations; diff -r 66395afbd915 -r f793dd5d84b2 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Nov 12 18:56:49 2011 +0100 +++ b/src/Pure/PIDE/document.scala Sat Nov 12 19:44:56 2011 +0100 @@ -488,7 +488,8 @@ case (a, Text.Info(r0, b)) if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) => result((a, Text.Info(convert(r0 + command_start), b))) - })) + }, + body.elements)) } yield Text.Info(convert(r0 + command_start), a) } @@ -501,7 +502,7 @@ def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2) def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2)) } - cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1)) + cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1, body.elements)) } } } diff -r 66395afbd915 -r f793dd5d84b2 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Sat Nov 12 18:56:49 2011 +0100 +++ b/src/Pure/PIDE/markup_tree.scala Sat Nov 12 19:44:56 2011 +0100 @@ -15,20 +15,29 @@ object Markup_Tree { - sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A]) - sealed case class Select[A](result: PartialFunction[Text.Markup, A]) + sealed case class Cumulate[A]( + info: A, result: PartialFunction[(A, Text.Markup), A], elements: Option[Set[String]]) + sealed case class Select[A]( + result: PartialFunction[Text.Markup, A], elements: Option[Set[String]]) val empty: Markup_Tree = new Markup_Tree(Branches.empty) object Entry { def apply(markup: Text.Markup, subtree: Markup_Tree): Entry = - Entry(markup.range, List(markup.info), subtree) + Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree) } - sealed case class Entry(range: Text.Range, rev_markup: List[XML.Elem], subtree: Markup_Tree) + sealed case class Entry( + range: Text.Range, + rev_markup: List[XML.Elem], + elements: Set[String], + subtree: Markup_Tree) { - def + (m: XML.Elem): Entry = copy(rev_markup = m :: rev_markup) + def + (info: XML.Elem): Entry = + if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup) + else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name) + def markup: List[XML.Elem] = rev_markup.reverse } @@ -102,17 +111,18 @@ val root_info = body.info def result(x: A, entry: Entry): Option[A] = - { - val (y, changed) = - (entry.markup :\ (x, false))((info, res) => - { - val (y, changed) = res - val arg = (x, Text.Info(entry.range, info)) - if (body.result.isDefinedAt(arg)) (body.result(arg), true) - else res - }) - if (changed) Some(y) else None - } + if (body.elements match { case Some(es) => es.exists(entry.elements) case None => true }) { + val (y, changed) = + (entry.markup :\ (x, false))((info, res) => + { + val (y, changed) = res + val arg = (x, Text.Info(entry.range, info)) + if (body.result.isDefinedAt(arg)) (body.result(arg), true) + else res + }) + if (changed) Some(y) else None + } + else None def stream( last: Text.Offset, diff -r 66395afbd915 -r f793dd5d84b2 src/Tools/jEdit/src/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Sat Nov 12 18:56:49 2011 +0100 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Sat Nov 12 19:44:56 2011 +0100 @@ -89,7 +89,8 @@ } case _ => null } - })) + }, + Some(Set(Markup.ENTITY)))) markup match { case Text.Info(_, Some(link)) #:: _ => link case _ => null diff -r 66395afbd915 -r f793dd5d84b2 src/Tools/jEdit/src/isabelle_markup.scala --- a/src/Tools/jEdit/src/isabelle_markup.scala Sat Nov 12 18:56:49 2011 +0100 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Sat Nov 12 19:44:56 2011 +0100 @@ -89,11 +89,12 @@ val message = Markup_Tree.Select[Color]( - { - case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color - case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color - case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color - }) + { + case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color + case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color + case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color + }, + Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR))) val tooltip_message = Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty, @@ -102,7 +103,8 @@ if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msgs + (serial -> Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))) - }) + }, + Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR))) val gutter_message = Markup_Tree.Select[Icon]( @@ -113,20 +115,23 @@ case _ => warning_icon } case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon - }) + }, + Some(Set(Markup.WARNING, Markup.ERROR))) val background1 = Markup_Tree.Select[Color]( { case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color - }) + }, + Some(Set(Markup.BAD, Markup.HILITE))) val background2 = Markup_Tree.Select[Color]( { case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color - }) + }, + Some(Set(Markup.TOKEN_RANGE))) val foreground = Markup_Tree.Select[Color]( @@ -134,7 +139,8 @@ case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color - }) + }, + Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM))) private val text_colors: Map[String, Color] = Map( @@ -164,8 +170,10 @@ val text_color = Markup_Tree.Select[Color]( { - case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m) - }) + case Text.Info(_, XML.Elem(Markup(m, _), _)) + if text_colors.isDefinedAt(m) => text_colors(m) + }, + Some(Set() ++ text_colors.keys)) private val tooltips: Map[String, String] = Map( @@ -191,16 +199,19 @@ Markup_Tree.Select[String]( { case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name) - case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body) + case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => + string_of_typing("ML:", body) case Text.Info(_, XML.Elem(Markup(name, _), _)) if tooltips.isDefinedAt(name) => tooltips(name) - }) + }, + Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys)) val tooltip2 = Markup_Tree.Select[String]( { case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body) - }) + }, + Some(Set(Markup.TYPING))) private val subexp_include = Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, @@ -212,7 +223,8 @@ { case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => (range, subexp_color) - }) + }, + Some(subexp_include)) /* token markup -- text styles */