# HG changeset patch
# User wenzelm
# Date 1375875992 -7200
# Node ID ea3338812e67622fc76caf519939c48d8b62e27e
# Parent  671421cef59003bb225fdcfcb5272d04a494f59e
more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;

diff -r 671421cef590 -r ea3338812e67 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 07 11:50:14 2013 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 07 13:46:32 2013 +0200
@@ -320,19 +320,19 @@
     val node: Node
     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
-    def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
     def eq_content(other: Snapshot): Boolean
     def cumulate_markup[A](
       range: Text.Range,
       info: A,
       elements: Option[Set[String]],
-      result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]]
+      result: Command.State => (A, Text.Markup) => Option[A]): Stream[Text.Info[A]]
     def select_markup[A](
       range: Text.Range,
       elements: Option[Set[String]],
-      result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
+      result: Command.State => Text.Markup => Option[A]): Stream[Text.Info[A]]
   }
 
   type Assign_Update =
@@ -564,33 +564,30 @@
             })
 
         def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
-          result: Command.State => PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
+          result: Command.State => (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
         {
           val former_range = revert(range)
           for {
             (command, command_start) <- node.command_range(former_range).toStream
             st = state.command_state(version, command)
             res = result(st)
-            Text.Info(r0, a) <- st.markup.
-              cumulate[A]((former_range - command_start).restrict(command.range), info, elements,
-                {
-                  case (a, Text.Info(r0, b))
-                  if res.isDefinedAt((a, Text.Info(convert(r0 + command_start), b))) =>
-                    res((a, Text.Info(convert(r0 + command_start), b)))
-                })
+            Text.Info(r0, a) <- st.markup.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)) })
           } yield Text.Info(convert(r0 + command_start), a)
         }
 
         def select_markup[A](range: Text.Range, elements: Option[Set[String]],
-          result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]] =
+          result: Command.State => Text.Markup => Option[A]): Stream[Text.Info[A]] =
         {
-          def result1(st: Command.State) =
+          def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
           {
             val res = result(st)
-            new PartialFunction[(Option[A], Text.Markup), Option[A]] {
-              def isDefinedAt(arg: (Option[A], Text.Markup)): Boolean = res.isDefinedAt(arg._2)
-              def apply(arg: (Option[A], Text.Markup)): Option[A] = Some(res(arg._2))
-            }
+            (_: Option[A], x: Text.Markup) =>
+              res(x) match {
+                case None => None
+                case some => Some(some)
+              }
           }
           for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
             yield Text.Info(r, x)
diff -r 671421cef590 -r ea3338812e67 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 11:50:14 2013 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Wed Aug 07 13:46:32 2013 +0200
@@ -223,7 +223,7 @@
     to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
 
   def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
-    result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
+    result: (A, Text.Markup) => Option[A]): Stream[Text.Info[A]] =
   {
     val notable: Elements => Boolean =
       result_elements match {
@@ -233,15 +233,12 @@
 
     def results(x: A, entry: Entry): Option[A] =
     {
-      val (y, changed) =
-        // FIXME proper cumulation order (including status markup) (!?)
-        ((x, false) /: entry.rev_markup)((res, info) =>
-          {
-            val (y, changed) = res
-            val arg = (y, Text.Info(entry.range, info))
-            if (result.isDefinedAt(arg)) (result(arg), true)
-            else res
-          })
+      var y = x
+      var changed = false
+      for {
+        info <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
+        y1 <- result(y, Text.Info(entry.range, info))
+      } { y = y1; changed = true }
       if (changed) Some(y) else None
     }
 
diff -r 671421cef590 -r ea3338812e67 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 11:50:14 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Aug 07 13:46:32 2013 +0200
@@ -154,11 +154,12 @@
         snapshot.cumulate_markup[(Protocol.Status, Int)](
           range, (Protocol.Status.init, 0), Some(overview_include), _ =>
           {
-            case ((status, pri), Text.Info(_, XML.Elem(markup, _)))
-            if overview_include(markup.name) =>
+            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
               if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
-                (status, pri max Rendering.message_pri(markup.name))
-              else (Protocol.command_status(status, markup), pri)
+                Some((status, pri max Rendering.message_pri(markup.name)))
+              else if (overview_include(markup.name))
+                Some((Protocol.command_status(status, markup), pri))
+              else None
           })
       if (results.isEmpty) None
       else {
@@ -188,8 +189,10 @@
   {
     snapshot.select_markup(range, Some(highlight_include), _ =>
         {
-          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
-            Text.Info(snapshot.convert(info_range), highlight_color)
+          case Text.Info(info_range, XML.Elem(markup, _)) =>
+            if (highlight_include(markup.name))
+              Some(Text.Info(snapshot.convert(info_range), highlight_color))
+            else None
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   }
 
@@ -203,7 +206,8 @@
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
-            Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
+            val link = Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0))
+            Some(link :: links)
 
           case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
           if !props.exists(
@@ -216,8 +220,10 @@
                 Isabelle_System.source_file(Path.explode(name)) match {
                   case Some(path) =>
                     val jedit_file = Isabelle_System.platform_path(path)
-                    Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
-                  case None => links
+                    val link =
+                      Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0))
+                    Some(link :: links)
+                  case None => None
                 }
 
               case Position.Def_Id_Offset(id, offset) =>
@@ -227,13 +233,17 @@
                       node.commands.iterator.takeWhile(_ != command).map(_.source) ++
                         Iterator.single(command.source(Text.Range(0, command.decode(offset))))
                     val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
-                    Text.Info(snapshot.convert(info_range),
-                      Hyperlink(command.node_name.node, line, column)) :: links
-                  case None => links
+                    val link =
+                      Text.Info(snapshot.convert(info_range),
+                        Hyperlink(command.node_name.node, line, column))
+                    Some(link :: links)
+                  case None => None
                 }
 
-              case _ => links
+              case _ => None
             }
+
+          case _ => None
         }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
   }
 
@@ -246,10 +256,11 @@
         {
           case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
           if !command_state.results.defined(serial) =>
-            Text.Info(snapshot.convert(info_range), elem)
-          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
-          if name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
-            Text.Info(snapshot.convert(info_range), elem)
+            Some(Text.Info(snapshot.convert(info_range), elem))
+          case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _)) =>
+            if (name == Markup.BROWSER || name == Markup.GRAPHVIEW || name == Markup.SENDBACK)
+              Some(Text.Info(snapshot.convert(info_range), elem))
+            else None
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
 
 
@@ -257,7 +268,7 @@
   {
     val results =
       snapshot.select_markup[Command.Results](range, None, command_state =>
-        { case _ => command_state.results }).map(_.info)
+        { case _ => Some(command_state.results) }).map(_.info)
     (Command.Results.empty /: results)(_ ++ _)
   }
 
@@ -272,12 +283,14 @@
           if name == Markup.WRITELN || name == Markup.WARNING || name == Markup.ERROR =>
             val entry: Command.Results.Entry =
               (serial -> XML.Elem(Markup(Markup.message(name), props), body))
-            Text.Info(snapshot.convert(info_range), entry) :: msgs
+            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
 
           case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
           if !body.isEmpty =>
             val entry: Command.Results.Entry = (Document_ID.make(), msg)
-            Text.Info(snapshot.convert(info_range), entry) :: msgs
+            Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
+
+          case _ => None
         }).toList.flatMap(_.info)
     if (results.isEmpty) None
     else {
@@ -328,7 +341,7 @@
         range, Text.Info(range, (Timing.zero, Nil)), Some(tooltip_elements), _ =>
         {
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
-            Text.Info(r, (t1 + t2, info))
+            Some(Text.Info(r, (t1 + t2, info)))
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
             val kind1 = space_explode('_', kind).mkString(" ")
             val txt1 = kind1 + " " + quote(name)
@@ -337,19 +350,20 @@
               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
                 "\n" + t.message
               else ""
-            add(prev, r, (true, XML.Text(txt1 + txt2)))
+            Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
             val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
-            add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
+            Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
           if name == Markup.SORTING || name == Markup.TYPING =>
-            add(prev, r, (true, pretty_typing("::", body)))
+            Some(add(prev, r, (true, pretty_typing("::", body))))
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
-            add(prev, r, (false, pretty_typing("ML:", body)))
-          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
-          if tooltips.isDefinedAt(name) =>
-            add(prev, r, (true, XML.Text(tooltips(name))))
+            Some(add(prev, r, (false, pretty_typing("ML:", body))))
+          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
+            if (tooltips.isDefinedAt(name))
+              Some(add(prev, r, (true, XML.Text(tooltips(name)))))
+            else None
         }).toList.map(_.info)
 
     results.map(_.info).flatMap(_._2) match {
@@ -383,15 +397,17 @@
         {
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
               List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
-            pri max Rendering.information_pri
+            Some(pri max Rendering.information_pri)
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
             body match {
               case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
-                pri max Rendering.legacy_pri
-              case _ => pri max Rendering.warning_pri
+                Some(pri max Rendering.legacy_pri)
+              case _ =>
+                Some(pri max Rendering.warning_pri)
             }
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _))) =>
-            pri max Rendering.error_pri
+            Some(pri max Rendering.error_pri)
+          case _ => None
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
     gutter_icons.get(pri)
@@ -404,19 +420,19 @@
     Rendering.warning_pri -> warning_color,
     Rendering.error_pri -> error_color)
 
-  private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+  private val squiggly_include = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
 
   def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   {
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
+      snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
         {
-          case (pri, Text.Info(_, msg @ XML.Elem(Markup(name, _), _)))
-          if name == Markup.WRITELN ||
-            name == Markup.WARNING ||
-            name == Markup.ERROR =>
-              if (Protocol.is_information(msg)) pri max Rendering.information_pri
-              else pri max Rendering.message_pri(name)
+          case (pri, Text.Info(_, msg @ XML.Elem(markup, _))) =>
+            if (Protocol.is_information(msg))
+              Some(pri max Rendering.information_pri)
+            else if (squiggly_include.contains(markup.name))
+              Some(pri max Rendering.message_pri(markup.name))
+            else None
         })
     for {
       Text.Info(r, pri) <- results
@@ -442,19 +458,20 @@
       snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
         {
           case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
-            pri max Rendering.information_pri
-          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
-          if name == Markup.WRITELN_MESSAGE ||
-            name == Markup.TRACING_MESSAGE ||
-            name == Markup.WARNING_MESSAGE ||
-            name == Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
+            Some(pri max Rendering.information_pri)
+          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
+            if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
+                name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
+              Some(pri max Rendering.message_pri(name))
+            else None
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 
     val is_separator = pri > 0 &&
       snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
         {
-          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => true
+          case (_, Text.Info(_, XML.Elem(Markup(Markup.SEPARATOR, _), _))) => Some(true)
+          case _ => None
         }).exists(_.info)
 
     message_colors.get(pri).map((_, is_separator))
@@ -483,20 +500,21 @@
             {
               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
               if (Protocol.command_status_markup(markup.name)) =>
-                (Some(Protocol.command_status(status, markup)), color)
+                Some((Some(Protocol.command_status(status, markup)), color))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _))) =>
-                (None, Some(bad_color))
+                Some((None, Some(bad_color)))
               case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
-                (None, Some(intensify_color))
+                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 =>
-                    (None, Some(active_result_color))
+                    Some((None, Some(active_result_color)))
                   case _ =>
-                    (None, Some(active_color))
+                    Some((None, Some(active_color)))
                 }
-              case (_, Text.Info(_, XML.Elem(markup, _))) if active_include(markup.name) =>
-                (None, Some(active_color))
+              case (_, Text.Info(_, XML.Elem(markup, _))) =>
+                if (active_include(markup.name)) Some((None, Some(active_color)))
+                else None
             })
         color <-
           (result match {
@@ -513,14 +531,16 @@
   def background2(range: Text.Range): Stream[Text.Info[Color]] =
     snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
       {
-        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
+        case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => Some(light_color)
+        case _ => None
       })
 
 
   def bullet(range: Text.Range): Stream[Text.Info[Color]] =
     snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
       {
-        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => bullet_color
+        case Text.Info(_, XML.Elem(Markup(Markup.BULLET, _), _)) => Some(bullet_color)
+        case _ => None
       })
 
 
@@ -530,10 +550,11 @@
   def foreground(range: Text.Range): Stream[Text.Info[Color]] =
     snapshot.select_markup(range, Some(foreground_elements), _ =>
       {
-        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
-        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => antiquoted_color
+        case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => Some(quoted_color)
+        case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => Some(quoted_color)
+        case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => Some(quoted_color)
+        case Text.Info(_, XML.Elem(Markup(Markup.ANTIQ, _), _)) => Some(antiquoted_color)
+        case _ => None
       })
 
 
@@ -570,8 +591,7 @@
     else
       snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
         {
-          case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
-          if text_colors.isDefinedAt(m) => text_colors(m)
+          case (_, Text.Info(_, XML.Elem(markup, _))) => text_colors.get(markup.name)
         })
   }
 
@@ -583,7 +603,7 @@
   def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
     snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
       {
-        case (depth, Text.Info(_, XML.Elem(Markup(name, _), _)))
-        if fold_depth_include(name) => depth + 1
+        case (depth, Text.Info(_, XML.Elem(markup, _))) =>
+          if (fold_depth_include(markup.name)) Some(depth + 1) else None
       })
 }