quasi-abstract module Rendering, with Isabelle-specific implementation;

--- a/src/Tools/jEdit/src/document_view.scala	Sun Nov 25 17:15:21 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Sun Nov 25 18:47:33 2012 +0100
@@ -67,8 +67,7 @@
 {
   private val session = model.session
 
-  def get_rendering(): Isabelle_Rendering =
-    Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
+  def get_rendering(): Rendering = Rendering(model.snapshot(), Isabelle.options.value)
 
   val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false)
 

--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 25 17:15:21 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 25 18:47:33 2012 +0100
@@ -45,7 +45,7 @@
       new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
         override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
         {
-          val rendering = Isabelle_Rendering(snapshot, Isabelle.options.value)
+          val rendering = Rendering(snapshot, Isabelle.options.value)
           new Pretty_Tooltip(view, parent, rendering, x, y, body)
           null
         }

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Nov 25 17:15:21 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sun Nov 25 18:47:33 2012 +0100
@@ -1,7 +1,8 @@
 /*  Title:      Tools/jEdit/src/isabelle_rendering.scala
     Author:     Makarius
 
-Isabelle specific physical rendering and markup selection.
+Isabelle-specific implementation of quasi-abstract rendering and
+markup interpretation.
 */
 
 package isabelle.jedit
@@ -11,7 +12,6 @@
 
 import java.awt.Color
 import javax.swing.Icon
-import java.io.{File => JFile}
 
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
 import org.gjt.sp.jedit.GUIUtilities
@@ -20,10 +20,10 @@
 import scala.collection.immutable.SortedMap
 
 
-object Isabelle_Rendering
+object Rendering
 {
-  def apply(snapshot: Document.Snapshot, options: Options): Isabelle_Rendering =
-    new Isabelle_Rendering(snapshot, options)
+  def apply(snapshot: Document.Snapshot, options: Options): Rendering =
+    new Rendering(snapshot, options)
 
 
   /* message priorities */
@@ -103,7 +103,7 @@
 }
 
 
-class Isabelle_Rendering private(val snapshot: Document.Snapshot, val options: Options)
+class Rendering private(val snapshot: Document.Snapshot, val options: Options)
 {
   /* colors */
 
@@ -162,7 +162,7 @@
           {
             case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
               if (markup.name == Isabelle_Markup.WARNING || markup.name == Isabelle_Markup.ERROR)
-                (status, pri max Isabelle_Rendering.message_pri(markup.name))
+                (status, pri max Rendering.message_pri(markup.name))
               else (Protocol.command_status(status, markup), pri)
           })
       if (results.isEmpty) None
@@ -171,8 +171,8 @@
           ((Protocol.Status.init, 0) /: results) {
             case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
 
-        if (pri == Isabelle_Rendering.warning_pri) Some(warning_color)
-        else if (pri == Isabelle_Rendering.error_pri) Some(error_color)
+        if (pri == Rendering.warning_pri) Some(warning_color)
+        else if (pri == Rendering.error_pri) Some(error_color)
         else if (status.is_unprocessed) Some(unprocessed_color)
         else if (status.is_running) Some(running_color)
         else if (status.is_failed) Some(error_color)
@@ -336,21 +336,21 @@
           case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
             body match {
               case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) =>
-                pri max Isabelle_Rendering.legacy_pri
-              case _ => pri max Isabelle_Rendering.warning_pri
+                pri max Rendering.legacy_pri
+              case _ => pri max Rendering.warning_pri
             }
           case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
-            pri max Isabelle_Rendering.error_pri
+            pri max Rendering.error_pri
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
-    Isabelle_Rendering.gutter_icons.get(pri)
+    Rendering.gutter_icons.get(pri)
   }
 
 
   private val squiggly_colors = Map(
-    Isabelle_Rendering.writeln_pri -> writeln_color,
-    Isabelle_Rendering.warning_pri -> warning_color,
-    Isabelle_Rendering.error_pri -> error_color)
+    Rendering.writeln_pri -> writeln_color,
+    Rendering.warning_pri -> warning_color,
+    Rendering.error_pri -> error_color)
 
   def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
   {
@@ -361,7 +361,7 @@
           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
           if name == Isabelle_Markup.WRITELN ||
             name == Isabelle_Markup.WARNING ||
-            name == Isabelle_Markup.ERROR => pri max Isabelle_Rendering.message_pri(name)
+            name == Isabelle_Markup.ERROR => pri max Rendering.message_pri(name)
         })
     for {
       Text.Info(r, pri) <- results
@@ -375,10 +375,10 @@
       Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE)
 
   private val message_colors = Map(
-    Isabelle_Rendering.writeln_pri -> writeln_message_color,
-    Isabelle_Rendering.tracing_pri -> tracing_message_color,
-    Isabelle_Rendering.warning_pri -> warning_message_color,
-    Isabelle_Rendering.error_pri -> error_message_color)
+    Rendering.writeln_pri -> writeln_message_color,
+    Rendering.tracing_pri -> tracing_message_color,
+    Rendering.warning_pri -> warning_message_color,
+    Rendering.error_pri -> error_message_color)
 
   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
@@ -389,7 +389,7 @@
           if name == Isabelle_Markup.WRITELN_MESSAGE ||
             name == Isabelle_Markup.TRACING_MESSAGE ||
             name == Isabelle_Markup.WARNING_MESSAGE ||
-            name == Isabelle_Markup.ERROR_MESSAGE => pri max Isabelle_Rendering.message_pri(name)
+            name == Isabelle_Markup.ERROR_MESSAGE => pri max Rendering.message_pri(name)
         })
     val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
 

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 25 17:15:21 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 25 18:47:33 2012 +0100
@@ -22,10 +22,10 @@
 object Pretty_Text_Area
 {
   private def text_rendering(base_snapshot: Document.Snapshot, formatted_body: XML.Body):
-    (String, Isabelle_Rendering) =
+    (String, Rendering) =
   {
     val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body)
-    val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
+    val rendering = Rendering(state.snapshot(), Isabelle.options.value)
     (text, rendering)
   }
 
@@ -62,7 +62,7 @@
   private var current_font_size: Int = 12
   private var current_body: XML.Body = Nil
   private var current_base_snapshot = Document.State.init.snapshot()
-  private var current_rendering: Isabelle_Rendering =
+  private var current_rendering: Rendering =
     Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
   private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
 

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 25 17:15:21 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 25 18:47:33 2012 +0100
@@ -24,7 +24,7 @@
 class Pretty_Tooltip(
   view: View,
   parent: JComponent,
-  rendering: Isabelle_Rendering,
+  rendering: Rendering,
   mouse_x: Int, mouse_y: Int, body: XML.Body)
   extends JWindow(JEdit_Lib.parent_window(parent) getOrElse view)
 {
@@ -81,14 +81,14 @@
   /* controls */
 
   private val close = new Label {
-    icon = Isabelle_Rendering.tooltip_close_icon
+    icon = Rendering.tooltip_close_icon
     tooltip = "Close tooltip window"
     listenTo(mouse.clicks)
     reactions += { case _: MouseClicked => window.dispose() }
   }
 
   private val detach = new Label {
-    icon = Isabelle_Rendering.tooltip_detach_icon
+    icon = Rendering.tooltip_detach_icon
     tooltip = "Detach tooltip window"
     listenTo(mouse.clicks)
     reactions += {

--- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Nov 25 17:15:21 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Nov 25 18:47:33 2012 +0100
@@ -26,7 +26,7 @@
 class Rich_Text_Area(
   view: View,
   text_area: TextArea,
-  get_rendering: () => Isabelle_Rendering,
+  get_rendering: () => Rendering,
   hovering: Boolean)
 {
   private val buffer = text_area.getBuffer
@@ -65,7 +65,7 @@
 
   /* common painter state */
 
-  @volatile private var painter_rendering: Isabelle_Rendering = null
+  @volatile private var painter_rendering: Rendering = null
   @volatile private var painter_clip: Shape = null
 
   private val set_state = new TextAreaExtension
@@ -90,7 +90,7 @@
     }
   }
 
-  def robust_rendering(body: Isabelle_Rendering => Unit)
+  def robust_rendering(body: Rendering => Unit)
   {
     robust_body(()) { body(painter_rendering) }
   }
@@ -98,8 +98,7 @@
 
   /* active areas within the text */
 
-  private class Active_Area[A](
-    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
+  private class Active_Area[A](rendering: Rendering => Text.Range => Option[Text.Info[A]])
   {
     private var the_text_info: Option[(String, Text.Info[A])] = None
 
@@ -123,7 +122,7 @@
       }
     }
 
-    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
+    def update_rendering(r: Rendering, range: Text.Range)
     { update(rendering(r)(range)) }
 
     def reset { update(None) }
@@ -133,10 +132,9 @@
 
   private var control: Boolean = false
 
-  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
-  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
-  private val sendback_area =
-    new Active_Area[Option[Document.Exec_ID]]((r: Isabelle_Rendering) => r.sendback _)
+  private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
+  private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
+  private val sendback_area = new Active_Area[Option[Document.Exec_ID]]((r: Rendering) => r.sendback _)
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
@@ -294,7 +292,7 @@
 
   /* text */
 
-  private def paint_chunk_list(rendering: Isabelle_Rendering,
+  private def paint_chunk_list(rendering: Rendering,
     gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   {
     val clip_rect = gfx.getClipBounds

--- a/src/Tools/jEdit/src/token_markup.scala	Sun Nov 25 17:15:21 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Nov 25 18:47:33 2012 +0100
@@ -222,8 +222,7 @@
         val (styled_tokens, context1) =
           if (line_ctxt.isDefined && syntax.isDefined) {
             val (tokens, ctxt1) = syntax.get.scan_context(line, line_ctxt.get)
-            val styled_tokens =
-              tokens.map(tok => (Isabelle_Rendering.token_markup(syntax.get, tok), tok))
+            val styled_tokens = tokens.map(tok => (Rendering.token_markup(syntax.get, tok), tok))
             (styled_tokens, new Line_Context(Some(ctxt1)))
           }
           else {