clarified Isabelle_Rendering vs. physical painting;
authorwenzelm
Tue Jan 10 23:26:27 2012 +0100 (2012-01-10)
changeset 461781c5c88f6feb5
parent 46177 adac34829e10
child 46183 eda2c0aeb1f2
clarified Isabelle_Rendering vs. physical painting;
discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/text_area_painter.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Jan 10 18:12:55 2012 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Jan 10 23:26:27 2012 +0100
     1.3 @@ -239,9 +239,10 @@
     1.4      def convert(range: Text.Range): Text.Range
     1.5      def revert(i: Text.Offset): Text.Offset
     1.6      def revert(range: Text.Range): Text.Range
     1.7 -    def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
     1.8 -    def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
     1.9 -      : Stream[Text.Info[Option[A]]]
    1.10 +    def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    1.11 +      result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
    1.12 +    def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.13 +      result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]]
    1.14    }
    1.15  
    1.16    type Assign =
    1.17 @@ -471,37 +472,31 @@
    1.18          def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.19          def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.20  
    1.21 -        def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A])
    1.22 -          : Stream[Text.Info[A]] =
    1.23 +        def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
    1.24 +          result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    1.25          {
    1.26 -          val info = body.info
    1.27 -          val result = body.result
    1.28 -
    1.29            val former_range = revert(range)
    1.30            for {
    1.31              (command, command_start) <- node.command_range(former_range).toStream
    1.32              Text.Info(r0, a) <- command_state(command).markup.
    1.33 -              cumulate((former_range - command_start).restrict(command.range))(
    1.34 -                Markup_Tree.Cumulate[A](info,
    1.35 -                  {
    1.36 -                    case (a, Text.Info(r0, b))
    1.37 -                    if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.38 -                      result((a, Text.Info(convert(r0 + command_start), b)))
    1.39 -                  },
    1.40 -                  body.elements))
    1.41 +              cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
    1.42 +                {
    1.43 +                  case (a, Text.Info(r0, b))
    1.44 +                  if result.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
    1.45 +                    result((a, Text.Info(convert(r0 + command_start), b)))
    1.46 +                })
    1.47            } yield Text.Info(convert(r0 + command_start), a)
    1.48          }
    1.49  
    1.50 -        def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
    1.51 -          : Stream[Text.Info[Option[A]]] =
    1.52 +        def select_markup[A](range: Text.Range, elements: Option[Set[String]],
    1.53 +          result: PartialFunction[Text.Markup, A]): Stream[Text.Info[Option[A]]] =
    1.54          {
    1.55 -          val result = body.result
    1.56            val result1 =
    1.57              new PartialFunction[(Option[A], Text.Markup), Option[A]] {
    1.58                def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = result.isDefinedAt(arg._2)
    1.59                def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(result(arg._2))
    1.60              }
    1.61 -          cumulate_markup(range)(Markup_Tree.Cumulate[Option[A]](None, result1, body.elements))
    1.62 +          cumulate_markup(range, None, elements, result1)
    1.63          }
    1.64        }
    1.65      }
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Jan 10 18:12:55 2012 +0100
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Jan 10 23:26:27 2012 +0100
     2.3 @@ -16,11 +16,6 @@
     2.4  
     2.5  object Markup_Tree
     2.6  {
     2.7 -  sealed case class Cumulate[A](
     2.8 -    info: A, result: PartialFunction[(A, Text.Markup), A], elements: Option[Set[String]])
     2.9 -  sealed case class Select[A](
    2.10 -    result: PartialFunction[Text.Markup, A], elements: Option[Set[String]])
    2.11 -
    2.12    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    2.13  
    2.14    object Entry
    2.15 @@ -107,18 +102,17 @@
    2.16      }
    2.17    }
    2.18  
    2.19 -  def cumulate[A](root_range: Text.Range)(body: Cumulate[A]): Stream[Text.Info[A]] =
    2.20 +  def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
    2.21 +    result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
    2.22    {
    2.23 -    val root_info = body.info
    2.24 -
    2.25 -    def result(x: A, entry: Entry): Option[A] =
    2.26 -      if (body.elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
    2.27 +    def results(x: A, entry: Entry): Option[A] =
    2.28 +      if (result_elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
    2.29          val (y, changed) =
    2.30            (entry.markup :\ (x, false))((info, res) =>
    2.31              {
    2.32                val (y, changed) = res
    2.33                val arg = (y, Text.Info(entry.range, info))
    2.34 -              if (body.result.isDefinedAt(arg)) (body.result(arg), true)
    2.35 +              if (result.isDefinedAt(arg)) (result(arg), true)
    2.36                else res
    2.37              })
    2.38          if (changed) Some(y) else None
    2.39 @@ -135,7 +129,7 @@
    2.40            val subtree = entry.subtree.overlapping(subrange).toStream
    2.41            val start = subrange.start
    2.42  
    2.43 -          result(parent.info, entry) match {
    2.44 +          results(parent.info, entry) match {
    2.45              case Some(res) =>
    2.46                val next = Text.Info(subrange, res)
    2.47                val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
     3.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Jan 10 18:12:55 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Jan 10 23:26:27 2012 +0100
     3.3 @@ -214,10 +214,7 @@
     3.4      : Option[(Text.Range, Color)] =
     3.5    {
     3.6      val offset = text_area.xyToOffset(x, y)
     3.7 -    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.subexp) match {
     3.8 -      case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
     3.9 -      case _ => None
    3.10 -    }
    3.11 +    Isabelle_Rendering.subexp(snapshot, Text.Range(offset, offset + 1))
    3.12    }
    3.13  
    3.14    @volatile private var _highlight_range: Option[(Text.Range, Color)] = None
    3.15 @@ -278,30 +275,10 @@
    3.16          val snapshot = update_snapshot()
    3.17          val offset = text_area.xyToOffset(x, y)
    3.18          val range = Text.Range(offset, offset + 1)
    3.19 -
    3.20 -        if (control) {
    3.21 -          val tooltips =
    3.22 -            (snapshot.select_markup(range)(Isabelle_Rendering.tooltip1) match
    3.23 -              {
    3.24 -                case Text.Info(_, Some(text)) #:: _ => List(text)
    3.25 -                case _ => Nil
    3.26 -              }) :::
    3.27 -            (snapshot.select_markup(range)(Isabelle_Rendering.tooltip2) match
    3.28 -              {
    3.29 -                case Text.Info(_, Some(text)) #:: _ => List(text)
    3.30 -                case _ => Nil
    3.31 -              })
    3.32 -          if (tooltips.isEmpty) null
    3.33 -          else Isabelle.tooltip(tooltips.mkString("\n"))
    3.34 -        }
    3.35 -        else {
    3.36 -          snapshot.cumulate_markup(range)(Isabelle_Rendering.tooltip_message) match
    3.37 -          {
    3.38 -            case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
    3.39 -              Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
    3.40 -            case _ => null
    3.41 -          }
    3.42 -        }
    3.43 +        val tip =
    3.44 +          if (control) Isabelle_Rendering.tooltip(snapshot, range)
    3.45 +          else Isabelle_Rendering.tooltip_message(snapshot, range)
    3.46 +        tip.map(Isabelle.tooltip(_)) getOrElse null
    3.47        }
    3.48      }
    3.49    }
    3.50 @@ -326,17 +303,13 @@
    3.51                  val line_range = proper_line_range(start(i), end(i))
    3.52  
    3.53                  // gutter icons
    3.54 -                val icons =
    3.55 -                  (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
    3.56 -                    snapshot.select_markup(line_range)(Isabelle_Rendering.gutter_message).iterator)
    3.57 -                  yield icon).toList.sortWith(_ >= _)
    3.58 -                icons match {
    3.59 -                  case icon :: _ =>
    3.60 +                Isabelle_Rendering.gutter_message(snapshot, line_range) match {
    3.61 +                  case Some(icon) =>
    3.62                      val icn = icon.icon
    3.63                      val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
    3.64                      val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
    3.65                      icn.paintIcon(gutter, gfx, x0, y0)
    3.66 -                  case Nil =>
    3.67 +                  case None =>
    3.68                  }
    3.69                }
    3.70              }
     4.1 --- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Jan 10 18:12:55 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Tue Jan 10 23:26:27 2012 +0100
     4.3 @@ -57,40 +57,40 @@
     4.4          case Some(model) =>
     4.5            val snapshot = model.snapshot()
     4.6            val markup =
     4.7 -            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
     4.8 -              Markup_Tree.Select[Hyperlink](
     4.9 -                {
    4.10 -                  // FIXME Protocol.Hyperlink extractor
    4.11 -                  case Text.Info(info_range,
    4.12 -                      XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
    4.13 -                    if (props.find(
    4.14 -                      { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
    4.15 -                        case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
    4.16 -                        case _ => false }).isEmpty) =>
    4.17 -                    val Text.Range(begin, end) = info_range
    4.18 -                    val line = buffer.getLineOfOffset(begin)
    4.19 -                    (Position.File.unapply(props), Position.Line.unapply(props)) match {
    4.20 -                      case (Some(def_file), Some(def_line)) =>
    4.21 -                        new External_Hyperlink(begin, end, line, def_file, def_line)
    4.22 -                      case _ if !snapshot.is_outdated =>
    4.23 -                        (props, props) match {
    4.24 -                          case (Position.Id(def_id), Position.Offset(def_offset)) =>
    4.25 -                            snapshot.state.find_command(snapshot.version, def_id) match {
    4.26 -                              case Some((def_node, def_cmd)) =>
    4.27 -                                def_node.command_start(def_cmd) match {
    4.28 -                                  case Some(def_cmd_start) =>
    4.29 -                                    new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
    4.30 -                                      def_cmd_start + def_cmd.decode(def_offset))
    4.31 -                                  case None => null
    4.32 -                                }
    4.33 -                              case None => null
    4.34 -                            }
    4.35 -                          case _ => null
    4.36 -                        }
    4.37 -                      case _ => null
    4.38 -                    }
    4.39 -                },
    4.40 -                Some(Set(Isabelle_Markup.ENTITY))))
    4.41 +            snapshot.select_markup[Hyperlink](
    4.42 +              Text.Range(buffer_offset, buffer_offset + 1),
    4.43 +              Some(Set(Isabelle_Markup.ENTITY)),
    4.44 +              {
    4.45 +                // FIXME Protocol.Hyperlink extractor
    4.46 +                case Text.Info(info_range,
    4.47 +                    XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _))
    4.48 +                  if (props.find(
    4.49 +                    { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
    4.50 +                      case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
    4.51 +                      case _ => false }).isEmpty) =>
    4.52 +                  val Text.Range(begin, end) = info_range
    4.53 +                  val line = buffer.getLineOfOffset(begin)
    4.54 +                  (Position.File.unapply(props), Position.Line.unapply(props)) match {
    4.55 +                    case (Some(def_file), Some(def_line)) =>
    4.56 +                      new External_Hyperlink(begin, end, line, def_file, def_line)
    4.57 +                    case _ if !snapshot.is_outdated =>
    4.58 +                      (props, props) match {
    4.59 +                        case (Position.Id(def_id), Position.Offset(def_offset)) =>
    4.60 +                          snapshot.state.find_command(snapshot.version, def_id) match {
    4.61 +                            case Some((def_node, def_cmd)) =>
    4.62 +                              def_node.command_start(def_cmd) match {
    4.63 +                                case Some(def_cmd_start) =>
    4.64 +                                  new Internal_Hyperlink(def_cmd.node_name.node, begin, end, line,
    4.65 +                                    def_cmd_start + def_cmd.decode(def_offset))
    4.66 +                                case None => null
    4.67 +                              }
    4.68 +                            case None => null
    4.69 +                          }
    4.70 +                        case _ => null
    4.71 +                      }
    4.72 +                    case _ => null
    4.73 +                  }
    4.74 +              })
    4.75            markup match {
    4.76              case Text.Info(_, Some(link)) #:: _ => link
    4.77              case _ => null
     5.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Jan 10 18:12:55 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Tue Jan 10 23:26:27 2012 +0100
     5.3 @@ -78,17 +78,21 @@
     5.4  
     5.5    /* markup selectors */
     5.6  
     5.7 -  val message =
     5.8 -    Markup_Tree.Select[Color](
     5.9 -      {
    5.10 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
    5.11 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
    5.12 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
    5.13 -      },
    5.14 -      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
    5.15 +  def message_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
    5.16 +    for {
    5.17 +      Text.Info(r, Some(color)) <-
    5.18 +        snapshot.select_markup(range,
    5.19 +          Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
    5.20 +          {
    5.21 +            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN, _), _)) => regular_color
    5.22 +            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), _)) => warning_color
    5.23 +            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_color
    5.24 +          })
    5.25 +    } yield Text.Info(r, color)
    5.26  
    5.27 -  val tooltip_message =
    5.28 -    Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
    5.29 +  def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
    5.30 +    snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
    5.31 +      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
    5.32        {
    5.33          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
    5.34          if markup == Isabelle_Markup.WRITELN ||
    5.35 @@ -96,50 +100,83 @@
    5.36              markup == Isabelle_Markup.ERROR =>
    5.37            msgs + (serial ->
    5.38              Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
    5.39 -      },
    5.40 -      Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
    5.41 +      }) match {
    5.42 +        case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
    5.43 +          Some(msgs.iterator.map(_._2).mkString("\n"))
    5.44 +        case _ => None
    5.45 +      }
    5.46  
    5.47 -  val gutter_message =
    5.48 -    Markup_Tree.Select[Icon](
    5.49 -      {
    5.50 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
    5.51 -          body match {
    5.52 -            case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
    5.53 -            case _ => warning_icon
    5.54 -          }
    5.55 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
    5.56 -      },
    5.57 -      Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)))
    5.58 +  def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
    5.59 +  {
    5.60 +    val icons =
    5.61 +      (for {
    5.62 +        Text.Info(_, Some(icon)) <-
    5.63 +          // FIXME snapshot.cumulate_markup
    5.64 +          snapshot.select_markup[Icon](range,
    5.65 +            Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
    5.66 +            {
    5.67 +              case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body)) =>
    5.68 +                body match {
    5.69 +                  case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => legacy_icon
    5.70 +                  case _ => warning_icon
    5.71 +                }
    5.72 +              case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _)) => error_icon
    5.73 +            })
    5.74 +        } yield icon).toList.sortWith(_ >= _)
    5.75 +    icons match {
    5.76 +      case icon :: _ => Some(icon)
    5.77 +      case Nil => None
    5.78 +    }
    5.79 +  }
    5.80  
    5.81 -  val background1 =
    5.82 -    Markup_Tree.Cumulate[(Option[Protocol.Status], Option[Color])](
    5.83 -      (Some(Protocol.Status()), None),
    5.84 -      {
    5.85 -        case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
    5.86 -        if (Protocol.command_status_markup(markup.name)) =>
    5.87 -          (Some(Protocol.command_status(status, markup)), color)
    5.88 -        case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
    5.89 -          (None, Some(bad_color))
    5.90 -        case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
    5.91 -          (None, Some(hilite_color))
    5.92 -      },
    5.93 -      Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE))
    5.94 +  def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
    5.95 +  {
    5.96 +    for {
    5.97 +      Text.Info(r, result) <-
    5.98 +        snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
    5.99 +          range, (Some(Protocol.Status()), None),
   5.100 +          Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
   5.101 +          {
   5.102 +            case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
   5.103 +            if (Protocol.command_status_markup(markup.name)) =>
   5.104 +              (Some(Protocol.command_status(status, markup)), color)
   5.105 +            case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
   5.106 +              (None, Some(bad_color))
   5.107 +            case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
   5.108 +              (None, Some(hilite_color))
   5.109 +          })
   5.110 +      color <-
   5.111 +        (result match {
   5.112 +          case (Some(status), _) =>
   5.113 +            if (status.is_running) Some(running1_color)
   5.114 +            else if (status.is_unprocessed) Some(unprocessed1_color)
   5.115 +            else None
   5.116 +          case (_, opt_color) => opt_color
   5.117 +        })
   5.118 +    } yield Text.Info(r, color)
   5.119 +  }
   5.120  
   5.121 -  val background2 =
   5.122 -    Markup_Tree.Select[Color](
   5.123 -      {
   5.124 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
   5.125 -      },
   5.126 -      Some(Set(Isabelle_Markup.TOKEN_RANGE)))
   5.127 +  def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   5.128 +    for {
   5.129 +      Text.Info(r, Some(color)) <-
   5.130 +        snapshot.select_markup(range,
   5.131 +          Some(Set(Isabelle_Markup.TOKEN_RANGE)),
   5.132 +          {
   5.133 +            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
   5.134 +          })
   5.135 +    } yield Text.Info(r, color)
   5.136  
   5.137 -  val foreground =
   5.138 -    Markup_Tree.Select[Color](
   5.139 -      {
   5.140 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
   5.141 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
   5.142 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
   5.143 -      },
   5.144 -      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)))
   5.145 +  def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
   5.146 +    for {
   5.147 +      Text.Info(r, Some(color)) <-
   5.148 +        snapshot.select_markup(range,
   5.149 +          Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
   5.150 +          {
   5.151 +            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
   5.152 +            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
   5.153 +            case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
   5.154 +          })
   5.155 +    } yield Text.Info(r, color)
   5.156  
   5.157    private val text_colors: Map[String, Color] =
   5.158      Map(
   5.159 @@ -166,13 +203,14 @@
   5.160        Isabelle_Markup.ML_MALFORMED -> get_color("#FF6A6A"),
   5.161        Isabelle_Markup.ANTIQ -> get_color("blue"))
   5.162  
   5.163 -  val text_color =
   5.164 -    Markup_Tree.Select[Color](
   5.165 +  private val text_color_elements = Set.empty[String] ++ text_colors.keys
   5.166 +
   5.167 +  def text_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Option[Color]]] =
   5.168 +    snapshot.select_markup(range, Some(text_color_elements),
   5.169        {
   5.170          case Text.Info(_, XML.Elem(Markup(m, _), _))
   5.171          if text_colors.isDefinedAt(m) => text_colors(m)
   5.172 -      },
   5.173 -      Some(Set() ++ text_colors.keys))
   5.174 +      })
   5.175  
   5.176    private val tooltips: Map[String, String] =
   5.177      Map(
   5.178 @@ -194,24 +232,32 @@
   5.179      Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
   5.180        margin = Isabelle.Int_Property("tooltip-margin"))
   5.181  
   5.182 -  val tooltip1 =
   5.183 -    Markup_Tree.Select[String](
   5.184 -      {
   5.185 -        case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) => kind + " " + quote(name)
   5.186 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
   5.187 -          string_of_typing("ML:", body)
   5.188 -        case Text.Info(_, XML.Elem(Markup(name, _), _))
   5.189 -        if tooltips.isDefinedAt(name) => tooltips(name)
   5.190 -      },
   5.191 -      Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys))
   5.192 +  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
   5.193 +  {
   5.194 +    val tip1 =
   5.195 +      snapshot.select_markup(range,
   5.196 +        Some(Set(Isabelle_Markup.ENTITY, Isabelle_Markup.ML_TYPING) ++ tooltips.keys),
   5.197 +        {
   5.198 +          case Text.Info(_, XML.Elem(Isabelle_Markup.Entity(kind, name), _)) =>
   5.199 +            kind + " " + quote(name)
   5.200 +          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body)) =>
   5.201 +            string_of_typing("ML:", body)
   5.202 +          case Text.Info(_, XML.Elem(Markup(name, _), _))
   5.203 +          if tooltips.isDefinedAt(name) => tooltips(name)
   5.204 +        })
   5.205 +    val tip2 =
   5.206 +      snapshot.select_markup(range, Some(Set(Isabelle_Markup.TYPING)),
   5.207 +        {
   5.208 +          case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
   5.209 +            string_of_typing("::", body)
   5.210 +        })
   5.211  
   5.212 -  val tooltip2 =
   5.213 -    Markup_Tree.Select[String](
   5.214 -      {
   5.215 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body)) =>
   5.216 -          string_of_typing("::", body)
   5.217 -      },
   5.218 -      Some(Set(Isabelle_Markup.TYPING)))
   5.219 +    val tips =
   5.220 +      (tip1 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil }) :::
   5.221 +      (tip2 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil })
   5.222 +
   5.223 +    if (tips.isEmpty) None else Some(tips.mkString("\n"))
   5.224 +  }
   5.225  
   5.226    private val subexp_include =
   5.227      Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
   5.228 @@ -220,13 +266,17 @@
   5.229        Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR, Isabelle_Markup.ML_SOURCE,
   5.230        Isabelle_Markup.DOC_SOURCE)
   5.231  
   5.232 -  val subexp =
   5.233 -    Markup_Tree.Select[(Text.Range, Color)](
   5.234 -      {
   5.235 -        case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   5.236 -          (range, subexp_color)
   5.237 -      },
   5.238 -      Some(subexp_include))
   5.239 +  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[(Text.Range, Color)] =
   5.240 +  {
   5.241 +    snapshot.select_markup(range, Some(subexp_include),
   5.242 +        {
   5.243 +          case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   5.244 +            (range, subexp_color)
   5.245 +        }) match {
   5.246 +      case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
   5.247 +      case _ => None
   5.248 +    }
   5.249 +  }
   5.250  
   5.251  
   5.252    /* token markup -- text styles */
     6.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Tue Jan 10 18:12:55 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Tue Jan 10 23:26:27 2012 +0100
     6.3 @@ -91,18 +91,7 @@
     6.4  
     6.5              // background color (1)
     6.6              for {
     6.7 -              Text.Info(range, result) <-
     6.8 -                snapshot.cumulate_markup(line_range)(Isabelle_Rendering.background1).iterator
     6.9 -              // FIXME more abstract Isabelle_Rendering.markup etc.
    6.10 -              val opt_color =
    6.11 -                result match {
    6.12 -                  case (Some(status), _) =>
    6.13 -                    if (status.is_running) Some(Isabelle_Rendering.running1_color)
    6.14 -                    else if (status.is_unprocessed) Some(Isabelle_Rendering.unprocessed1_color)
    6.15 -                    else None
    6.16 -                  case (_, color) => color
    6.17 -                }
    6.18 -              color <- opt_color
    6.19 +              Text.Info(range, color) <- Isabelle_Rendering.background1(snapshot, line_range)
    6.20                r <- Isabelle.gfx_range(text_area, range)
    6.21              } {
    6.22                gfx.setColor(color)
    6.23 @@ -111,8 +100,7 @@
    6.24  
    6.25              // background color (2)
    6.26              for {
    6.27 -              Text.Info(range, Some(color)) <-
    6.28 -                snapshot.select_markup(line_range)(Isabelle_Rendering.background2).iterator
    6.29 +              Text.Info(range, color) <- Isabelle_Rendering.background2(snapshot, line_range)
    6.30                r <- Isabelle.gfx_range(text_area, range)
    6.31              } {
    6.32                gfx.setColor(color)
    6.33 @@ -121,8 +109,7 @@
    6.34  
    6.35              // squiggly underline
    6.36              for {
    6.37 -              Text.Info(range, Some(color)) <-
    6.38 -                snapshot.select_markup(line_range)(Isabelle_Rendering.message).iterator
    6.39 +              Text.Info(range, color) <- Isabelle_Rendering.message_color(snapshot, line_range)
    6.40                r <- Isabelle.gfx_range(text_area, range)
    6.41              } {
    6.42                gfx.setColor(color)
    6.43 @@ -213,7 +200,7 @@
    6.44  
    6.45          val markup =
    6.46            for {
    6.47 -            r1 <- painter_snapshot.select_markup(chunk_range)(Isabelle_Rendering.text_color)
    6.48 +            r1 <- Isabelle_Rendering.text_color(painter_snapshot, chunk_range)
    6.49              r2 <- r1.try_restrict(chunk_range)
    6.50            } yield r2
    6.51  
    6.52 @@ -314,8 +301,7 @@
    6.53  
    6.54              // foreground color
    6.55              for {
    6.56 -              Text.Info(range, Some(color)) <-
    6.57 -                snapshot.select_markup(line_range)(Isabelle_Rendering.foreground).iterator
    6.58 +              Text.Info(range, color) <- Isabelle_Rendering.foreground(snapshot, line_range)
    6.59                r <- Isabelle.gfx_range(text_area, range)
    6.60              } {
    6.61                gfx.setColor(color)
     7.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Jan 10 18:12:55 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jan 10 23:26:27 2012 +0100
     7.3 @@ -178,7 +178,8 @@
     7.4            if (line_ctxt.isDefined && Isabelle.session.is_ready) {
     7.5              val syntax = Isabelle.session.current_syntax()
     7.6              val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
     7.7 -            val styled_tokens = tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))
     7.8 +            val styled_tokens =
     7.9 +              tokens.map(tok => (Isabelle_Rendering.token_markup(syntax, tok), tok))
    7.10              (styled_tokens, new Line_Context(Some(ctxt1)))
    7.11            }
    7.12            else {