text_rendering as managed task, with cancellation;

--- a/src/Pure/Concurrent/simple_thread.scala	Thu Sep 20 19:23:05 2012 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala	Thu Sep 20 20:13:42 2012 +0200
@@ -15,6 +15,12 @@
 
 object Simple_Thread
 {
+  /* prending interrupts */
+
+  def interrupted_exception(): Unit =
+    if (Thread.interrupted()) throw new InterruptedException
+
+
   /* plain thread */
 
   def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Sep 20 19:23:05 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Sep 20 20:13:42 2012 +0200
@@ -20,7 +20,15 @@
 
 object Pretty_Text_Area
 {
-  def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
+  private def text_rendering(base_snapshot: Document.Snapshot, formatted_body: XML.Body):
+    (String, Isabelle_Rendering) =
+  {
+    val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body)
+    val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
+    (text, rendering)
+  }
+
+  private def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
     : (String, Document.State) =
   {
     val command = Command.rich_text(Document.new_id(), formatted_body)
@@ -51,54 +59,52 @@
 
   Swing_Thread.require()
 
-  private var current_font_metrics: FontMetrics = null
   private var current_font_family = "Dialog"
   private var current_font_size: Int = 12
-  private var current_margin: Int = 0
   private var current_body: XML.Body = Nil
   private var current_base_snapshot = Document.State.init.snapshot()
-  private var current_rendering: Isabelle_Rendering = text_rendering()._2
+  private var current_rendering: Isabelle_Rendering =
+    Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
+  private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
 
   private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
 
-  private def text_rendering(): (String, Isabelle_Rendering) =
-  {
-    Swing_Thread.require()
-
-    val body =
-      Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics))
-    val (text, state) = Pretty_Text_Area.document_state(current_base_snapshot, body)
-    val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
-
-    (text, rendering)
-  }
-
   def refresh()
   {
     Swing_Thread.require()
 
     val font = new Font(current_font_family, Font.PLAIN, current_font_size)
-
     getPainter.setFont(font)
     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
     getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
 
-    current_font_metrics = painter.getFontMetrics(font)
-    current_margin = (getWidth / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
+    val font_metrics = getPainter.getFontMetrics(font)
+    val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
+
+    val base_snapshot = current_base_snapshot
+    val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
 
-    val (text, rendering) = text_rendering()
-    current_rendering = rendering
+    future_rendering.map(_.cancel(true))
+    future_rendering = Some(default_thread_pool.submit(() =>
+      {
+        val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
+        Simple_Thread.interrupted_exception()
 
-    try {
-      getBuffer.beginCompoundEdit
-      getBuffer.setReadOnly(false)
-      setText(text)
-      setCaretPosition(0)
-      getBuffer.setReadOnly(true)
-    }
-    finally {
-      getBuffer.endCompoundEdit
-    }
+        Swing_Thread.later {
+          current_rendering = rendering
+
+          try {
+            getBuffer.beginCompoundEdit
+            getBuffer.setReadOnly(false)
+            setText(text)
+            setCaretPosition(0)
+            getBuffer.setReadOnly(true)
+          }
+          finally {
+            getBuffer.endCompoundEdit
+          }
+        }
+      }))
   }
 
   def resize(font_family: String, font_size: Int)