concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;

--- a/src/Pure/PIDE/document.scala	Tue Sep 07 22:28:58 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Sep 07 23:06:52 2010 +0200
@@ -172,7 +172,7 @@
     def convert(range: Text.Range): Text.Range
     def revert(i: Text.Offset): Text.Offset
     def revert(range: Text.Range): Text.Range
-    def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+    def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
       : Stream[Text.Info[Option[A]]]
   }
 
@@ -310,7 +310,7 @@
         def revert(range: Text.Range): Text.Range =
           if (edits.isEmpty) range else range.map(revert(_))
 
-        def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+        def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
           : Stream[Text.Info[Option[A]]] =
         {
           val former_range = revert(range)

--- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 22:28:58 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 23:06:52 2010 +0200
@@ -43,6 +43,8 @@
   }
 
   val empty = new Markup_Tree(Branches.empty)
+
+  type Select[A] = PartialFunction[Text.Info[Any], A]
 }
 
 
@@ -89,7 +91,7 @@
   private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
     Branches.overlapping(range, branches).toStream
 
-  def select[A](root_range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
+  def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
     : Stream[Text.Info[Option[A]]] =
   {
     def stream(

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Sep 07 22:28:58 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Sep 07 23:06:52 2010 +0200
@@ -272,7 +272,7 @@
           handler.handleToken(line_segment, style, offset, length, context)
 
         val syntax = session.current_syntax()
-        val token_markup: PartialFunction[Text.Info[Any], Byte] =
+        val token_markup: Markup_Tree.Select[Byte] =
         {
           case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
           if syntax.keyword_kind(name).isDefined =>

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 22:28:58 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 23:06:52 2010 +0200
@@ -13,11 +13,11 @@
 import scala.actors.Actor._
 
 import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
-import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
+import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
 import javax.swing.{JPanel, ToolTipManager}
 import javax.swing.event.{CaretListener, CaretEvent}
 
-import org.gjt.sp.jedit.{jEdit, GUIUtilities, OperatingSystem}
+import org.gjt.sp.jedit.{jEdit, OperatingSystem}
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.options.GutterOptionPane
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
@@ -26,75 +26,6 @@
 
 object Document_View
 {
-  /* physical rendering */
-
-  val outdated_color = new Color(240, 240, 240)
-  val unfinished_color = new Color(255, 228, 225)
-
-  val regular_color = new Color(192, 192, 192)
-  val warning_color = new Color(255, 168, 0)
-  val error_color = new Color(255, 80, 80)
-  val bad_color = new Color(255, 204, 153, 100)
-
-  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
-  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
-
-  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
-  {
-    val state = snapshot.state(command)
-    if (snapshot.is_outdated) Some(outdated_color)
-    else
-      Isar_Document.command_status(state.status) match {
-        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
-        case Isar_Document.Unprocessed => Some(unfinished_color)
-        case _ => None
-      }
-  }
-
-  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
-  {
-    val state = snapshot.state(command)
-    if (snapshot.is_outdated) None
-    else
-      Isar_Document.command_status(state.status) match {
-        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
-        case Isar_Document.Unprocessed => Some(unfinished_color)
-        case Isar_Document.Failed => Some(error_color)
-        case _ => None
-      }
-  }
-
-
-  /* markup selectors */
-
-  private val message_markup: PartialFunction[Text.Info[Any], 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
-  }
-
-  private val background_markup: PartialFunction[Text.Info[Any], Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
-  }
-
-  private val box_markup: PartialFunction[Text.Info[Any], Color] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
-  }
-
-  private val tooltip_markup: PartialFunction[Text.Info[Any], String] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
-      Pretty.string_of(List(Pretty.block(body)), margin = 40)
-    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
-    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
-    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
-    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
-  }
-
-
   /* document view of text area */
 
   private val key = new Object
@@ -217,24 +148,17 @@
 
   /* subexpression highlighting */
 
-  private val subexp_include =
-    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
-
-  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
+  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
+    : Option[(Text.Range, Color)] =
   {
-    val subexp_markup: PartialFunction[Text.Info[Any], Text.Range] =
-    {
-      case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
-        snapshot.convert(range)
-    }
     val offset = text_area.xyToOffset(x, y)
-    snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup) match {
-      case Text.Info(_, r) #:: _ => r
+    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
+      case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
       case _ => None
     }
   }
 
-  private var highlight_range: Option[Text.Range] = None
+  private var highlight_range: Option[(Text.Range, Color)] = None
 
   private val focus_listener = new FocusAdapter {
     override def focusLost(e: FocusEvent) { highlight_range = None }
@@ -246,10 +170,10 @@
       if (!model.buffer.isLoaded) highlight_range = None
       else
         Isabelle.swing_buffer_lock(model.buffer) {
-          highlight_range.map(invalidate_line_range(_))
+          highlight_range map { case (range, _) => invalidate_line_range(range) }
           highlight_range =
             if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
-          highlight_range.map(invalidate_line_range(_))
+          highlight_range map { case (range, _) => invalidate_line_range(range) }
         }
     }
   }
@@ -279,7 +203,7 @@
                 (command, command_start) <- cmds if !command.is_ignored
                 val range = line_range.restrict(snapshot.convert(command.range + command_start))
                 r <- Isabelle.gfx_range(text_area, range)
-                color <- Document_View.status_color(snapshot, command)
+                color <- Isabelle_Markup.status_color(snapshot, command)
               } {
                 gfx.setColor(color)
                 gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
@@ -288,29 +212,29 @@
               // background color: markup
               for {
                 Text.Info(range, Some(color)) <-
-                  snapshot.select_markup(line_range)(Document_View.background_markup).iterator
+                  snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
                 r <- Isabelle.gfx_range(text_area, range)
               } {
                 gfx.setColor(color)
                 gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
               }
 
-              // subexpression highlighting -- potentially from other snapshot
-              if (highlight_range.isDefined) {
-                if (line_range.overlaps(highlight_range.get)) {
-                  Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
+              // sub-expression highlighting -- potentially from other snapshot
+              highlight_range match {
+                case Some((range, color)) if line_range.overlaps(range) =>
+                  Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
                     case None =>
                     case Some(r) =>
-                      gfx.setColor(Color.black)
+                      gfx.setColor(color)
                       gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
                   }
-                }
+                case _ =>
               }
 
               // boxed text
               for {
                 Text.Info(range, Some(color)) <-
-                  snapshot.select_markup(line_range)(Document_View.box_markup).iterator
+                  snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
                 r <- Isabelle.gfx_range(text_area, range)
               } {
                 gfx.setColor(color)
@@ -320,7 +244,7 @@
               // squiggly underline
               for {
                 Text.Info(range, Some(color)) <-
-                  snapshot.select_markup(line_range)(Document_View.message_markup).iterator
+                  snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
                 if color != null
                 r <- Isabelle.gfx_range(text_area, range)
               } {
@@ -344,7 +268,8 @@
       Isabelle.swing_buffer_lock(model.buffer) {
         val snapshot = model.snapshot()
         val offset = text_area.xyToOffset(x, y)
-        snapshot.select_markup(Text.Range(offset, offset + 1))(Document_View.tooltip_markup) match {
+        snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
+        {
           case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
           case _ => null
         }
@@ -378,9 +303,9 @@
               val states = cmds.map(p => snapshot.state(p._1)).toStream
               val opt_icon =
                 if (states.exists(_.results.exists(p => Isar_Document.is_error(p._2))))
-                  Some(Document_View.error_icon)
+                  Some(Isabelle_Markup.error_icon)
                 else if (states.exists(_.results.exists(p => Isar_Document.is_warning(p._2))))
-                  Some(Document_View.warning_icon)
+                  Some(Isabelle_Markup.warning_icon)
                 else None
               opt_icon match {
                 case Some(icon) if icon.getIconWidth > 0 && icon.getIconHeight > 0 =>
@@ -465,7 +390,7 @@
             val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
             val y = line_to_y(line1)
             val height = HEIGHT * (line2 - line1)
-            color <- Document_View.overview_color(snapshot, command)
+            color <- Isabelle_Markup.overview_color(snapshot, command)
           } {
             gfx.setColor(color)
             gfx.fillRect(0, y, getWidth - 1, height)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Tue Sep 07 23:06:52 2010 +0200
@@ -0,0 +1,98 @@
+/*  Title:      Tools/jEdit/src/jedit/isabelle_markup.scala
+    Author:     Makarius
+
+Isabelle specific physical rendering and markup selection.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Color
+
+import org.gjt.sp.jedit.GUIUtilities
+
+
+object Isabelle_Markup
+{
+  /* physical rendering */
+
+  val outdated_color = new Color(240, 240, 240)
+  val unfinished_color = new Color(255, 228, 225)
+
+  val regular_color = new Color(192, 192, 192)
+  val warning_color = new Color(255, 168, 0)
+  val error_color = new Color(255, 80, 80)
+  val bad_color = new Color(255, 204, 153, 100)
+
+  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
+  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
+
+
+  /* command status */
+
+  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+  {
+    val state = snapshot.state(command)
+    if (snapshot.is_outdated) Some(outdated_color)
+    else
+      Isar_Document.command_status(state.status) match {
+        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
+        case Isar_Document.Unprocessed => Some(unfinished_color)
+        case _ => None
+      }
+  }
+
+  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+  {
+    val state = snapshot.state(command)
+    if (snapshot.is_outdated) None
+    else
+      Isar_Document.command_status(state.status) match {
+        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
+        case Isar_Document.Unprocessed => Some(unfinished_color)
+        case Isar_Document.Failed => Some(error_color)
+        case _ => None
+      }
+  }
+
+
+  /* markup selectors */
+
+  private val subexp_include =
+    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
+
+  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
+  {
+    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+      (range, Color.black)
+  }
+
+  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 background: Markup_Tree.Select[Color] =
+  {
+    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+  }
+
+  val box: Markup_Tree.Select[Color] =
+  {
+    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
+  }
+
+  val tooltip: Markup_Tree.Select[String] =
+  {
+    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+      Pretty.string_of(List(Pretty.block(body)), margin = 40)
+    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
+    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
+    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
+    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
+  }
+}