--- 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))
}
}
}
--- 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,
--- 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
--- 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 */