# HG changeset patch
# User wenzelm
# Date 1392998808 -3600
# Node ID af028f35af60ca6c7e8192c2c141abbf23fe0b3c
# Parent  b657146dc030a059f681832f0372c86fef587c4a# Parent  5ff4742f27ec72fd57a875f6e191be86269ec433
merged

diff -r b657146dc030 -r af028f35af60 NEWS
--- a/NEWS	Fri Feb 21 12:33:49 2014 +0100
+++ b/NEWS	Fri Feb 21 17:06:48 2014 +0100
@@ -32,6 +32,11 @@
 * Improved support for Isabelle/ML, with jEdit mode "isabelle-ml" for
 auxiliary ML files.
 
+* Improved completion based on context information about embedded
+languages: keywords are only completed for outer syntax, symbols for
+languages that support them.  E.g. no symbol completion for ML source,
+but within ML strings, comments, antiquotations.
+
 * Document panel: simplied interaction where every single mouse click
 (re)opens document via desktop environment or as jEdit buffer.
 
diff -r b657146dc030 -r af028f35af60 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/General/antiquote.ML	Fri Feb 21 17:06:48 2014 +0100
@@ -32,7 +32,8 @@
 (* reports *)
 
 fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) =
-  [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
+  [(start, Markup.antiquote), (stop, Markup.antiquote),
+   (pos, Markup.antiquoted), (pos, Markup.language_antiquotation)];
 
 fun antiquote_reports text =
   maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq));
diff -r b657146dc030 -r af028f35af60 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Feb 21 17:06:48 2014 +0100
@@ -15,6 +15,8 @@
 object Command
 {
   type Edit = (Option[Command], Option[Command])
+  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
+
 
 
   /** accumulated results from prover **/
@@ -54,21 +56,60 @@
   }
 
 
+  /* markup */
+
+  object Markup_Index
+  {
+    val markup: Markup_Index = Markup_Index(false, "")
+  }
+
+  sealed case class Markup_Index(status: Boolean, file_name: String)
+
+  object Markups
+  {
+    val empty: Markups = new Markups(Map.empty)
+
+    def init(markup: Markup_Tree): Markups =
+      new Markups(Map(Markup_Index.markup -> markup))
+  }
+
+  final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
+  {
+    def apply(index: Markup_Index): Markup_Tree =
+      rep.getOrElse(index, Markup_Tree.empty)
+
+    def add(index: Markup_Index, markup: Text.Markup): Markups =
+      new Markups(rep + (index -> (this(index) + markup)))
+
+    def ++ (other: Markups): Markups =
+      new Markups(
+        (rep.keySet ++ other.rep.keySet)
+          .map(index => index -> (this(index) ++ other(index))).toMap)
+
+    override def hashCode: Int = rep.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Markups => rep == other.rep
+        case _ => false
+      }
+    override def toString: String = rep.iterator.mkString("Markups(", ", ", ")")
+  }
+
+
   /* state */
 
   sealed case class State(
     command: Command,
     status: List[Markup] = Nil,
     results: Results = Results.empty,
-    markups: Map[String, Markup_Tree] = Map.empty)
+    markups: Markups = Markups.empty)
   {
-    def get_markup(file_name: String): Markup_Tree =
-      markups.getOrElse(file_name, Markup_Tree.empty)
+    /* markup */
 
-    def markup: Markup_Tree = get_markup("")
+    def markup(index: Markup_Index): Markup_Tree = markups(index)
 
     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
-      markup.to_XML(command.range, command.source, filter)
+      markup(Markup_Index.markup).to_XML(command.range, command.source, filter)
 
 
     /* content */
@@ -79,10 +120,17 @@
       results == other.results &&
       markups == other.markups
 
-    private def add_status(st: Markup): State = copy(status = st :: status)
+    private def add_status(st: Markup): State =
+      copy(status = st :: status)
 
-    private def add_markup(file_name: String, m: Text.Markup): State =
-      copy(markups = markups + (file_name -> (get_markup(file_name) + m)))
+    private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
+    {
+      val markups1 =
+        if (status || Protocol.status_elements(m.info.name))
+          markups.add(Markup_Index(true, file_name), m)
+        else markups
+      copy(markups = markups1.add(Markup_Index(false, file_name), m))
+    }
 
     def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
       message match {
@@ -90,8 +138,9 @@
           (this /: msgs)((state, msg) =>
             msg match {
               case elem @ XML.Elem(markup, Nil) =>
-                state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
-
+                state.
+                  add_status(markup).
+                  add_markup(true, "", Text.Info(command.proper_range, elem))
               case _ =>
                 System.err.println("Ignored status message: " + msg)
                 state
@@ -111,8 +160,8 @@
                         case Some(range) =>
                           if (!range.is_singularity) {
                             val props = Position.purge(atts)
-                            state.add_markup(file_name,
-                              Text.Info(range, XML.Elem(Markup(name, props), args)))
+                            val info = Text.Info(range, XML.Elem(Markup(name, props), args))
+                            state.add_markup(false, file_name, info)
                           }
                           else state
                         case None => bad(); state
@@ -125,7 +174,7 @@
                   val range = command.proper_range
                   val props = Position.purge(atts)
                   val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
-                  state.add_markup("", info)
+                  state.add_markup(false, "", info)
 
                 case _ => /* FIXME bad(); */ state
               }
@@ -141,7 +190,7 @@
                 for {
                   (file_name, chunk) <- command.chunks
                   range <- Protocol.message_positions(command.id, alt_id, chunk, message)
-                } st = st.add_markup(file_name, Text.Info(range, message2))
+                } st = st.add_markup(false, file_name, Text.Info(range, message2))
               }
               st
 
@@ -155,9 +204,7 @@
       copy(
         status = other.status ::: status,
         results = results ++ other.results,
-        markups =
-          (markups.keySet ++ other.markups.keySet)
-            .map(a => a -> (get_markup(a) ++ other.get_markup(a))).toMap
+        markups = markups ++ other.markups
       )
   }
 
@@ -189,15 +236,7 @@
   def name(span: List[Token]): String =
     span.find(_.is_command) match { case Some(tok) => tok.source case _ => "" }
 
-  type Blob = Exn.Result[(Document.Node.Name, Option[(SHA1.Digest, File)])]
-
-  def apply(
-    id: Document_ID.Command,
-    node_name: Document.Node.Name,
-    blobs: List[Blob],
-    span: List[Token],
-    results: Results = Results.empty,
-    markup: Markup_Tree = Markup_Tree.empty): Command =
+  private def source_span(span: List[Token]): (String, List[Token]) =
   {
     val source: String =
       span match {
@@ -213,16 +252,30 @@
       span1 += Token(kind, s1)
       i += n
     }
-
-    new Command(id, node_name, blobs, span1.toList, source, results, markup)
+    (source, span1.toList)
   }
 
-  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
+  def apply(
+    id: Document_ID.Command,
+    node_name: Document.Node.Name,
+    blobs: List[Blob],
+    span: List[Token]): Command =
+  {
+    val (source, span1) = source_span(span)
+    new Command(id, node_name, blobs, span1, source, Results.empty, Markup_Tree.empty)
+  }
 
-  def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
-      : Command =
-    Command(id, Document.Node.Name.empty, Nil, List(Token(Token.Kind.UNPARSED, source)),
-      results, markup)
+  val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Nil, Nil)
+
+  def unparsed(
+    id: Document_ID.Command,
+    source: String,
+    results: Results,
+    markup: Markup_Tree): Command =
+  {
+    val (source1, span) = source_span(List(Token(Token.Kind.UNPARSED, source)))
+    new Command(id, Document.Node.Name.empty, Nil, span, source1, results, markup)
+  }
 
   def unparsed(source: String): Command =
     unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
@@ -316,7 +369,7 @@
   /* accumulated results */
 
   val init_state: Command.State =
-    Command.State(this, results = init_results, markups = Map("" -> init_markup))
+    Command.State(this, results = init_results, markups = Command.Markups.init(init_markup))
 
   val empty_state: Command.State = Command.State(this)
 }
diff -r b657146dc030 -r af028f35af60 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Feb 21 17:06:48 2014 +0100
@@ -357,6 +357,7 @@
     val state: State
     val version: Version
     val is_outdated: Boolean
+
     def convert(i: Text.Offset): Text.Offset
     def revert(i: Text.Offset): Text.Offset
     def convert(range: Text.Range): Text.Range
@@ -366,15 +367,19 @@
     val node: Node
     val thy_load_commands: List[Command]
     def eq_content(other: Snapshot): Boolean
-    def cumulate_markup[A](
+
+    def cumulate[A](
       range: Text.Range,
       info: A,
       elements: String => Boolean,
-      result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
-    def select_markup[A](
+      result: Command.State => (A, Text.Markup) => Option[A],
+      status: Boolean = false): List[Text.Info[A]]
+
+    def select[A](
       range: Text.Range,
       elements: String => Boolean,
-      result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
+      result: Command.State => Text.Markup => Option[A],
+      status: Boolean = false): List[Text.Info[A]]
   }
 
   type Assign_Update =
@@ -601,14 +606,14 @@
         val version = stable.version.get_finished
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
 
+
+        /* local node content */
+
         def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
         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))
 
-
-        /* local node content */
-
         val node_name = name
         val node = version.nodes(name)
 
@@ -629,38 +634,51 @@
           (thy_load_commands zip other.thy_load_commands).forall(eq_commands)
         }
 
-        def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
-          result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
+
+        /* cumulate markup */
+
+        def cumulate[A](
+          range: Text.Range,
+          info: A,
+          elements: String => Boolean,
+          result: Command.State => (A, Text.Markup) => Option[A],
+          status: Boolean = false): List[Text.Info[A]] =
         {
           val former_range = revert(range)
           thy_load_commands match {
             case thy_load_command :: _ =>
               val file_name = node_name.node
+              val markup_index = Command.Markup_Index(status, file_name)
               (for {
                 chunk <- thy_load_command.chunks.get(file_name).iterator
                 st = state.command_state(version, thy_load_command)
                 res = result(st)
-                Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A](
+                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
                   former_range.restrict(chunk.range), info, elements,
                   { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
                 ).iterator
               } yield Text.Info(convert(r0), a)).toList
 
             case _ =>
+              val markup_index = Command.Markup_Index(status, "")
               (for {
                 (command, command_start) <- node.command_range(former_range)
                 st = state.command_state(version, command)
                 res = result(st)
-                Text.Info(r0, a) <- st.markup.cumulate[A](
+                Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
                   (former_range - command_start).restrict(command.range), info, elements,
-                  { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
-                ).iterator
+                  {
+                    case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
+                  }).iterator
               } yield Text.Info(convert(r0 + command_start), a)).toList
           }
         }
 
-        def select_markup[A](range: Text.Range, elements: String => Boolean,
-          result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
+        def select[A](
+          range: Text.Range,
+          elements: String => Boolean,
+          result: Command.State => Text.Markup => Option[A],
+          status: Boolean = false): List[Text.Info[A]] =
         {
           def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
           {
@@ -671,7 +689,7 @@
                 case some => Some(some)
               }
           }
-          for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
+          for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status))
             yield Text.Info(r, x)
         }
       }
diff -r b657146dc030 -r af028f35af60 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Fri Feb 21 17:06:48 2014 +0100
@@ -28,6 +28,7 @@
   val language_prop: T
   val language_ML: T
   val language_document: T
+  val language_antiquotation: T
   val language_text: T
   val language_rail: T
   val bindingN: string val binding: T
@@ -255,9 +256,9 @@
 val language_type = language "type" true;
 val language_term = language "term" true;
 val language_prop = language "prop" true;
-
 val language_ML = language "ML" false;
 val language_document = language "document" false;
+val language_antiquotation = language "antiquotation" true;
 val language_text = language "text" true;
 val language_rail = language "rail" true;
 
diff -r b657146dc030 -r af028f35af60 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Feb 21 17:06:48 2014 +0100
@@ -38,53 +38,29 @@
 
   /* tree building blocks */
 
-  object Elements
-  {
-    val empty = new Elements(Set.empty)
-  }
-
-  final class Elements private(private val rep: Set[String])
-  {
-    def exists(pred: String => Boolean): Boolean = rep.exists(pred)
-
-    def + (name: String): Elements =
-      if (rep(name)) this
-      else new Elements(rep + name)
-
-    def + (elem: XML.Elem): Elements = this + elem.markup.name
-    def ++ (elems: Iterable[XML.Elem]): Elements = (this /: elems.iterator)(_ + _)
-
-    def ++ (other: Elements): Elements =
-      if (this eq other) this
-      else if (rep.isEmpty) other
-      else (this /: other.rep)(_ + _)
-  }
-
   object Entry
   {
     def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
-      Entry(markup.range, List(markup.info), Elements.empty + markup.info,
-        subtree, subtree.make_elements)
-
-    def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
-      Entry(range, rev_markups, Elements.empty ++ rev_markups,
-        subtree, subtree.make_elements)
+      Entry(markup.range, List(markup.info), subtree)
   }
 
   sealed case class Entry(
     range: Text.Range,
     rev_markup: List[XML.Elem],
-    elements: Elements,
-    subtree: Markup_Tree,
-    subtree_elements: Elements)
+    subtree: Markup_Tree)
   {
     def markup: List[XML.Elem] = rev_markup.reverse
 
-    def + (markup: Text.Markup): Entry =
-      copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info)
+    def filter_markup(pred: String => Boolean): List[XML.Elem] =
+    {
+      var result: List[XML.Elem] = Nil
+      for { elem <- rev_markup; if (pred(elem.name)) }
+        result ::= elem
+      result.toList
+    }
 
-    def \ (markup: Text.Markup): Entry =
-      copy(subtree = subtree + markup, subtree_elements = subtree_elements + markup.info)
+    def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
+    def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)
   }
 
   object Branches
@@ -154,10 +130,6 @@
     }
   }
 
-  def make_elements: Elements =
-    (Elements.empty /: branches)(
-      { case (elements, (_, entry)) => elements ++ entry.subtree_elements ++ entry.elements })
-
   def + (new_markup: Text.Markup): Markup_Tree =
   {
     val new_range = new_markup.range
@@ -230,8 +202,7 @@
       var y = x
       var changed = false
       for {
-        elem <- entry.markup
-        if elements(elem.name)
+        elem <- entry.filter_markup(elements)
         y1 <- result(y, Text.Info(entry.range, elem))
       } { y = y1; changed = true }
       if (changed) Some(y) else None
@@ -244,13 +215,10 @@
       stack match {
         case (parent, (range, entry) :: more) :: rest =>
           val subrange = range.restrict(root_range)
-          val subtree =
-            if (entry.subtree_elements.exists(elements))
-              entry.subtree.overlapping(subrange).toList
-            else Nil
+          val subtree = entry.subtree.overlapping(subrange).toList
           val start = subrange.start
 
-          (if (entry.elements.exists(elements)) results(parent.info, entry) else None) match {
+          results(parent.info, entry) match {
             case Some(res) =>
               val next = Text.Info(subrange, res)
               val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
diff -r b657146dc030 -r af028f35af60 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Feb 21 17:06:48 2014 +0100
@@ -63,10 +63,6 @@
     def is_failed: Boolean = failed
   }
 
-  val command_status_markup: Set[String] =
-    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
-      Markup.FINISHED, Markup.FAILED)
-
   def command_status(status: Status, markup: Markup): Status =
     markup match {
       case Markup(Markup.ACCEPTED, _) => status.copy(accepted = true)
@@ -81,6 +77,13 @@
   def command_status(markups: List[Markup]): Status =
     (Status.init /: markups)(command_status(_, _))
 
+  val command_status_elements: Set[String] =
+    Set(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
+      Markup.FINISHED, Markup.FAILED)
+
+  val status_elements: Set[String] =
+    command_status_elements + Markup.WARNING + Markup.ERROR
+
 
   /* command timing */
 
@@ -162,12 +165,12 @@
 
   /* result messages */
 
-  private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
+  private val clean_elements = Set(Markup.REPORT, Markup.NO_REPORT)
 
   def clean_message(body: XML.Body): XML.Body =
     body filter {
-      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name)
-      case XML.Elem(Markup(name, _), _) => !clean(name)
+      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean_elements(name)
+      case XML.Elem(Markup(name, _), _) => !clean_elements(name)
       case _ => true
     } map {
       case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
@@ -272,7 +275,8 @@
 
   /* reported positions */
 
-  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+  private val position_elements =
+    Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
 
   def message_positions(
     command_id: Document_ID.Command,
@@ -294,9 +298,9 @@
     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
         case XML.Wrapped_Elem(Markup(name, props), _, body) =>
-          body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
+          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
         case XML.Elem(Markup(name, props), body) =>
-          body.foldLeft(if (include_pos(name)) elem_positions(props, set) else set)(positions)
+          body.foldLeft(if (position_elements(name)) elem_positions(props, set) else set)(positions)
         case XML.Text(_) => set
       }
 
diff -r b657146dc030 -r af028f35af60 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Feb 21 17:06:48 2014 +0100
@@ -159,9 +159,10 @@
       case Some(snapshot) =>
         val root = data.root
         for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
-          Isabelle_Sidekick.swing_markup_tree(
-            snapshot.state.command_state(snapshot.version, command).markup, root,
-              (info: Text.Info[List[XML.Elem]]) =>
+          val markup =
+            snapshot.state.command_state(snapshot.version, command).
+              markup(Command.Markup_Index.markup)
+          Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
               {
                 val range = info.range + command_start
                 val content = command.source(info.range).replace('\n', ' ')
diff -r b657146dc030 -r af028f35af60 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 12:33:49 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 17:06:48 2014 +0100
@@ -146,6 +146,75 @@
     else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
     else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
     else JEditToken.KEYWORD1
+
+
+  /* markup elements */
+
+  private val completion_elements =
+    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+      Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
+      Markup.ML_STRING, Markup.ML_COMMENT)
+
+  private val highlight_elements =
+    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
+      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
+      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
+      Markup.VAR, Markup.TFREE, Markup.TVAR)
+
+  private val hyperlink_elements =
+    Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+
+  private val active_elements =
+    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
+      Markup.SENDBACK, Markup.SIMP_TRACE)
+
+  private val tooltip_message_elements =
+    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+
+  private val tooltip_descriptions =
+    Map(
+      Markup.TOKEN_RANGE -> "inner syntax token",
+      Markup.FREE -> "free variable",
+      Markup.SKOLEM -> "skolem variable",
+      Markup.BOUND -> "bound variable",
+      Markup.VAR -> "schematic variable",
+      Markup.TFREE -> "free type variable",
+      Markup.TVAR -> "schematic type variable")
+
+  private val tooltip_elements =
+    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
+      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
+      tooltip_descriptions.keys
+
+  private val gutter_elements =
+    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+
+  private val squiggly_elements =
+    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+
+  private val line_background_elements =
+    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE,
+      Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE,
+      Markup.INFORMATION)
+
+  private val separator_elements = Set(Markup.SEPARATOR)
+
+  private val background1_elements =
+    Protocol.command_status_elements + Markup.WRITELN_MESSAGE +
+      Markup.TRACING_MESSAGE + Markup.WARNING_MESSAGE +
+      Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
+      active_elements
+
+  private val background2_elements = Set(Markup.TOKEN_RANGE)
+
+  private val foreground_elements =
+    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
+      Markup.CARTOUCHE, Markup.ANTIQUOTED)
+
+  private val bullet_elements = Set(Markup.BULLET)
+
+  private val fold_depth_elements =
+    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
 }
 
 
@@ -202,14 +271,10 @@
 
   /* completion context */
 
-  private val completion_elements =
-    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
-      Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT)
-
   def completion_context(caret: Text.Offset): Option[Completion.Context] =
     if (caret > 0) {
       val result =
-        snapshot.select_markup(Text.Range(caret - 1, caret + 1), completion_elements, _ =>
+        snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ =>
           {
             case Text.Info(_, elem)
             if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
@@ -229,25 +294,22 @@
 
   /* command status overview */
 
-  val overview_limit = options.int("jedit_text_overview_limit")
-
-  private val overview_elements =
-    Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
+  def overview_limit: Int = options.int("jedit_text_overview_limit")
 
   def overview_color(range: Text.Range): Option[Color] =
   {
     if (snapshot.is_outdated) None
     else {
       val results =
-        snapshot.cumulate_markup[(Protocol.Status, Int)](
-          range, (Protocol.Status.init, 0), overview_elements, _ =>
+        snapshot.cumulate[(Protocol.Status, Int)](
+          range, (Protocol.Status.init, 0), Protocol.status_elements, _ =>
           {
             case ((status, pri), Text.Info(_, elem)) =>
-              if (Protocol.command_status_markup(elem.name))
+              if (Protocol.command_status_elements(elem.name))
                 Some((Protocol.command_status(status, elem.markup), pri))
               else
                 Some((status, pri max Rendering.message_pri(elem.name)))
-          })
+          }, status = true)
       if (results.isEmpty) None
       else {
         val (status, pri) =
@@ -267,15 +329,9 @@
 
   /* highlighted area */
 
-  private val highlight_elements =
-    Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
-      Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
-      Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
-      Markup.VAR, Markup.TFREE, Markup.TVAR)
-
   def highlight(range: Text.Range): Option[Text.Info[Color]] =
   {
-    snapshot.select_markup(range, highlight_elements, _ =>
+    snapshot.select(range, Rendering.highlight_elements, _ =>
       {
         case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
       }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
@@ -284,9 +340,6 @@
 
   /* hyperlinks */
 
-  private val hyperlink_elements =
-    Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
-
   private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
     if (Path.is_ok(name))
       Isabelle_System.source_file(Path.explode(name)).map(path =>
@@ -303,8 +356,8 @@
 
   def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
   {
-    snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
-      range, Vector.empty, hyperlink_elements, _ =>
+    snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
+      range, Vector.empty, Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
@@ -346,11 +399,8 @@
 
   /* active elements */
 
-  private val active_elements =
-    Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE)
-
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
-    snapshot.select_markup(range, active_elements, command_state =>
+    snapshot.select(range, Rendering.active_elements, command_state =>
       {
         case Text.Info(info_range, elem) =>
           if (elem.name == Markup.DIALOG) {
@@ -368,7 +418,7 @@
   def command_results(range: Text.Range): Command.Results =
   {
     val results =
-      snapshot.select_markup[Command.Results](range, _ => true, command_state =>
+      snapshot.select[Command.Results](range, _ => true, command_state =>
         { case _ => Some(command_state.results) }).map(_.info)
     (Command.Results.empty /: results)(_ ++ _)
   }
@@ -376,14 +426,11 @@
 
   /* tooltip messages */
 
-  private val tooltip_message_elements =
-    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
-
   def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
   {
     val results =
-      snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](
-        range, Nil, tooltip_message_elements, _ =>
+      snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
+        range, Nil, Rendering.tooltip_message_elements, _ =>
         {
           case (msgs, Text.Info(info_range,
             XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
@@ -410,25 +457,10 @@
 
   /* tooltips */
 
-  private val tooltips: Map[String, String] =
-    Map(
-      Markup.TOKEN_RANGE -> "inner syntax token",
-      Markup.FREE -> "free variable",
-      Markup.SKOLEM -> "skolem variable",
-      Markup.BOUND -> "bound variable",
-      Markup.VAR -> "schematic variable",
-      Markup.TFREE -> "free type variable",
-      Markup.TVAR -> "schematic type variable")
-
-  private val tooltip_elements =
-    Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
-      Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++
-      tooltips.keys
-
   private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
     Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
 
-  private val timing_threshold: Double = options.real("jedit_timing_threshold")
+  private def timing_threshold: Double = options.real("jedit_timing_threshold")
 
   def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
   {
@@ -443,8 +475,8 @@
     }
 
     val results =
-      snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
-        range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
+      snapshot.cumulate[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
+        range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
         {
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
@@ -471,9 +503,8 @@
           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
             Some(add(prev, r, (true, XML.Text("language: " + language))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
-            if (tooltips.isDefinedAt(name))
-              Some(add(prev, r, (true, XML.Text(tooltips(name)))))
-            else None
+            Rendering.tooltip_descriptions.get(name).
+              map(descr => add(prev, r, (true, XML.Text(descr))))
         }).map(_.info)
 
     results.map(_.info).flatMap(res => res._2.toList) match {
@@ -485,7 +516,7 @@
     }
   }
 
-  val tooltip_margin: Int = options.int("jedit_tooltip_margin")
+  def tooltip_margin: Int = options.int("jedit_tooltip_margin")
 
   lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
   lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
@@ -499,13 +530,10 @@
     Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
     Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
 
-  private val gutter_elements =
-    Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
-
   def gutter_message(range: Text.Range): Option[Icon] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, gutter_elements, _ =>
+      snapshot.cumulate[Int](range, 0, Rendering.gutter_elements, _ =>
         {
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
               List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
@@ -528,18 +556,16 @@
 
   /* squiggly underline */
 
-  private val squiggly_colors = Map(
+  private lazy val squiggly_colors = Map(
     Rendering.writeln_pri -> writeln_color,
     Rendering.information_pri -> information_color,
     Rendering.warning_pri -> warning_color,
     Rendering.error_pri -> error_color)
 
-  private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
-
   def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, squiggly_elements, _ =>
+      snapshot.cumulate[Int](range, 0, Rendering.squiggly_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) =>
             if (Protocol.is_information(elem))
@@ -556,21 +582,17 @@
 
   /* message output */
 
-  private val message_colors = Map(
+  private lazy val message_colors = Map(
     Rendering.writeln_pri -> writeln_message_color,
     Rendering.information_pri -> information_message_color,
     Rendering.tracing_pri -> tracing_message_color,
     Rendering.warning_pri -> warning_message_color,
     Rendering.error_pri -> error_message_color)
 
-  private val line_background_elements =
-    Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE,
-      Markup.ERROR_MESSAGE, Markup.INFORMATION)
-
   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
+      snapshot.cumulate[Int](range, 0, Rendering.line_background_elements, _ =>
         {
           case (pri, Text.Info(_, elem)) =>
             if (elem.name == Markup.INFORMATION)
@@ -582,7 +604,7 @@
 
     val is_separator =
       pri > 0 &&
-      snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
+      snapshot.cumulate[Boolean](range, false, Rendering.separator_elements, _ =>
         {
           case _ => Some(true)
         }).exists(_.info)
@@ -596,38 +618,34 @@
 
   /* text background */
 
-  private val background1_elements =
-    Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
-      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
-      active_elements
-
   def background1(range: Text.Range): List[Text.Info[Color]] =
   {
     if (snapshot.is_outdated) List(Text.Info(range, outdated_color))
     else
       for {
         Text.Info(r, result) <-
-          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
-            range, (Some(Protocol.Status.init), None), background1_elements, command_state =>
-            {
-              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
-              if (Protocol.command_status_markup(markup.name)) =>
-                Some((Some(Protocol.command_status(status, markup)), color))
-              case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
-                Some((None, Some(bad_color)))
-              case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
-                Some((None, Some(intensify_color)))
-              case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
-                command_state.results.get(serial) match {
-                  case Some(Protocol.Dialog_Result(res)) if res == result =>
-                    Some((None, Some(active_result_color)))
-                  case _ =>
-                    Some((None, Some(active_color)))
-                }
-              case (_, Text.Info(_, elem)) =>
-                if (active_elements(elem.name)) Some((None, Some(active_color)))
-                else None
-            })
+          snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
+            range, (Some(Protocol.Status.init), None), Rendering.background1_elements,
+            command_state =>
+              {
+                case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
+                if (Protocol.command_status_elements(markup.name)) =>
+                  Some((Some(Protocol.command_status(status, markup)), color))
+                case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
+                  Some((None, Some(bad_color)))
+                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
+                  Some((None, Some(intensify_color)))
+                case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
+                  command_state.results.get(serial) match {
+                    case Some(Protocol.Dialog_Result(res)) if res == result =>
+                      Some((None, Some(active_result_color)))
+                    case _ =>
+                      Some((None, Some(active_color)))
+                  }
+                case (_, Text.Info(_, elem)) =>
+                  if (Rendering.active_elements(elem.name)) Some((None, Some(active_color)))
+                  else None
+              })
         color <-
           (result match {
             case (Some(status), opt_color) =>
@@ -640,16 +658,13 @@
   }
 
   def background2(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ => _ => Some(light_color))
+    snapshot.select(range, Rendering.background2_elements, _ => _ => Some(light_color))
 
 
   /* text foreground */
 
-  private val foreground_elements =
-    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
-
   def foreground(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select_markup(range, foreground_elements, _ =>
+    snapshot.select(range, Rendering.foreground_elements, _ =>
       {
         case Text.Info(_, elem) =>
           if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
@@ -658,7 +673,7 @@
 
   /* text color */
 
-  private val text_colors: Map[String, Color] = Map(
+  private lazy val text_colors: Map[String, Color] = Map(
       Markup.KEYWORD1 -> keyword1_color,
       Markup.KEYWORD2 -> keyword2_color,
       Markup.STRING -> Color.BLACK,
@@ -687,13 +702,13 @@
       Markup.ML_STRING -> inner_quoted_color,
       Markup.ML_COMMENT -> inner_comment_color)
 
-  private val text_color_elements = text_colors.keySet
+  private lazy val text_color_elements = text_colors.keySet
 
   def text_color(range: Text.Range, color: Color): List[Text.Info[Color]] =
   {
     if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
     else
-      snapshot.cumulate_markup(range, color, text_color_elements, _ =>
+      snapshot.cumulate(range, color, text_color_elements, _ =>
         {
           case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
         })
@@ -703,16 +718,13 @@
   /* virtual bullets */
 
   def bullet(range: Text.Range): List[Text.Info[Color]] =
-    snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color))
+    snapshot.select(range, Rendering.bullet_elements, _ => _ => Some(bullet_color))
 
 
   /* text folds */
 
-  private val fold_depth_elements =
-    Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
-
   def fold_depth(range: Text.Range): List[Text.Info[Int]] =
-    snapshot.cumulate_markup[Int](range, 0, fold_depth_elements, _ =>
+    snapshot.cumulate[Int](range, 0, Rendering.fold_depth_elements, _ =>
       {
         case (depth, _) => Some(depth + 1)
       })