# HG changeset patch
# User wenzelm
# Date 1321094749 -3600
# Node ID 3f290b6288cf7992cb1298ac2ae943f1115e6d74
# Parent  98af01f897c98de7cf455063c18977bf7c70e673
tuned signature;

diff -r 98af01f897c9 -r 3f290b6288cf src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Nov 11 22:09:07 2011 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Nov 12 11:45:49 2011 +0100
@@ -240,8 +240,7 @@
     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 cumulate_markup[A](range: Text.Range)(body: Markup_Tree.Cumulate[A]): Stream[Text.Info[A]]
     def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
       : Stream[Text.Info[Option[A]]]
   }
@@ -473,18 +472,23 @@
         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)))
+                  }))
           } yield Text.Info(convert(r0 + command_start), a)
         }
 
diff -r 98af01f897c9 -r 3f290b6288cf src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 22:09:07 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Nov 12 11:45:49 2011 +0100
@@ -15,7 +15,7 @@
 
 object Markup_Tree
 {
-  type Cumulate[A] = PartialFunction[(A, Text.Markup), A]
+  sealed case class Cumulate[A](info: A, result: PartialFunction[(A, Text.Markup), A])
   type Select[A] = PartialFunction[Text.Markup, A]
 
   val empty: Markup_Tree = new Markup_Tree(Branches.empty)
@@ -84,15 +84,18 @@
     }
   }
 
-  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
+    val result = body.result
+
     def stream(
       last: Text.Offset,
       stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])]): Stream[Text.Info[A]] =
     {
       stack match {
         case (parent, (range, (info, tree)) #:: more) :: rest =>
-          val subrange = range.restrict(root.range)
+          val subrange = range.restrict(root_range)
           val subtree = tree.overlapping(subrange).toStream
           val start = subrange.start
 
@@ -112,12 +115,13 @@
           else nexts
 
         case Nil =>
-          val stop = root.range.stop
-          if (last < stop) Stream(root.restrict(Text.Range(last, stop)))
+          val stop = root_range.stop
+          if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
           else Stream.empty
       }
     }
-    stream(root.range.start, List((root, overlapping(root.range).toStream)))
+    stream(root_range.start,
+      List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
   }
 
   def select[A](root_range: Text.Range)(result: Select[A]): Stream[Text.Info[Option[A]]] =
diff -r 98af01f897c9 -r 3f290b6288cf src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Nov 11 22:09:07 2011 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sat Nov 12 11:45:49 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 98af01f897c9 -r 3f290b6288cf src/Tools/jEdit/src/isabelle_markup.scala
--- a/src/Tools/jEdit/src/isabelle_markup.scala	Fri Nov 11 22:09:07 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Nov 12 11:45:49 2011 +0100
@@ -94,13 +94,14 @@
     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
   }
 
-  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")))
+      })
 
   val gutter_message: Markup_Tree.Select[Icon] =
   {