--- a/Admin/Release/CHECKLIST Fri May 02 21:18:50 2014 +0200
+++ b/Admin/Release/CHECKLIST Fri May 02 23:31:25 2014 +0200
@@ -17,7 +17,8 @@
- check HTML header of library;
-- check sources: see isabelle.Check_Source;
+- check sources:
+ isabelle java isabelle.Check_Source '~~' '$AFP_BASE'
- run isabelle update_keywords;
--- a/NEWS Fri May 02 21:18:50 2014 +0200
+++ b/NEWS Fri May 02 23:31:25 2014 +0200
@@ -126,6 +126,9 @@
* More support for remote files (e.g. http) using standard Java
networking operations instead of jEdit virtual file-systems.
+* Improved Console/Scala plugin: more uniform scala.Console output,
+more robust treatment of threads and interrupts.
+
*** Pure ***
--- a/src/HOL/Library/Function_Algebras.thy Fri May 02 21:18:50 2014 +0200
+++ b/src/HOL/Library/Function_Algebras.thy Fri May 02 23:31:25 2014 +0200
@@ -176,7 +176,7 @@
instance "fun" :: (type, ring_char_0) ring_char_0 ..
-text {* Ordereded structures *}
+text {* Ordered structures *}
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
by default (auto simp add: le_fun_def intro: add_left_mono)
--- a/src/Pure/General/output.ML Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/General/output.ML Fri May 02 23:31:25 2014 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/General/output.ML
Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
-Isabelle output channels.
+Isabelle channels for diagnostic output.
*)
signature BASIC_OUTPUT =
--- a/src/Pure/General/output.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/General/output.scala Fri May 02 23:31:25 2014 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/General/output.ML
Author: Makarius
-Isabelle output channels: plain text without markup.
+Isabelle channels for diagnostic output.
*/
package isabelle
@@ -12,7 +12,8 @@
def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
- def warning(msg: String) { System.err.println(warning_text(msg)) }
- def error_message(msg: String) { System.err.println(error_text(msg)) }
+ def writeln(msg: String) { Console.err.println(msg) }
+ def warning(msg: String) { Console.err.println(warning_text(msg)) }
+ def error_message(msg: String) { Console.err.println(error_text(msg)) }
}
--- a/src/Pure/General/scan.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/General/scan.scala Fri May 02 23:31:25 2014 +0200
@@ -458,7 +458,7 @@
class Paged_Reader(override val offset: Int) extends Byte_Reader
{
override lazy val source: CharSequence = restricted_seq
- def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\032'
+ def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\u001a'
def rest: Paged_Reader = if (seq.isDefinedAt(offset)) new Paged_Reader(offset + 1) else this
def pos: InputPosition = new OffsetPosition(source, offset)
def atEnd: Boolean = !seq.isDefinedAt(offset)
--- a/src/Pure/System/isabelle_process.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/System/isabelle_process.scala Fri May 02 23:31:25 2014 +0200
@@ -12,7 +12,7 @@
class Isabelle_Process(
- receiver: Prover.Message => Unit = System.out.println(_),
+ receiver: Prover.Message => Unit = Console.println(_),
prover_args: List[String] = Nil)
{
/* text and tree data */
--- a/src/Pure/System/options.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/System/options.scala Fri May 02 23:31:25 2014 +0200
@@ -147,13 +147,13 @@
val options = (Options.init() /: more_options)(_ + _)
if (get_option != "")
- System.out.println(options.check_name(get_option).value)
+ Console.println(options.check_name(get_option).value)
if (export_file != "")
File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
if (get_option == "" && export_file == "")
- System.out.println(options.print)
+ Console.println(options.print)
case _ => error("Bad arguments:\n" + cat_lines(args))
}
--- a/src/Pure/Tools/build.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/Tools/build.scala Fri May 02 23:31:25 2014 +0200
@@ -32,13 +32,17 @@
class Console_Progress(verbose: Boolean) extends Progress
{
- override def echo(msg: String) { System.out.println(msg) }
+ override def echo(msg: String) { Console.println(msg) }
override def theory(session: String, theory: String): Unit =
if (verbose) echo(session + ": theory " + theory)
@volatile private var is_stopped = false
def interrupt_handler[A](e: => A): A = Interrupt.handler { is_stopped = true } { e }
- override def stopped: Boolean = is_stopped
+ override def stopped: Boolean =
+ {
+ if (Thread.interrupted) is_stopped = true
+ is_stopped
+ }
}
@@ -807,7 +811,11 @@
// scheduler loop
case class Result(current: Boolean, heap: String, rc: Int)
- def sleep(): Unit = Thread.sleep(500)
+ def sleep()
+ {
+ try { Thread.sleep(500) }
+ catch { case Exn.Interrupt() => Thread.currentThread.interrupt }
+ }
@tailrec def loop(
pending: Queue,
--- a/src/Pure/Tools/check_source.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/Tools/check_source.scala Fri May 02 23:31:25 2014 +0200
@@ -37,5 +37,25 @@
if (content.contains('\r'))
Output.warning("CR character" + Position.here(file_pos))
}
+
+ def check_hg(root: Path)
+ {
+ Output.writeln("Checking " + root + " ...")
+ Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error
+ for {
+ file <- Isabelle_System.hg("manifest", root).check_error.out_lines
+ if file.endsWith(".thy") || file.endsWith(".ML")
+ } check_file(root + Path.explode(file))
+ }
+
+
+ /* command line entry point */
+
+ def main(args: Array[String])
+ {
+ Command_Line.tool0 {
+ for (root <- args) check_hg(Path.explode(root))
+ }
+ }
}
--- a/src/Pure/Tools/doc.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/Tools/doc.scala Fri May 02 23:31:25 2014 +0200
@@ -77,7 +77,7 @@
def view(path: Path)
{
- if (path.is_file) System.out.println(Library.trim_line(File.read(path)))
+ if (path.is_file) Console.println(Library.trim_line(File.read(path)))
else {
val pdf = path.ext("pdf")
if (pdf.is_file) Isabelle_System.pdf_viewer(pdf)
@@ -92,7 +92,7 @@
{
Command_Line.tool0 {
val entries = contents()
- if (args.isEmpty) System.out.println(cat_lines(contents_lines().map(_._2)))
+ if (args.isEmpty) Console.println(cat_lines(contents_lines().map(_._2)))
else {
args.foreach(arg =>
entries.collectFirst { case Doc(name, _, path) if arg == name => path } match {
--- a/src/Pure/Tools/keywords.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Pure/Tools/keywords.scala Fri May 02 23:31:25 2014 +0200
@@ -141,7 +141,7 @@
}
val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
- System.err.println(file)
+ Output.writeln(file)
File.write(Path.explode(file), output)
}
--- a/src/Tools/jEdit/etc/settings Fri May 02 21:18:50 2014 +0200
+++ b/src/Tools/jEdit/etc/settings Fri May 02 23:31:25 2014 +0200
@@ -7,7 +7,7 @@
#JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss1m"
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"
#JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss8m"
-JEDIT_SYSTEM_OPTIONS="-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dscala.repl.no-threads=true"
+JEDIT_SYSTEM_OPTIONS="-Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle"
ISABELLE_JEDIT_OPTIONS=""
--- a/src/Tools/jEdit/src/plugin.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Fri May 02 23:31:25 2014 +0200
@@ -147,7 +147,7 @@
/* current document content */
- def snapshot(view: View): Document.Snapshot =
+ def snapshot(view: View): Document.Snapshot = Swing_Thread.now
{
val buffer = view.getBuffer
document_model(buffer) match {
@@ -156,7 +156,7 @@
}
}
- def rendering(view: View): Rendering =
+ def rendering(view: View): Rendering = Swing_Thread.now
{
val text_area = view.getTextArea
document_view(text_area) match {
--- a/src/Tools/jEdit/src/scala_console.scala Fri May 02 21:18:50 2014 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala Fri May 02 23:31:25 2014 +0200
@@ -59,7 +59,7 @@
/* global state -- owned by Swing thread */
- private var interpreters = Map[Console, IMain]()
+ private var interpreters = Map.empty[Console, Interpreter]
private var global_console: Console = null
private var global_out: Output = null
@@ -67,16 +67,22 @@
private val console_stream = new OutputStream
{
- val buf = new StringBuilder
+ val buf = new StringBuffer
override def flush()
{
- val str = UTF8.decode_permissive(buf.toString)
- buf.clear
- if (global_out == null) System.out.print(str)
- else Swing_Thread.now { global_out.writeAttrs(null, str) }
+ val s = buf.synchronized { val s = buf.toString; buf.setLength(0); s }
+ val str = UTF8.decode_permissive(s)
+ Swing_Thread.later {
+ if (global_out == null) System.out.print(str)
+ else global_out.writeAttrs(null, str)
+ }
}
override def close() { flush () }
- def write(byte: Int) { buf.append(byte.toChar) }
+ def write(byte: Int) {
+ val c = byte.toChar
+ buf.append(c)
+ if (c == '\n') flush()
+ }
}
private val console_writer = new Writer
@@ -101,18 +107,72 @@
global_console = console
global_out = out
global_err = if (err == null) out else err
- val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
- console_stream.flush
- global_console = null
- global_out = null
- global_err = null
- Exn.release(res)
+ try {
+ scala.Console.withErr(console_stream) {
+ scala.Console.withOut(console_stream) { e }
+ }
+ }
+ finally {
+ console_stream.flush
+ global_console = null
+ global_out = null
+ global_err = null
+ }
}
private def report_error(str: String)
{
if (global_console == null || global_err == null) System.err.println(str)
- else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
+ else Swing_Thread.later { global_err.print(global_console.getErrorColor, str) }
+ }
+
+
+ /* interpreter thread */
+
+ private abstract class Request
+ private case class Start(console: Console) extends Request
+ private case class Execute(console: Console, out: Output, err: Output, command: String)
+ extends Request
+
+ private class Interpreter
+ {
+ private val running = Synchronized(None: Option[Thread])
+ def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
+
+ private val settings = new GenericRunnerSettings(report_error)
+ settings.classpath.value = reconstruct_classpath()
+
+ private val interp = new IMain(settings, new PrintWriter(console_writer, true))
+ {
+ override def parentClassLoader = new JARClassLoader
+ }
+ interp.setContextClassLoader
+
+ val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
+ {
+ case Start(console) =>
+ interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
+ interp.bind("console", "console.Console", console)
+ interp.interpret("import isabelle.jedit.PIDE")
+ true
+
+ case Execute(console, out, err, command) =>
+ with_console(console, out, err) {
+ try {
+ running.change(_ => Some(Thread.currentThread()))
+ interp.interpret(command)
+ }
+ finally {
+ running.change(_ => None)
+ Thread.interrupted()
+ }
+ Swing_Thread.later {
+ if (err != null) err.commandDone()
+ out.commandDone()
+ }
+ true
+ }
+ }
}
@@ -120,24 +180,20 @@
override def openConsole(console: Console)
{
- val settings = new GenericRunnerSettings(report_error)
- settings.classpath.value = reconstruct_classpath()
-
- val interp = new IMain(settings, new PrintWriter(console_writer, true))
- {
- override def parentClassLoader = new JARClassLoader
- }
- interp.setContextClassLoader
- interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
- interp.bind("console", "console.Console", console)
- interp.interpret("import isabelle.jedit.PIDE")
-
+ val interp = new Interpreter
+ interp.thread.send(Start(console))
interpreters += (console -> interp)
}
override def closeConsole(console: Console)
{
- interpreters -= console
+ interpreters.get(console) match {
+ case Some(interp) =>
+ interp.interrupt
+ interp.thread.shutdown
+ interpreters -= console
+ case None =>
+ }
}
override def printInfoMessage(out: Output)
@@ -158,19 +214,11 @@
override def execute(console: Console, input: String, out: Output, err: Output, command: String)
{
- val interp = interpreters(console)
- with_console(console, out, err) { interp.interpret(command) }
- if (err != null) err.commandDone()
- out.commandDone()
+ interpreters(console).thread.send(Execute(console, out, err, command))
}
override def stop(console: Console)
{
- closeConsole(console)
- console.clear
- openConsole(console)
- val out = console.getOutput
- out.commandDone
- printPrompt(console, out)
+ interpreters.get(console).foreach(_.interrupt)
}
}