# HG changeset patch # User bulwahn # Date 1329826525 -3600 # Node ID 46124c9b5663c0a2f9134b781a2b1b95b9571893 # Parent ad21900e0ee9a3c0f12eea67b0c9482b8888320e# Parent 0ad69b30b39c1b491ac2957590e7b1422f132d00 merged diff -r ad21900e0ee9 -r 46124c9b5663 doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Tue Feb 21 12:20:33 2012 +0100 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Tue Feb 21 13:15:25 2012 +0100 @@ -149,7 +149,7 @@ \isamarkuptrue% % \begin{isamarkuptext}% -The \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \hyperlink{theory.Main}{\mbox{\isa{Main}}} theory already provides a code +The \isa{HOL} \isa{Main} theory already provides a code generator setup which should be suitable for most applications. Common extensions and modifications are available by certain theories of the \isa{HOL} library; beside being useful in @@ -173,12 +173,12 @@ \isa{Suc} is eliminated; includes \isa{Code{\isaliteral{5F}{\isacharunderscore}}Integer} and \isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}. - \item[\hyperlink{theory.Code-Numeral}{\mbox{\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}}}] provides an additional datatype + \item[\isa{Code{\isaliteral{5F}{\isacharunderscore}}Numeral}] provides an additional datatype \isa{index} which is mapped to target-language built-in integers. Useful for code setups which involve e.g.~indexing of target-language arrays. Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}. - \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{String{\isaliteral{2E}{\isachardot}}literal} which is isomorphic to strings; \isa{String{\isaliteral{2E}{\isachardot}}literal}s are mapped to target-language strings. Useful + \item[\isa{String}] provides an additional datatype \isa{String{\isaliteral{2E}{\isachardot}}literal} which is isomorphic to strings; \isa{String{\isaliteral{2E}{\isachardot}}literal}s are mapped to target-language strings. Useful for code setups which involve e.g.~printing (error) messages. Part of \isa{HOL{\isaliteral{2D}{\isacharminus}}Main}. diff -r ad21900e0ee9 -r 46124c9b5663 doc-src/Codegen/Thy/document/Evaluation.tex --- a/doc-src/Codegen/Thy/document/Evaluation.tex Tue Feb 21 12:20:33 2012 +0100 +++ b/doc-src/Codegen/Thy/document/Evaluation.tex Tue Feb 21 13:15:25 2012 +0100 @@ -372,7 +372,7 @@ arbitrary ML code as well. A typical example for \hyperlink{command.code-reflect}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}reflect}}}} can be found in the - \hyperlink{theory.Predicate}{\mbox{\isa{Predicate}}} theory.% + \isa{Predicate} theory.% \end{isamarkuptext}% \isamarkuptrue% % diff -r ad21900e0ee9 -r 46124c9b5663 doc-src/Codegen/Thy/document/Foundations.tex --- a/doc-src/Codegen/Thy/document/Foundations.tex Tue Feb 21 12:20:33 2012 +0100 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Tue Feb 21 13:15:25 2012 +0100 @@ -31,9 +31,9 @@ components which can be customised individually. Conceptually all components operate on Isabelle's logic framework - \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}. Practically, the object logic \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} + \isa{Pure}. Practically, the object logic \isa{HOL} provides the necessary facilities to make use of the code generator, - mainly since it is an extension of \hyperlink{theory.Pure}{\mbox{\isa{Pure}}}. + mainly since it is an extension of \isa{Pure}. The constellation of the different components is visualized in the following picture. diff -r ad21900e0ee9 -r 46124c9b5663 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Tue Feb 21 12:20:33 2012 +0100 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Tue Feb 21 13:15:25 2012 +0100 @@ -30,7 +30,7 @@ \cite{scala-overview-tech-report}. To profit from this tutorial, some familiarity and experience with - \hyperlink{theory.HOL}{\mbox{\isa{HOL}}} \cite{isa-tutorial} and its basic theories is assumed.% + \isa{HOL} \cite{isa-tutorial} and its basic theories is assumed.% \end{isamarkuptext}% \isamarkuptrue% % diff -r ad21900e0ee9 -r 46124c9b5663 doc-src/Codegen/Thy/document/Refinement.tex --- a/doc-src/Codegen/Thy/document/Refinement.tex Tue Feb 21 12:20:33 2012 +0100 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Tue Feb 21 13:15:25 2012 +0100 @@ -628,9 +628,9 @@ % \begin{isamarkuptext}% Typical data structures implemented by representations involving - invariants are available in the library, theory \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} + invariants are available in the library, theory \isa{Mapping} specifies key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping}); - these can be implemented by red-black-trees (theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).% + these can be implemented by red-black-trees (theory \isa{RBT}).% \end{isamarkuptext}% \isamarkuptrue% % diff -r ad21900e0ee9 -r 46124c9b5663 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Tue Feb 21 12:20:33 2012 +0100 +++ b/src/Pure/System/isabelle_process.ML Tue Feb 21 13:15:25 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 ad21900e0ee9 -r 46124c9b5663 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Tue Feb 21 12:20:33 2012 +0100 +++ b/src/Pure/System/isabelle_process.scala Tue Feb 21 13:15:25 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 ad21900e0ee9 -r 46124c9b5663 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Tue Feb 21 12:20:33 2012 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Tue Feb 21 13:15:25 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) } } }