# HG changeset patch
# User wenzelm
# Date 1329824700 -3600
# Node ID 26977429b784d36da5d8745c47c10fd99082362f
# Parent  0133d31f9ab4ca122025f98794d7cc8440a17f58# Parent  092f4eca98485add0d670d01abbde4ca76dd1bf3
merged;

diff -r 092f4eca9848 -r 26977429b784 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Feb 21 11:08:05 2012 +0100
+++ b/src/Pure/System/isabelle_process.ML	Tue Feb 21 12:45:00 2012 +0100
@@ -6,13 +6,13 @@
 
 Startup phases:
   . raw Posix process startup with uncontrolled output on stdout/stderr
-  . stdout \002: ML running
+  . stderr \002: ML running
   .. stdin/stdout/stderr freely available (raw ML loop)
   .. protocol thread initialization
   ... rendezvous on system channel
   ... message INIT(pid): channels ready
-  ... message STATUS(keywords)
-  ... message READY: main loop ready
+  ... message RAW(keywords)
+  ... message RAW(ready): main loop ready
 *)
 
 signature ISABELLE_PROCESS =
@@ -165,7 +165,7 @@
 fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
   let
     val _ = OS.Process.sleep (seconds 0.5);  (*yield to raw ML toplevel*)
-    val _ = Output.physical_stdout Symbol.STX;
+    val _ = Output.physical_stderr Symbol.STX;
 
     val _ = quick_and_dirty := true;
     val _ = Goal.parallel_proofs := 0;
diff -r 092f4eca9848 -r 26977429b784 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Tue Feb 21 11:08:05 2012 +0100
+++ b/src/Pure/System/isabelle_process.scala	Tue Feb 21 12:45:00 2012 +0100
@@ -152,15 +152,15 @@
 
   private val process_manager = Simple_Thread.fork("process_manager")
   {
-    val (startup_failed, startup_output) =
+    val (startup_failed, startup_errors) =
     {
       val expired = System.currentTimeMillis() + timeout.ms
       val result = new StringBuilder(100)
 
       var finished: Option[Boolean] = None
       while (finished.isEmpty && System.currentTimeMillis() <= expired) {
-        while (finished.isEmpty && process.stdout.ready) {
-          val c = process.stdout.read
+        while (finished.isEmpty && process.stderr.ready) {
+          val c = process.stderr.read
           if (c == 2) finished = Some(true)
           else result += c.toChar
         }
@@ -169,7 +169,7 @@
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
-    system_result(startup_output)
+    if (startup_errors != "") system_result(startup_errors)
 
     if (startup_failed) {
       put_result(Isabelle_Markup.EXIT, "Return code: 127")
diff -r 092f4eca9848 -r 26977429b784 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 11:08:05 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Tue Feb 21 12:45:00 2012 +0100
@@ -10,6 +10,7 @@
 
 import isabelle._
 
+import scala.annotation.tailrec
 import scala.collection.mutable
 import scala.collection.immutable.SortedMap
 import scala.actors.Actor._
@@ -354,11 +355,7 @@
     private val WIDTH = 10
     private val HEIGHT = 2
 
-    private def line_to_y(line: Int): Int =
-      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
-
-    private def y_to_line(y: Int): Int =
-      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
+    private def lines(): Int = model.buffer.getLineCount max text_area.getVisibleLines
 
     setPreferredSize(new Dimension(WIDTH, 0))
 
@@ -366,7 +363,7 @@
 
     addMouseListener(new MouseAdapter {
       override def mousePressed(event: MouseEvent) {
-        val line = y_to_line(event.getY)
+        val line = (event.getY * lines()) / getHeight
         if (line >= 0 && line < text_area.getLineCount)
           text_area.setCaretPosition(text_area.getLineStartOffset(line))
       }
@@ -387,23 +384,44 @@
       super.paintComponent(gfx)
       Swing_Thread.assert()
 
-      val buffer = model.buffer
-      Isabelle.buffer_lock(buffer) {
-        val snapshot = update_snapshot()
+      robust_body(()) {
+        val buffer = model.buffer
+        Isabelle.buffer_lock(buffer) {
+          val snapshot = update_snapshot()
+
+          gfx.setColor(getBackground)
+          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
+
+          val line_count = buffer.getLineCount
+          val char_count = buffer.getLength
+
+          val L = lines()
+          val H = getHeight()
 
-        for {
-          line <- 0 until buffer.getLineCount
-          range <-
-            try {
-              Some(proper_line_range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line)))
+          @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit =
+          {
+            if (l < line_count && h < H) {
+              val p1 = p + H
+              val q1 = q + HEIGHT * L
+              val (l1, h1) =
+                if (p1 >= q1) (l + 1, h + (p1 - q) / L)
+                else (l + (q1 - p) / H, h + HEIGHT)
+
+              val start = buffer.getLineStartOffset(l)
+              val end =
+                if (l1 < line_count) buffer.getLineStartOffset(l1)
+                else char_count
+
+              Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match {
+                case None =>
+                case Some(color) =>
+                  gfx.setColor(color)
+                  gfx.fillRect(0, h, getWidth, h1 - h)
+              }
+              paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L)
             }
-            catch { case e: ArrayIndexOutOfBoundsException => None }
-          color <- Isabelle_Rendering.overview_color(snapshot, range)
-        } {
-          val y = line_to_y(line)
-          val h = (line_to_y(line + 1) - y) max 2
-          gfx.setColor(color)
-          gfx.fillRect(0, y, getWidth - 1, h)
+          }
+          paint_loop(0, 0, 0, 0)
         }
       }
     }