# HG changeset patch
# User wenzelm
# Date 1321125249 -3600
# Node ID 6f9e24376ffd577eaef10fa49b4d9108aa708e25
# Parent  b2b087c20e453edf4b29bf316d9c3315bbdc1d15# Parent  f793dd5d84b23a64aa996e5ec19c1cf9d6ba996d
merged

diff -r b2b087c20e45 -r 6f9e24376ffd src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Sat Nov 12 13:01:56 2011 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy	Sat Nov 12 20:14:09 2011 +0100
@@ -1071,25 +1071,16 @@
 done
 
 lemma member_of_Package: 
- "\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk> 
-  \<Longrightarrow> pid (declclass m) = pid C" 
-proof -
-  assume   member: "G\<turnstile>m member_of C"
-  then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C")
-  proof (induct rule: members.induct)
-    fix C m
-    assume     C: "declclass m = C"
-    then show "pid (declclass m) = pid C"
-      by simp
-  next
-    fix C S m  
-    assume inheritable: "G \<turnstile> m inheritable_in pid C"
-    assume         hyp: "PROP ?P m S" and
-           package_acc: "accmodi m = Package" 
-    with inheritable package_acc hyp
-    show "pid (declclass m) = pid C" 
-      by (auto simp add: inheritable_in_def)
-  qed
+  assumes "G\<turnstile>m member_of C"
+    and "accmodi m = Package"
+  shows "pid (declclass m) = pid C"
+  using assms
+proof induct
+  case Immediate
+  then show ?case by simp
+next
+  case Inherited
+  then show ?case by (auto simp add: inheritable_in_def)
 qed
 
 lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)"
@@ -1581,19 +1572,14 @@
 apply (force elim: imethds_norec intro: rtrancl_into_rtrancl2)
 done
 
-lemma imethds_cases [consumes 3, case_names NewMethod InheritedMethod]:
-  assumes im: "im \<in> imethds G I sig" and  
-         ifI: "iface G I = Some i" and
-          ws: "ws_prog G" and
-     hyp_new:  "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig 
-                = Some im \<Longrightarrow> P" and
-     hyp_inh: "\<And> J. \<lbrakk>J \<in> set (isuperIfs i); im \<in> imethds G J sig\<rbrakk> \<Longrightarrow> P"
-  shows P
-proof -
-  from ifI ws im hyp_new hyp_inh
-  show "P"
-    by (auto simp add: imethds_rec)
-qed
+lemma imethds_cases:
+  assumes im: "im \<in> imethds G I sig"
+    and ifI: "iface G I = Some i"
+    and ws: "ws_prog G"
+  obtains (NewMethod) "table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)) sig = Some im"
+    | (InheritedMethod) J where "J \<in> set (isuperIfs i)" and "im \<in> imethds G J sig"
+using assms by (auto simp add: imethds_rec)
+
 
 subsection "accimethd"
 
@@ -1758,7 +1744,7 @@
 lemma accmethd_SomeD:
 "accmethd G S C sig = Some m
  \<Longrightarrow> methd G C sig = Some m \<and> G\<turnstile>method sig m of C accessible_from S"
-by (auto simp add: accmethd_def dest: filter_tab_SomeD)
+by (auto simp add: accmethd_def)
 
 lemma accmethd_SomeI:
 "\<lbrakk>methd G C sig = Some m; G\<turnstile>method sig m of C accessible_from S\<rbrakk> 
@@ -1836,13 +1822,13 @@
       next
         case (Some statM)
         note statM = Some
-        let "?filter C" = 
-              "filter_tab
+        let ?filter = 
+              "\<lambda>C. filter_tab
                 (\<lambda>_ dynM. G,sig \<turnstile> dynM overrides statM \<or> dynM = statM)
                 (methd G C)"
-        let "?class_rec C" =
-              "(class_rec G C empty
-                           (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C)))"
+        let ?class_rec =
+              "\<lambda>C. class_rec G C empty
+                           (\<lambda>C c subcls_mthds. subcls_mthds ++ (?filter C))"
         from statM Subcls ws subclseq_dynC_statC
         have dynmethd_dynC_def:
              "?Dynmethd_def dynC sig =
@@ -1924,18 +1910,19 @@
   \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C statC \<and> (\<exists> statM. methd G statC sig = Some statM)"
 by (auto simp add: dynmethd_rec)
  
-lemma dynmethd_Some_cases [consumes 3, case_names Static Overrides]:
-  assumes      dynM: "dynmethd G statC dynC sig = Some dynM" and
-        is_cls_dynC: "is_class G dynC" and
-                 ws: "ws_prog G" and
-         hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
-       hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;dynM\<noteq>statM;
-                       G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
-  shows P
+lemma dynmethd_Some_cases:
+  assumes dynM: "dynmethd G statC dynC sig = Some dynM"
+    and is_cls_dynC: "is_class G dynC"
+    and ws: "ws_prog G"
+  obtains (Static) "methd G statC sig = Some dynM"
+    | (Overrides) statM
+      where "methd G statC sig = Some statM"
+        and "dynM \<noteq> statM"
+        and "G,sig\<turnstile>dynM overrides statM"
 proof -
   from is_cls_dynC obtain dc where clsDynC: "class G dynC = Some dc" by blast
-  from clsDynC ws dynM hyp_static hyp_override
-  show "P"
+  from clsDynC ws dynM Static Overrides
+  show ?thesis
   proof (induct rule: ws_class_induct)
     case (Object co)
     with ws  have "statC = Object" 
@@ -1972,25 +1959,20 @@
 qed
 
 
-lemma dynmethd_Some_rec_cases [consumes 3, 
-                               case_names Static Override  Recursion]:
-  assumes          dynM: "dynmethd G statC dynC sig = Some dynM" and
-                clsDynC: "class G dynC = Some c" and
-                     ws: "ws_prog G" and
-             hyp_static: "methd G statC sig = Some dynM \<Longrightarrow> P" and
-           hyp_override: "\<And> statM. \<lbrakk>methd G statC sig = Some statM;
-                                     methd G dynC sig = Some dynM; statM\<noteq>dynM;
-                                     G,sig\<turnstile> dynM overrides statM\<rbrakk> \<Longrightarrow> P" and
-
-          hyp_recursion: "\<lbrakk>dynC\<noteq>Object;
-                           dynmethd G statC (super c) sig = Some dynM\<rbrakk> \<Longrightarrow> P"
-  shows P
+lemma dynmethd_Some_rec_cases:
+  assumes dynM: "dynmethd G statC dynC sig = Some dynM"
+    and clsDynC: "class G dynC = Some c"
+    and ws: "ws_prog G"
+  obtains (Static) "methd G statC sig = Some dynM"
+    | (Override) statM where "methd G statC sig = Some statM"
+        and "methd G dynC sig = Some dynM" and "statM \<noteq> dynM"
+        and "G,sig\<turnstile> dynM overrides statM"
+    | (Recursion) "dynC \<noteq> Object" and "dynmethd G statC (super c) sig = Some dynM"
 proof -
-  from clsDynC have "is_class G dynC" by simp
-  note no_override_in_Object' = no_override_in_Object [OF dynM this ws]
-  from ws clsDynC dynM hyp_static hyp_override hyp_recursion
+  from clsDynC have *: "is_class G dynC" by simp
+  from ws clsDynC dynM Static Override Recursion
   show ?thesis
-    by (auto simp add: dynmethd_rec dest: no_override_in_Object')
+    by (auto simp add: dynmethd_rec dest: no_override_in_Object [OF dynM * ws])
 qed
 
 lemma dynmethd_declC: 
@@ -2095,24 +2077,22 @@
   qed
 qed
 
-lemma dynmethd_cases [consumes 4, case_names Static Overrides]:
-  assumes     statM: "methd G statC sig = Some statM" and 
-           subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and
-       is_cls_statC: "is_class G statC" and
-                 ws: "ws_prog G" and
-         hyp_static: "dynmethd G statC dynC sig = Some statM \<Longrightarrow> P" and
-       hyp_override: "\<And> dynM. \<lbrakk>dynmethd G statC dynC sig = Some dynM;
-                                 dynM\<noteq>statM;
-                           G,sig\<turnstile>dynM overrides statM\<rbrakk> \<Longrightarrow> P"
-  shows P
+lemma dynmethd_cases:
+  assumes statM: "methd G statC sig = Some statM"
+    and subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC"
+    and is_cls_statC: "is_class G statC"
+    and ws: "ws_prog G"
+  obtains (Static) "dynmethd G statC dynC sig = Some statM"
+    | (Overrides) dynM where "dynmethd G statC dynC sig = Some dynM"
+        and "dynM \<noteq> statM" and "G,sig\<turnstile>dynM overrides statM"
 proof -
+  note hyp_static = Static and hyp_override = Overrides
   from subclseq is_cls_statC 
   have is_cls_dynC: "is_class G dynC" by (rule subcls_is_class2)
   then obtain dc where
     clsDynC: "class G dynC = Some dc" by blast
   from statM subclseq is_cls_statC ws 
-  obtain dynM
-    where dynM: "dynmethd G statC dynC sig = Some dynM"
+  obtain dynM where dynM: "dynmethd G statC dynC sig = Some dynM"
     by (blast dest: methd_Some_dynmethd_Some)
   from dynM is_cls_dynC ws 
   show ?thesis
@@ -2151,14 +2131,13 @@
 
 subsection "dynlookup"
 
-lemma dynlookup_cases [consumes 1, case_names NullT IfaceT ClassT ArrayT]:
-"\<lbrakk>dynlookup G statT dynC sig = x;
-           \<lbrakk>statT = NullT       ; empty sig = x                  \<rbrakk> \<Longrightarrow> P;
-  \<And> I.    \<lbrakk>statT = IfaceT I    ; dynimethd G I      dynC sig = x\<rbrakk> \<Longrightarrow> P;
-  \<And> statC.\<lbrakk>statT = ClassT statC; dynmethd  G statC  dynC sig = x\<rbrakk> \<Longrightarrow> P;
-  \<And> ty.   \<lbrakk>statT = ArrayT ty   ; dynmethd  G Object dynC sig = x\<rbrakk> \<Longrightarrow> P
- \<rbrakk> \<Longrightarrow> P"
-by (cases statT) (auto simp add: dynlookup_def)
+lemma dynlookup_cases:
+  assumes "dynlookup G statT dynC sig = x"
+  obtains (NullT) "statT = NullT" and "empty sig = x"
+    | (IfaceT) I where "statT = IfaceT I" and "dynimethd G I dynC sig = x"
+    | (ClassT) statC where "statT = ClassT statC" and "dynmethd G statC dynC sig = x"
+    | (ArrayT) ty where "statT = ArrayT ty" and "dynmethd G Object dynC sig = x"
+using assms by (cases statT) (auto simp add: dynlookup_def)
 
 subsection "fields"
 
diff -r b2b087c20e45 -r 6f9e24376ffd src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Nov 12 20:14:09 2011 +0100
@@ -240,9 +240,8 @@
     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](info: Text.Info[A])(result: Markup_Tree.Cumulate[A])
-      : Stream[Text.Info[A]]
-    def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+    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]]]
   }
 
@@ -473,34 +472,37 @@
         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](root: Text.Info[A])(result: Markup_Tree.Cumulate[A])
+        def cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A])
           : Stream[Text.Info[A]] =
         {
-          val former_range = revert(root.range)
+          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(Text.Info((former_range - command_start).restrict(command.range), root.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)))
-              }
+              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))
           } yield Text.Info(convert(r0 + command_start), a)
         }
 
-        def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+        def select_markup[A](range: Text.Range)(body: Markup_Tree.Select[A])
           : Stream[Text.Info[Option[A]]] =
         {
-          val former_range = revert(range)
-          for {
-            (command, command_start) <- node.command_range(former_range).toStream
-            Text.Info(r0, x) <- command_state(command).markup.
-              select((former_range - command_start).restrict(command.range)) {
-                case Text.Info(r0, info)
-                if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
-                  result(Text.Info(convert(r0 + command_start), info))
-              }
-          } yield Text.Info(convert(r0 + command_start), x)
+          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))
         }
       }
     }
diff -r b2b087c20e45 -r 6f9e24376ffd src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 20:14:09 2011 +0100
@@ -15,25 +15,46 @@
 
 object Markup_Tree
 {
-  type Cumulate[A] = PartialFunction[(A, Text.Markup), A]
-  type Select[A] = PartialFunction[Text.Markup, A]
+  sealed case class Cumulate[A](
+    info: A, result: PartialFunction[(A, Text.Markup), A], elements: Option[Set[String]])
+  sealed case class Select[A](
+    result: PartialFunction[Text.Markup, A], elements: Option[Set[String]])
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
 
+  object Entry
+  {
+    def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
+      Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
+  }
+
+  sealed case class Entry(
+    range: Text.Range,
+    rev_markup: List[XML.Elem],
+    elements: Set[String],
+    subtree: Markup_Tree)
+  {
+    def + (info: XML.Elem): Entry =
+      if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup)
+      else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
+
+    def markup: List[XML.Elem] = rev_markup.reverse
+  }
+
   object Branches
   {
-    type Entry = (Text.Markup, Markup_Tree)
     type T = SortedMap[Text.Range, Entry]
-
     val empty: T = SortedMap.empty(Text.Range.Ordering)
-    def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
-    def single(entry: Entry): T = update(empty, entry)
   }
 }
 
 
 class Markup_Tree private(branches: Markup_Tree.Branches.T)
 {
+  private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
+    this(branches + (entry.range -> entry))
+
+
   import Markup_Tree._
 
   override def toString =
@@ -42,104 +63,85 @@
       case list => list.mkString("Tree(", ",", ")")
     }
 
-  private def overlapping(range: Text.Range): Branches.T =  // FIXME special cases!?
+  private def overlapping(range: Text.Range): Branches.T =
   {
     val start = Text.Range(range.start)
     val stop = Text.Range(range.stop)
     val bs = branches.range(start, stop)
     // FIXME check after Scala 2.8.x
     branches.get(stop) match {
-      case Some(end) if range overlaps end._1.range => Branches.update(bs, end)
+      case Some(end) if range overlaps end.range => bs + (end.range -> end)
       case _ => bs
     }
   }
 
-  def + (new_info: Text.Markup): Markup_Tree =
+  def + (new_markup: Text.Markup): Markup_Tree =
   {
-    val new_range = new_info.range
+    val new_range = new_markup.range
+
     branches.get(new_range) match {
-      case None =>
-        new Markup_Tree(Branches.update(branches, new_info -> empty))
-      case Some((info, subtree)) =>
-        val range = info.range
-        if (range.contains(new_range))
-          new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
+      case None => new Markup_Tree(branches, Entry(new_markup, empty))
+      case Some(entry) =>
+        if (entry.range == new_range)
+          new Markup_Tree(branches, entry + new_markup.info)
+        else if (entry.range.contains(new_range))
+          new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
         else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
-          new Markup_Tree(Branches.single(new_info -> this))
+          new Markup_Tree(Branches.empty, Entry(new_markup, this))
         else {
           val body = overlapping(new_range)
           if (body.forall(e => new_range.contains(e._1))) {
-            val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0
+            val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0 FIXME
               if (body.size > 1)
                 (Branches.empty /: branches)((rest, entry) =>
                   if (body.isDefinedAt(entry._1)) rest else rest + entry)
               else branches
-            new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
+            new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
           }
           else { // FIXME split markup!?
-            System.err.println("Ignored overlapping markup information: " + new_info)
+            System.err.println("Ignored overlapping markup information: " + new_markup)
             this
           }
         }
     }
   }
 
-  def cumulate[A](root: Text.Info[A])(result: Cumulate[A]): Stream[Text.Info[A]] =
+  def cumulate[A](root_range: Text.Range)(body: Cumulate[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 }) {
+        val (y, changed) =
+          (entry.markup :\ (x, false))((info, res) =>
+            {
+              val (y, changed) = res
+              val arg = (x, Text.Info(entry.range, info))
+              if (body.result.isDefinedAt(arg)) (body.result(arg), true)
+              else res
+            })
+        if (changed) Some(y) else None
+      }
+      else None
+
     def stream(
       last: Text.Offset,
-      stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]): Stream[Text.Info[A]] =
+      stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] =
     {
       stack match {
-        case (parent, (range, (info, tree)) #:: more) :: rest =>
-          val subrange = range.restrict(root.range)
-          val subtree = tree.overlapping(subrange).toStream
+        case (parent, (range, entry) #:: more) :: rest =>
+          val subrange = range.restrict(root_range)
+          val subtree = entry.subtree.overlapping(subrange).toStream
           val start = subrange.start
 
-          val arg = (parent.info, info)
-          if (result.isDefinedAt(arg)) {
-            val next = Text.Info(subrange, result(arg))
-            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
-            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
-            else nexts
+          result(parent.info, entry) match {
+            case Some(res) =>
+              val next = Text.Info(subrange, res)
+              val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
+              if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
+              else nexts
+            case None => stream(last, (parent, subtree #::: more) :: rest)
           }
-          else stream(last, (parent, subtree #::: more) :: rest)
-
-        case (parent, Stream.Empty) :: rest =>
-          val stop = parent.range.stop
-          val nexts = stream(stop, rest)
-          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
-          else nexts
-
-        case Nil =>
-          val stop = root.range.stop
-          if (last < stop) Stream(root.restrict(Text.Range(last, stop)))
-          else Stream.empty
-      }
-    }
-    stream(root.range.start, List((root, overlapping(root.range).toStream)))
-  }
-
-  def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
-  {
-    def stream(
-      last: Text.Offset,
-      stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
-        : Stream[Text.Info[Option[A]]] =
-    {
-      stack match {
-        case (parent, (range, (info, tree)) #:: more) :: rest =>
-          val subrange = range.restrict(root_range)
-          val subtree = tree.overlapping(subrange).toStream
-          val start = subrange.start
-
-          if (result.isDefinedAt(info)) {
-            val next = Text.Info[Option[A]](subrange, Some(result(info)))
-            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
-            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
-            else nexts
-          }
-          else stream(last, (parent, subtree #::: more) :: rest)
 
         case (parent, Stream.Empty) :: rest =>
           val stop = parent.range.stop
@@ -149,21 +151,25 @@
 
         case Nil =>
           val stop = root_range.stop
-          if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
+          if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
           else Stream.empty
       }
     }
     stream(root_range.start,
-      List((Text.Info(root_range, None), overlapping(root_range).toStream)))
+      List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
   }
 
   def swing_tree(parent: DefaultMutableTreeNode)
     (swing_node: Text.Markup => DefaultMutableTreeNode)
   {
-    for ((_, (info, subtree)) <- branches) {
-      val current = swing_node(info)
-      subtree.swing_tree(current)(swing_node)
-      parent.add(current)
+    for ((_, entry) <- branches) {
+      var current = parent
+      for (info <- entry.markup) {
+        val node = swing_node(Text.Info(entry.range, info))
+        current.add(node)
+        current = node
+      }
+      entry.subtree.swing_tree(current)(swing_node)
     }
   }
 }
diff -r b2b087c20e45 -r 6f9e24376ffd src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Pure/PIDE/text.scala	Sat Nov 12 20:14:09 2011 +0100
@@ -115,7 +115,7 @@
       catch { case ERROR(_) => None }
   }
 
-  type Markup = Info[XML.Tree]
+  type Markup = Info[XML.Elem]
 
 
   /* editing */
diff -r b2b087c20e45 -r 6f9e24376ffd src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Pure/variable.ML	Sat Nov 12 20:14:09 2011 +0100
@@ -297,7 +297,6 @@
 
 val fixed_ord = Name_Space.entry_ord o fixes_space;
 val intern_fixed = Name_Space.intern o fixes_space;
-val markup_fixed = Name_Space.markup o fixes_space;
 
 fun lookup_fixed ctxt x =
   let val x' = intern_fixed ctxt x
@@ -308,6 +307,10 @@
     SOME x' => if intern_fixed ctxt x' = x then x' else x
   | NONE => x);
 
+fun markup_fixed ctxt x =
+  Name_Space.markup (fixes_space ctxt) x
+  |> Markup.name (revert_fixed ctxt x);
+
 fun dest_fixes ctxt =
   let val (space, tab) = fixes_of ctxt
   in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
diff -r b2b087c20e45 -r 6f9e24376ffd src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Nov 12 20:14:09 2011 +0100
@@ -293,8 +293,7 @@
           else Isabelle.tooltip(tooltips.mkString("\n"))
         }
         else {
-          snapshot.cumulate_markup(Text.Info(range, SortedMap.empty[Long, String]))(
-            Isabelle_Markup.tooltip_message) match
+          snapshot.cumulate_markup(range)(Isabelle_Markup.tooltip_message) match
           {
             case Text.Info(_, msgs) #:: _ if !msgs.isEmpty =>
               Isabelle.tooltip(msgs.iterator.map(_._2).mkString("\n"))
diff -r b2b087c20e45 -r 6f9e24376ffd src/Tools/jEdit/src/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Sat Nov 12 20:14:09 2011 +0100
@@ -57,37 +57,40 @@
         case Some(model) =>
           val snapshot = model.snapshot()
           val markup =
-            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
-              // FIXME Isar_Document.Hyperlink extractor
-              case Text.Info(info_range,
-                  XML.Elem(Markup(Markup.ENTITY, props), _))
-                if (props.find(
-                  { case (Markup.KIND, Markup.ML_OPEN) => true
-                    case (Markup.KIND, 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))
+            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1))(
+              Markup_Tree.Select[Hyperlink](
+                {
+                  // FIXME Isar_Document.Hyperlink extractor
+                  case Text.Info(info_range,
+                      XML.Elem(Markup(Markup.ENTITY, props), _))
+                    if (props.find(
+                      { case (Markup.KIND, Markup.ML_OPEN) => true
+                        case (Markup.KIND, 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 None => null
+                          case _ => null
                         }
                       case _ => null
                     }
-                  case _ => null
-                }
-            }
+                },
+                Some(Set(Markup.ENTITY))))
           markup match {
             case Text.Info(_, Some(link)) #:: _ => link
             case _ => null
diff -r b2b087c20e45 -r 6f9e24376ffd src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 13:01:56 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 20:14:09 2011 +0100
@@ -87,48 +87,60 @@
 
   /* markup selectors */
 
-  val message: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
-    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
-    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
-  }
+  val message =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
+        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
+        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
+      },
+      Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
 
-  val tooltip_message: Markup_Tree.Cumulate[SortedMap[Long, String]] =
-  {
-    case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
-    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
-      msgs + (serial ->
-        Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
-  }
+  val tooltip_message =
+    Markup_Tree.Cumulate[SortedMap[Long, String]](SortedMap.empty,
+      {
+        case (msgs, Text.Info(_, msg @ XML.Elem(Markup(markup, Markup.Serial(serial)), _)))
+        if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
+          msgs + (serial ->
+            Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")))
+      },
+      Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)))
 
-  val gutter_message: Markup_Tree.Select[Icon] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
-      body match {
-        case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
-        case _ => warning_icon
-      }
-    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
-  }
+  val gutter_message =
+    Markup_Tree.Select[Icon](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
+          body match {
+            case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
+            case _ => warning_icon
+          }
+        case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+      },
+      Some(Set(Markup.WARNING, Markup.ERROR)))
 
-  val background1: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
-    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
-  }
+  val background1 =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+        case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
+      },
+      Some(Set(Markup.BAD, Markup.HILITE)))
 
-  val background2: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
-  }
+  val background2 =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
+      },
+      Some(Set(Markup.TOKEN_RANGE)))
 
-  val foreground: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
-    case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
-    case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
-  }
+  val foreground =
+    Markup_Tree.Select[Color](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
+        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
+      },
+      Some(Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM)))
 
   private val text_colors: Map[String, Color] =
     Map(
@@ -155,10 +167,13 @@
       Markup.ML_MALFORMED -> get_color("#FF6A6A"),
       Markup.ANTIQ -> get_color("blue"))
 
-  val text_color: Markup_Tree.Select[Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(m, _), _)) if text_colors.isDefinedAt(m) => text_colors(m)
-  }
+  val text_color =
+    Markup_Tree.Select[Color](
+      {
+        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(
@@ -180,29 +195,36 @@
     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(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
-    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => string_of_typing("ML:", body)
-    case Text.Info(_, XML.Elem(Markup(name, _), _))
-    if tooltips.isDefinedAt(name) => tooltips(name)
-  }
+  val tooltip1 =
+    Markup_Tree.Select[String](
+      {
+        case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
+        case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+          string_of_typing("ML:", body)
+        case Text.Info(_, XML.Elem(Markup(name, _), _))
+        if tooltips.isDefinedAt(name) => tooltips(name)
+      },
+      Some(Set(Markup.ENTITY, Markup.ML_TYPING) ++ tooltips.keys))
 
-  val tooltip2: Markup_Tree.Select[String] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
-  }
+  val tooltip2 =
+    Markup_Tree.Select[String](
+      {
+        case Text.Info(_, XML.Elem(Markup(Markup.TYPING, _), body)) => string_of_typing("::", body)
+      },
+      Some(Set(Markup.TYPING)))
 
   private val subexp_include =
     Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
       Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
       Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, 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)
-  }
+  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))
 
 
   /* token markup -- text styles */