--- 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}.
--- 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%
%
--- 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.
--- 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%
%
--- 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%
%
--- 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;
--- 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")
--- 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)
}
}
}