# HG changeset patch # User wenzelm # Date 1326234387 -3600 # Node ID 1c5c88f6feb53e8a22e4f8b6e2513fb2726c7841 # Parent adac34829e108fdab6525790edb0e3e92a6e7d0c clarified Isabelle_Rendering vs. physical painting; discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select; diff -r adac34829e10 -r 1c5c88f6feb5 src/Pure/PIDE/document.scala --- 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) } } } diff -r adac34829e10 -r 1c5c88f6feb5 src/Pure/PIDE/markup_tree.scala --- 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) diff -r adac34829e10 -r 1c5c88f6feb5 src/Tools/jEdit/src/document_view.scala --- 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 => } } } diff -r adac34829e10 -r 1c5c88f6feb5 src/Tools/jEdit/src/isabelle_hyperlinks.scala --- 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 diff -r adac34829e10 -r 1c5c88f6feb5 src/Tools/jEdit/src/isabelle_rendering.scala --- 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 */ diff -r adac34829e10 -r 1c5c88f6feb5 src/Tools/jEdit/src/text_area_painter.scala --- 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) diff -r adac34829e10 -r 1c5c88f6feb5 src/Tools/jEdit/src/token_markup.scala --- 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 {