# HG changeset patch
# User wenzelm
# Date 1399066285 -7200
# Node ID 94477e9ff063c6aa33148d4b170ecda05f248fcf
# Parent  ba18bd41e51033669f2357866f64bc6ecda1437e# Parent  477cd67f963fffa0d623256560a7afb0a47ece03
merged

diff -r ba18bd41e510 -r 94477e9ff063 Admin/Release/CHECKLIST
--- 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;
 
diff -r ba18bd41e510 -r 94477e9ff063 NEWS
--- 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 ***
 
diff -r ba18bd41e510 -r 94477e9ff063 src/HOL/Library/Function_Algebras.thy
--- 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)
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/General/output.ML
--- 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 =
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/General/output.scala
--- 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)) }
 }
 
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/General/scan.scala
--- 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)
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/System/isabelle_process.scala
--- 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 */
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/System/options.scala
--- 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))
       }
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/Tools/build.scala
--- 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,
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/Tools/check_source.scala
--- 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))
+    }
+  }
 }
 
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/Tools/doc.scala
--- 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 {
diff -r ba18bd41e510 -r 94477e9ff063 src/Pure/Tools/keywords.scala
--- 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)
   }
 
diff -r ba18bd41e510 -r 94477e9ff063 src/Tools/jEdit/etc/settings
--- 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=""
 
diff -r ba18bd41e510 -r 94477e9ff063 src/Tools/jEdit/src/plugin.scala
--- 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 {
diff -r ba18bd41e510 -r 94477e9ff063 src/Tools/jEdit/src/scala_console.scala
--- 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)
   }
 }