clarified Isabelle_Rendering vs. physical painting;
discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;
--- a/src/Pure/PIDE/document.scala Tue Jan 10 18:12:55 2012 +0100
+++ b/src/Pure/PIDE/document.scala Tue Jan 10 23:26:27 2012 +0100
@@ -239,9 +239,10 @@
def convert(range: Text.Range): Text.Range
def revert(i: Text.Offset): Text.Offset
def revert(range: Text.Range): Text.Range
- def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
- def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
- : Stream[Text.Info[Option[A]]]
+ def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
+ result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
+ def select_markup[A](range: Text.Range, elements: Option[Set[String]],
+ result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]]
}
type Assign =
@@ -471,37 +472,31 @@
def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
- def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A])
- : Stream[Text.Info[A]] =
+ def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
+ result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
{
- val info = body.info
- val result = body.result
-
val former_range = revert(range)
for {
(command, command_start) <- node.command_range(former_range).toStream
Text.Info(r0, a) <- command_state(command).markup.
- cumulate((former_range - command_start).restrict(command.range))(
- Markup_Tree.Cumulate[A](info,
- {
- 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))
+ cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
+ {
+ 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)))
+ })
} yield Text.Info(convert(r0 + command_start), a)
}
- def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
- : Stream[Text.Info[Option[A]]] =
+ def select_markup[A](range: Text.Range, elements: Option[Set[String]],
+ result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]] =
{
- val result = body.result
val result1 =
new PartialFunction[(Option[A], Text.Markup), Option[A]] {
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, body.elements))
+ cumulate_markup(range, None, elements, result1)
}
}
}
--- a/src/Pure/PIDE/markup_tree.scala Tue Jan 10 18:12:55 2012 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Tue Jan 10 23:26:27 2012 +0100
@@ -16,11 +16,6 @@
object Markup_Tree
{
- 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
@@ -107,18 +102,17 @@
}
}
- def cumulate[A](root_range: Text.Range)(body: Cumulate[A]): Stream[Text.Info[A]] =
+ def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
+ result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
{
- val root_info = body.info
-
- def result(x: A, entry: Entry): Option[A] =
- if (body.elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
+ def results(x: A, entry: Entry): Option[A] =
+ if (result_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 = (y, Text.Info(entry.range, info))
- if (body.result.isDefinedAt(arg)) (body.result(arg), true)
+ if (result.isDefinedAt(arg)) (result(arg), true)
else res
})
if (changed) Some(y) else None
@@ -135,7 +129,7 @@
val subtree = entry.subtree.overlapping(subrange).toStream
val start = subrange.start
- result(parent.info, entry) match {
+ results(parent.info, entry) match {
case Some(res) =>
val next = Text.Info(subrange, res)
val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
--- a/src/Tools/jEdit/src/document_view.scala Tue Jan 10 18:12:55 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Tue Jan 10 23:26:27 2012 +0100
@@ -214,10 +214,7 @@
: Option[(Text.Range, Color)] =
{
val offset = text_area.xyToOffset(x, y)
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.subexp) match {
- case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
- case _ => None
- }
+ Isabelle_Rendering.subexp(snapshot, Text.Range(offset, offset + 1))
}
@volatile private var _highlight_range: Option[(Text.Range, Color)] = None
@@ -278,30 +275,10 @@
val snapshot = update_snapshot()
val offset = text_area.xyToOffset(x, y)
val range = Text.Range(offset, offset + 1)
-
- if (control) {
- val tooltips =
- (snapshot.select_markup(range)(Isabelle_Rendering.tooltip1) match
- {
- case Text.Info(_, Some(text)) #:: _ => List(text)
- case _ => Nil
- }) :::
- (snapshot.select_markup(range)(Isabelle_Rendering.tooltip2) match
- {
- case Text.Info(_, Some(text)) #:: _ => List(text)
- case _ => Nil
- })
- if (tooltips.isEmpty) null
- else Isabelle.tooltip(tooltips.mkString("\n"))
- }
- else {
- snapshot.cumulate_markup(range)(Isabelle_Rendering.tooltip_message) match
- {
- case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
- Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
- case _ => null
- }
- }
+ val tip =
+ if (control) Isabelle_Rendering.tooltip(snapshot, range)
+ else Isabelle_Rendering.tooltip_message(snapshot, range)
+ tip.map(Isabelle.tooltip(_)) getOrElse null
}
}
}
@@ -326,17 +303,13 @@
val line_range = proper_line_range(start(i), end(i))
// gutter icons
- val icons =
- (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
- snapshot.select_markup(line_range)(Isabelle_Rendering.gutter_message).iterator)
- yield icon).toList.sortWith(_ >= _)
- icons match {
- case icon :: _ =>
+ Isabelle_Rendering.gutter_message(snapshot, line_range) match {
+ case Some(icon) =>
val icn = icon.icon
val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
icn.paintIcon(gutter, gfx, x0, y0)
- case Nil =>
+ case None =>
}
}
}
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Jan 10 18:12:55 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Tue Jan 10 23:26:27 2012 +0100
@@ -57,40 +57,40 @@
case Some(model) =>
val snapshot = model.snapshot()
val markup =
- snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
- Markup_Tree.Select[Hyperlink](
- {
- // FIXME Protocol.Hyperlink extractor
- case Text.Info(info_range,
- XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
- if (props.find(
- { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
- case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
- case _ => false }).isEmpty) =>
- val Text.Range(begin, end) = info_range
- val line = buffer.getLineOfOffset(begin)
- (Position.File.unapply(props), Position.Line.unapply(props)) match {
- case (Some(def_file), Some(def_line)) =>
- new External_Hyperlink(begin, end, line, def_file, def_line)
- case _ if !snapshot.is_outdated =>
- (props, props) match {
- case (Position.Id(def_id), Position.Offset(def_offset)) =>
- snapshot.state.find_command(snapshot.version, def_id) match {
- case Some((def_node, def_cmd)) =>
- def_node.command_start(def_cmd) match {
- case Some(def_cmd_start) =>
- new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
- def_cmd_start + def_cmd.decode(def_offset))
- case None => null
- }
- case None => null
- }
- case _ => null
- }
- case _ => null
- }
- },
- Some(Set(Isabelle_Markup.ENTITY))))
+ snapshot.select_markup[Hyperlink](
+ Text.Range(buffer_offset, buffer_offset + 1),
+ Some(Set(Isabelle_Markup.ENTITY)),
+ {
+ // FIXME Protocol.Hyperlink extractor
+ case Text.Info(info_range,
+ XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
+ if (props.find(
+ { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
+ case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
+ case _ => false }).isEmpty) =>
+ val Text.Range(begin, end) = info_range
+ val line = buffer.getLineOfOffset(begin)
+ (Position.File.unapply(props), Position.Line.unapply(props)) match {
+ case (Some(def_file), Some(def_line)) =>
+ new External_Hyperlink(begin, end, line, def_file, def_line)
+ case _ if !snapshot.is_outdated =>
+ (props, props) match {
+ case (Position.Id(def_id), Position.Offset(def_offset)) =>
+ snapshot.state.find_command(snapshot.version, def_id) match {
+ case Some((def_node, def_cmd)) =>
+ def_node.command_start(def_cmd) match {
+ case Some(def_cmd_start) =>
+ new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
+ def_cmd_start + def_cmd.decode(def_offset))
+ case None => null
+ }
+ case None => null
+ }
+ case _ => null
+ }
+ case _ => null
+ }
+ })
markup match {
case Text.Info(_, Some(link)) #:: _ => link
case _ => null
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Tue Jan 10 18:12:55 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Tue Jan 10 23:26:27 2012 +0100
@@ -78,17 +78,21 @@
/* markup selectors */
- val message =
- Markup_Tree.Select[Color](
- {
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
- },
- Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
+ def message_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
+ for {
+ Text.Info(r, Some(color)) <-
+ snapshot.select_markup(range,
+ Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ {
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
+ })
+ } yield Text.Info(r, color)
- val tooltip_message =
- Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
+ def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
+ snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
+ Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
{
case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
if markup == Isabelle_Markup.WRITELN ||
@@ -96,50 +100,83 @@
markup == Isabelle_Markup.ERROR =>
msgs + (serial ->
Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
- },
- Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
+ }) match {
+ case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
+ Some(msgs.iterator.map(_._2).mkString("\n"))
+ case _ => None
+ }
- val gutter_message =
- Markup_Tree.Select[Icon](
- {
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
- body match {
- case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
- case _ => warning_icon
- }
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
- },
- Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
+ def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
+ {
+ val icons =
+ (for {
+ Text.Info(_, Some(icon)) <-
+ // FIXME snapshot.cumulate_markup
+ snapshot.select_markup[Icon](range,
+ Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
+ {
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
+ body match {
+ case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
+ case _ => warning_icon
+ }
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
+ })
+ } yield icon).toList.sortWith(_ >= _)
+ icons match {
+ case icon :: _ => Some(icon)
+ case Nil => None
+ }
+ }
- val background1 =
- Markup_Tree.Cumulate[(Option[Protocol.Status], Option[Color])](
- (Some(Protocol.Status()), None),
- {
- case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
- if (Protocol.command_status_markup(markup.name)) =>
- (Some(Protocol.command_status(status, markup)), color)
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
- (None, Some(bad_color))
- case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
- (None, Some(hilite_color))
- },
- Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE))
+ def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
+ {
+ for {
+ Text.Info(r, result) <-
+ snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
+ range, (Some(Protocol.Status()), None),
+ Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
+ {
+ case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
+ if (Protocol.command_status_markup(markup.name)) =>
+ (Some(Protocol.command_status(status, markup)), color)
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
+ (None, Some(bad_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
+ (None, Some(hilite_color))
+ })
+ color <-
+ (result match {
+ case (Some(status), _) =>
+ if (status.is_running) Some(running1_color)
+ else if (status.is_unprocessed) Some(unprocessed1_color)
+ else None
+ case (_, opt_color) => opt_color
+ })
+ } yield Text.Info(r, color)
+ }
- val background2 =
- Markup_Tree.Select[Color](
- {
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
- },
- Some(Set(Isabelle_Markup.TOKEN_RANGE)))
+ def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
+ for {
+ Text.Info(r, Some(color)) <-
+ snapshot.select_markup(range,
+ Some(Set(Isabelle_Markup.TOKEN_RANGE)),
+ {
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
+ })
+ } yield Text.Info(r, color)
- val foreground =
- Markup_Tree.Select[Color](
- {
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
- },
- Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)))
+ def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
+ for {
+ Text.Info(r, Some(color)) <-
+ snapshot.select_markup(range,
+ Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
+ {
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
+ })
+ } yield Text.Info(r, color)
private val text_colors: Map[String, Color] =
Map(
@@ -166,13 +203,14 @@
Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
Isabelle_Markup.ANTIQ -> get_color("blue"))
- val text_color =
- Markup_Tree.Select[Color](
+ private val text_color_elements = Set.empty[String] ++ text_colors.keys
+
+ def text_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Option[Color]]] =
+ snapshot.select_markup(range, Some(text_color_elements),
{
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(
@@ -194,24 +232,32 @@
Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
margin = Isabelle.Int_Property("tooltip-margin"))
- val tooltip1 =
- Markup_Tree.Select[String](
- {
- case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) => kind + " " + quote(name)
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
- string_of_typing("ML:", body)
- case Text.Info(_, XML.Elem(Markup(name, _), _))
- if tooltips.isDefinedAt(name) => tooltips(name)
- },
- Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys))
+ def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
+ {
+ val tip1 =
+ snapshot.select_markup(range,
+ Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys),
+ {
+ case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) =>
+ kind + " " + quote(name)
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
+ string_of_typing("ML:", body)
+ case Text.Info(_, XML.Elem(Markup(name, _), _))
+ if tooltips.isDefinedAt(name) => tooltips(name)
+ })
+ val tip2 =
+ snapshot.select_markup(range, Some(Set(Isabelle_Markup.TYPING)),
+ {
+ case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
+ string_of_typing("::", body)
+ })
- val tooltip2 =
- Markup_Tree.Select[String](
- {
- case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
- string_of_typing("::", body)
- },
- Some(Set(Isabelle_Markup.TYPING)))
+ val tips =
+ (tip1 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil }) :::
+ (tip2 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil })
+
+ if (tips.isEmpty) None else Some(tips.mkString("\n"))
+ }
private val subexp_include =
Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
@@ -220,13 +266,17 @@
Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
Isabelle_Markup.DOC_SOURCE)
- val subexp =
- Markup_Tree.Select[(Text.Range, Color)](
- {
- case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
- (range, subexp_color)
- },
- Some(subexp_include))
+ def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[(Text.Range, Color)] =
+ {
+ snapshot.select_markup(range, Some(subexp_include),
+ {
+ case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+ (range, subexp_color)
+ }) match {
+ case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
+ case _ => None
+ }
+ }
/* token markup -- text styles */
--- a/src/Tools/jEdit/src/text_area_painter.scala Tue Jan 10 18:12:55 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala Tue Jan 10 23:26:27 2012 +0100
@@ -91,18 +91,7 @@
// background color (1)
for {
- Text.Info(range, result) <-
- snapshot.cumulate_markup(line_range)(Isabelle_Rendering.background1).iterator
- // FIXME more abstract Isabelle_Rendering.markup etc.
- val opt_color =
- result match {
- case (Some(status), _) =>
- if (status.is_running) Some(Isabelle_Rendering.running1_color)
- else if (status.is_unprocessed) Some(Isabelle_Rendering.unprocessed1_color)
- else None
- case (_, color) => color
- }
- color <- opt_color
+ Text.Info(range, color) <- Isabelle_Rendering.background1(snapshot, line_range)
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
@@ -111,8 +100,7 @@
// background color (2)
for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Rendering.background2).iterator
+ Text.Info(range, color) <- Isabelle_Rendering.background2(snapshot, line_range)
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
@@ -121,8 +109,7 @@
// squiggly underline
for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Rendering.message).iterator
+ Text.Info(range, color) <- Isabelle_Rendering.message_color(snapshot, line_range)
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
@@ -213,7 +200,7 @@
val markup =
for {
- r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Rendering.text_color)
+ r1 <- Isabelle_Rendering.text_color(painter_snapshot, chunk_range)
r2 <- r1.try_restrict(chunk_range)
} yield r2
@@ -314,8 +301,7 @@
// foreground color
for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Rendering.foreground).iterator
+ Text.Info(range, color) <- Isabelle_Rendering.foreground(snapshot, line_range)
r <- Isabelle.gfx_range(text_area, range)
} {
gfx.setColor(color)
--- a/src/Tools/jEdit/src/token_markup.scala Tue Jan 10 18:12:55 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Tue Jan 10 23:26:27 2012 +0100
@@ -178,7 +178,8 @@
if (line_ctxt.isDefined && Isabelle.session.is_ready) {
val syntax = Isabelle.session.current_syntax()
val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
- val styled_tokens = tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))
+ val styled_tokens =
+ tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))
(styled_tokens, new Line_Context(Some(ctxt1)))
}
else {