--- a/Admin/build Wed Apr 23 11:29:39 2014 +0200
+++ b/Admin/build Wed Apr 23 17:05:48 2014 +0200
@@ -74,7 +74,7 @@
## main
-#workaround for scalac 2.10.2
+#FIXME workaround for scalac 2.11.0
function stty() { :; }
export -f stty
--- a/Admin/components/components.sha1 Wed Apr 23 11:29:39 2014 +0200
+++ b/Admin/components/components.sha1 Wed Apr 23 17:05:48 2014 +0200
@@ -66,6 +66,7 @@
207e4916336335386589c918c5e3f3dcc14698f2 scala-2.10.2.tar.gz
21c8ee274ffa471ab54d4196ecd827bf3d43e591 scala-2.10.3.tar.gz
d4688ddaf83037ca43b5bf271325fc53ae70e3aa scala-2.10.4.tar.gz
+44d12297a78988ffd34363535e6a8e0d94c1d8b5 scala-2.11.0.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
43b5afbcad575ab6817d2289756ca22fd2ef43a9 spass-3.8ds.tar.gz
--- a/Admin/components/main Wed Apr 23 11:29:39 2014 +0200
+++ b/Admin/components/main Wed Apr 23 17:05:48 2014 +0200
@@ -9,7 +9,7 @@
jortho-1.0-2
kodkodi-1.5.2
polyml-5.5.1-1
-scala-2.10.4
+scala-2.11.0
spass-3.8ds
z3-3.2-1
z3-4.3.0
--- a/etc/settings Wed Apr 23 11:29:39 2014 +0200
+++ b/etc/settings Wed Apr 23 17:05:48 2014 +0200
@@ -12,16 +12,11 @@
### Isabelle/Scala
###
-ISABELLE_SCALA_BUILD_OPTIONS="-nowarn -target:jvm-1.5 -Xmax-classfile-name 130"
+ISABELLE_SCALA_BUILD_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.7 -Xmax-classfile-name 130"
ISABELLE_JAVA_SYSTEM_OPTIONS="-Dfile.encoding=UTF-8 -server"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-library.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-swing.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-actors.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-compiler.jar"
-classpath "$ISABELLE_HOME/lib/classes/scala-reflect.jar"
#paranoia setting -- avoid problems of Java/Swing versus XIM/IBus etc.
unset XMODIFIERS
--- a/src/Pure/Concurrent/future.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/Concurrent/future.scala Wed Apr 23 17:05:48 2014 +0200
@@ -2,30 +2,27 @@
Module: PIDE
Author: Makarius
-Future values.
-
-Notable differences to scala.actors.Future (as of Scala 2.7.7):
-
- * We capture/release exceptions as in the ML variant.
-
- * Future.join works for *any* actor, not just the one of the
- original fork.
+Value-oriented parallelism via futures and promises in Scala -- with
+signatures as in Isabelle/ML.
*/
package isabelle
-import scala.actors.Actor._
+import scala.util.{Success, Failure}
+import scala.concurrent.{Future => Scala_Future, Promise => Scala_Promise, Await}
+import scala.concurrent.duration.Duration
+import scala.concurrent.ExecutionContext.Implicits.global
object Future
{
def value[A](x: A): Future[A] = new Finished_Future(x)
- def fork[A](body: => A): Future[A] = new Pending_Future(body)
- def promise[A]: Promise[A] = new Promise_Future
+ def fork[A](body: => A): Future[A] = new Pending_Future(Scala_Future[A](body))
+ def promise[A]: Promise[A] = new Promise_Future[A](Scala_Promise[A])
}
-abstract class Future[A]
+trait Future[A]
{
def peek: Option[Exn.Result[A]]
def is_finished: Boolean = peek.isDefined
@@ -41,71 +38,43 @@
}
}
-abstract class Promise[A] extends Future[A]
+trait Promise[A] extends Future[A]
{
def fulfill_result(res: Exn.Result[A]): Unit
- def fulfill(x: A) { fulfill_result(Exn.Res(x)) }
+ def fulfill(x: A): Unit
}
+
private class Finished_Future[A](x: A) extends Future[A]
{
val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
val join: A = x
}
-private class Pending_Future[A](body: => A) extends Future[A]
+private class Pending_Future[A](future: Scala_Future[A]) extends Future[A]
{
- @volatile private var result: Option[Exn.Result[A]] = None
-
- private val evaluator = actor {
- result = Some(Exn.capture(body))
- loop { react { case _ => reply(result.get) } }
- }
+ def peek: Option[Exn.Result[A]] =
+ future.value match {
+ case Some(Success(x)) => Some(Exn.Res(x))
+ case Some(Failure(e)) => Some(Exn.Exn(e))
+ case None => None
+ }
+ override def is_finished: Boolean = future.isCompleted
- def peek: Option[Exn.Result[A]] = result
-
- def join: A =
- Exn.release {
- peek match {
- case Some(res) => res
- case None => (evaluator !? ()).asInstanceOf[Exn.Result[A]]
- }
- }
+ def join: A = Await.result(future, Duration.Inf)
+ override def map[B](f: A => B): Future[B] = new Pending_Future[B](future.map(f))
}
-private class Promise_Future[A] extends Promise[A]
+private class Promise_Future[A](promise: Scala_Promise[A])
+ extends Pending_Future(promise.future) with Promise[A]
{
- @volatile private var result: Option[Exn.Result[A]] = None
-
- private case object Read
- private case class Write(res: Exn.Result[A])
+ override def is_finished: Boolean = promise.isCompleted
- private val receiver = actor {
- loop {
- react {
- case Read if result.isDefined => reply(result.get)
- case Write(res) =>
- if (result.isDefined) reply(false)
- else { result = Some(res); reply(true) }
- }
+ def fulfill_result(res: Exn.Result[A]): Unit =
+ res match {
+ case Exn.Res(x) => promise.success(x)
+ case Exn.Exn(e) => promise.failure(e)
}
- }
-
- def peek: Option[Exn.Result[A]] = result
-
- def join: A =
- Exn.release {
- result match {
- case Some(res) => res
- case None => (receiver !? Read).asInstanceOf[Exn.Result[A]]
- }
- }
-
- def fulfill_result(res: Exn.Result[A]) {
- receiver !? Write(res) match {
- case false => error("Duplicate fulfillment of promise")
- case _ =>
- }
- }
+ def fulfill(x: A): Unit = promise.success(x)
}
--- a/src/Pure/Concurrent/simple_thread.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala Wed Apr 23 17:05:48 2014 +0200
@@ -15,10 +15,10 @@
object Simple_Thread
{
- /* prending interrupts */
+ /* pending interrupts */
def interrupted_exception(): Unit =
- if (Thread.interrupted()) throw new InterruptedException
+ if (Thread.interrupted()) throw Exn.Interrupt()
/* plain thread */
--- a/src/Pure/GUI/swing_thread.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/GUI/swing_thread.scala Wed Apr 23 17:05:48 2014 +0200
@@ -35,7 +35,7 @@
{
if (SwingUtilities.isEventDispatchThread()) body
else {
- lazy val result = { assert(); Exn.capture(body) }
+ lazy val result = { assert { Exn.capture(body) } }
SwingUtilities.invokeAndWait(new Runnable { def run = result })
Exn.release(result)
}
@@ -69,7 +69,7 @@
timer.setRepeats(false)
timer.addActionListener(new ActionListener {
override def actionPerformed(e: ActionEvent) {
- assert()
+ assert {}
timer.setInitialDelay(time.ms.toInt)
action
}
@@ -77,20 +77,20 @@
def invoke()
{
- require()
+ require {}
if (first) timer.start() else timer.restart()
}
def revoke()
{
- require()
+ require {}
timer.stop()
timer.setInitialDelay(time.ms.toInt)
}
def postpone(alt_time: Time)
{
- require()
+ require {}
if (timer.isRunning) {
timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
timer.restart()
--- a/src/Pure/GUI/system_dialog.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/GUI/system_dialog.scala Wed Apr 23 17:05:48 2014 +0200
@@ -26,7 +26,7 @@
private def check_window(): Window =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
_window match {
case Some(window) => window
@@ -48,7 +48,7 @@
private def conclude()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
require(_return_code.isDefined)
_window match {
--- a/src/Pure/General/completion.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/completion.scala Wed Apr 23 17:05:48 2014 +0200
@@ -266,10 +266,10 @@
/* abbreviations */
- private val caret_indicator = '\007'
+ private val caret_indicator = '\u0007'
private val antiquote = "@{"
private val default_abbrs =
- List("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
+ List("@{" -> "@{\u0007}", "`" -> "\\<open>\u0007\\<close>", "`" -> "\\<open>", "`" -> "\\<close>")
}
final class Completion private(
--- a/src/Pure/General/exn.ML Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/exn.ML Wed Apr 23 17:05:48 2014 +0200
@@ -19,6 +19,7 @@
val interrupt_exn: 'a result
val is_interrupt_exn: 'a result -> bool
val interruptible_capture: ('a -> 'b) -> 'a -> 'b result
+ val return_code: exn -> int -> int
val capture_exit: int -> ('a -> 'b) -> 'a -> 'b
exception EXCEPTIONS of exn list
end;
@@ -68,10 +69,13 @@
Res (f x) handle e => if is_interrupt e then reraise e else Exn e;
-(* POSIX process wrapper *)
+(* POSIX return code *)
+
+fun return_code exn rc =
+ if is_interrupt exn then (130: int) else rc;
fun capture_exit rc f x =
- f x handle exn => if is_interrupt exn then exit (130: int) else exit rc;
+ f x handle exn => exit (return_code exn rc);
(* concatenated exceptions *)
--- a/src/Pure/General/exn.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/exn.scala Wed Apr 23 17:05:48 2014 +0200
@@ -27,6 +27,34 @@
}
+ /* interrupts */
+
+ def is_interrupt(exn: Throwable): Boolean =
+ {
+ var found_interrupt = false
+ var e = exn
+ while (!found_interrupt && e != null) {
+ found_interrupt |= e.isInstanceOf[InterruptedException]
+ e = e.getCause
+ }
+ found_interrupt
+ }
+
+ object Interrupt
+ {
+ def apply(): Throwable = new InterruptedException
+ def unapply(exn: Throwable): Boolean = is_interrupt(exn)
+
+ val return_code = 130
+ }
+
+
+ /* POSIX return code */
+
+ def return_code(exn: Throwable, rc: Int): Int =
+ if (is_interrupt(exn)) Interrupt.return_code else rc
+
+
/* message */
private val runtime_exception = Class.forName("java.lang.RuntimeException")
@@ -44,8 +72,12 @@
else None
def message(exn: Throwable): String =
- user_message(exn) getOrElse
- (if (exn.isInstanceOf[InterruptedException]) "Interrupt"
- else exn.toString)
+ user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
+
+
+ /* TTY error message */
+
+ def error_message(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
+ def error_message(exn: Throwable): String = error_message(message(exn))
}
--- a/src/Pure/General/linear_set.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/linear_set.scala Wed Apr 23 17:05:48 2014 +0200
@@ -10,16 +10,18 @@
import scala.collection.SetLike
-import scala.collection.generic.{ImmutableSetFactory, CanBuildFrom,
- GenericSetTemplate, GenericCompanion}
+import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion}
+import scala.collection.mutable.{Builder, SetBuilder}
+import scala.language.higherKinds
-object Linear_Set extends ImmutableSetFactory[Linear_Set]
+object Linear_Set extends SetFactory[Linear_Set]
{
private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
override def empty[A] = empty_val.asInstanceOf[Linear_Set[A]]
implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A]
+ def newBuilder[A]: Builder[A, Linear_Set[A]] = new SetBuilder[A, Linear_Set[A]](empty[A])
class Duplicate[A](x: A) extends Exception
class Undefined[A](x: A) extends Exception
--- a/src/Pure/General/scan.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/General/scan.scala Wed Apr 23 17:05:48 2014 +0200
@@ -238,7 +238,7 @@
var rest = in
def try_parse[A](p: Parser[A]): Boolean =
{
- parse(p ^^^ (), rest) match {
+ parse(p ^^^ (()), rest) match {
case Success(_, next) => { rest = next; true }
case _ => false
}
--- a/src/Pure/PIDE/query_operation.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/PIDE/query_operation.scala Wed Apr 23 17:05:48 2014 +0200
@@ -65,7 +65,7 @@
private def content_update()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
/* snapshot */
@@ -174,7 +174,7 @@
def apply_query(query: List[String])
{
- Swing_Thread.require()
+ Swing_Thread.require {}
editor.current_node_snapshot(editor_context) match {
case Some(snapshot) =>
@@ -199,7 +199,7 @@
def locate_query()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
for {
command <- current_location
--- a/src/Pure/PIDE/session.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/PIDE/session.scala Wed Apr 23 17:05:48 2014 +0200
@@ -88,8 +88,8 @@
}
catch {
case exn: Throwable =>
- System.err.println("Failed to initialize protocol handler: " +
- name + "\n" + Exn.message(exn))
+ System.err.println(Exn.error_message(
+ "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)))
(handlers1, functions1)
}
@@ -102,8 +102,8 @@
try { functions(a)(msg) }
catch {
case exn: Throwable =>
- System.err.println("Failed invocation of protocol function: " +
- quote(a) + "\n" + Exn.message(exn))
+ System.err.println(Exn.error_message(
+ "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)))
false
}
case _ => false
--- a/src/Pure/PIDE/yxml.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/PIDE/yxml.scala Wed Apr 23 17:05:48 2014 +0200
@@ -16,8 +16,8 @@
{
/* chunk markers */
- val X = '\5'
- val Y = '\6'
+ val X = '\u0005'
+ val Y = '\u0006'
val is_X = (c: Char) => c == X
val is_Y = (c: Char) => c == Y
--- a/src/Pure/System/command_line.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/System/command_line.scala Wed Apr 23 17:05:48 2014 +0200
@@ -30,8 +30,8 @@
catch {
case exn: Throwable =>
if (debug) exn.printStackTrace
- System.err.println(Exn.message(exn))
- 2
+ System.err.println(Exn.error_message(exn))
+ Exn.return_code(exn, 2)
}
sys.exit(rc)
}
--- a/src/Pure/System/invoke_scala.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/System/invoke_scala.scala Wed Apr 23 17:05:48 2014 +0200
@@ -58,7 +58,7 @@
Exn.capture { f(arg) } match {
case Exn.Res(null) => (Tag.NULL, "")
case Exn.Res(res) => (Tag.OK, res)
- case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "")
+ case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
}
case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
--- a/src/Pure/System/isabelle_system.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Apr 23 17:05:48 2014 +0200
@@ -107,7 +107,7 @@
if (rc != 0) error(output)
val entries =
- (for (entry <- File.read(dump) split "\0" if entry != "") yield {
+ (for (entry <- File.read(dump) split "\u0000" if entry != "") yield {
val i = entry.indexOf('=')
if (i <= 0) (entry -> "")
else (entry.substring(0, i) -> entry.substring(i + 1))
@@ -332,7 +332,7 @@
kill_cmd(signal)
kill_cmd("0") == 0
}
- catch { case _: InterruptedException => true }
+ catch { case Exn.Interrupt() => true }
}
private def multi_kill(signal: String): Boolean =
@@ -341,7 +341,7 @@
var count = 10
while (running && count > 0) {
if (kill(signal)) {
- try { Thread.sleep(100) } catch { case _: InterruptedException => }
+ try { Thread.sleep(100) } catch { case Exn.Interrupt() => }
count -= 1
}
else running = false
@@ -446,6 +446,19 @@
def set_rc(i: Int): Bash_Result = copy(rc = i)
}
+ private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
+ {
+ private var count = 0L
+ def apply(progress: String => Unit)(line: String): Unit = synchronized {
+ progress(line)
+ count = count + line.length + 1
+ progress_limit match {
+ case Some(limit) if count > limit => proc.terminate
+ case _ =>
+ }
+ }
+ }
+
def bash_env(cwd: JFile, env: Map[String, String], script: String,
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
@@ -456,17 +469,7 @@
val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
proc.stdin.close
- val limited = new Object {
- private var count = 0L
- def apply(progress: String => Unit)(line: String): Unit = synchronized {
- progress(line)
- count = count + line.length + 1
- progress_limit match {
- case Some(limit) if count > limit => proc.terminate
- case _ =>
- }
- }
- }
+ val limited = new Limited_Progress(proc, progress_limit)
val (_, stdout) =
Simple_Thread.future("bash_stdout") {
File.read_lines(proc.stdout, limited(progress_stdout))
@@ -478,7 +481,7 @@
val rc =
try { proc.join }
- catch { case e: InterruptedException => proc.terminate; 130 }
+ catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
Bash_Result(stdout.join, stderr.join, rc)
}
}
--- a/src/Pure/Tools/build.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/Tools/build.scala Wed Apr 23 17:05:48 2014 +0200
@@ -423,6 +423,8 @@
verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
{ case (deps, (name, info)) =>
+ if (progress.stopped) throw Exn.Interrupt()
+
try {
val (preloaded, parent_syntax) =
info.parent match {
@@ -605,7 +607,7 @@
args_file.delete
timer.map(_.cancel())
- if (res.rc == 130) {
+ if (res.rc == Exn.Interrupt.return_code) {
if (timeout) res.add_err("*** Timeout").set_rc(1)
else res.add_err("*** Interrupt")
}
@@ -832,7 +834,7 @@
File.write(output_dir + log(name), Library.terminate_lines(res.out_lines))
progress.echo(name + " FAILED")
- if (res.rc != 130) {
+ if (res.rc != Exn.Interrupt.return_code) {
progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
val lines = res.out_lines.filterNot(_.startsWith("\f"))
val tail = lines.drop(lines.length - 20 max 0)
--- a/src/Pure/Tools/main.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/Tools/main.scala Wed Apr 23 17:05:48 2014 +0200
@@ -25,7 +25,7 @@
def exit_error(exn: Throwable): Nothing =
{
GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
- system_dialog.return_code(2)
+ system_dialog.return_code(Exn.return_code(exn, 2))
system_dialog.join_exit
}
@@ -60,7 +60,9 @@
build_heap = true, more_dirs = more_dirs,
system_mode = system_mode, sessions = List(session)))
}
- catch { case exn: Throwable => (Exn.message(exn) + "\n", 2) }
+ catch {
+ case exn: Throwable => (Exn.error_message(exn) + "\n", Exn.return_code(exn, 2))
+ }
system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
system_dialog.return_code(rc)
@@ -155,7 +157,7 @@
catch { case exn: Throwable => exit_error(exn) }
if (system_dialog.stopped) {
- system_dialog.return_code(130)
+ system_dialog.return_code(Exn.Interrupt.return_code)
system_dialog.join_exit
}
}
@@ -195,7 +197,7 @@
val path = (new JFile(isabelle_home, link)).toPath
val writer = Files.newBufferedWriter(path, UTF8.charset)
- try { writer.write("!<symlink>" + content + "\0") }
+ try { writer.write("!<symlink>" + content + "\u0000") }
finally { writer.close }
Files.setAttribute(path, "dos:system", true)
--- a/src/Pure/build-jars Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/build-jars Wed Apr 23 17:05:48 2014 +0200
@@ -232,13 +232,6 @@
isabelle_jdk jar cfe "$(jvmpath "$TARGET")" isabelle.Main META-INF isabelle || \
fail "Failed to produce $TARGET"
- cp "$SCALA_HOME/lib/scala-compiler.jar" \
- "$SCALA_HOME/lib/scala-library.jar" \
- "$SCALA_HOME/lib/scala-swing.jar" \
- "$SCALA_HOME/lib/scala-actors.jar" \
- "$SCALA_HOME/lib/scala-reflect.jar" \
- "$TARGET_DIR"
-
popd >/dev/null
rm -rf classes
--- a/src/Pure/library.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Pure/library.scala Wed Apr 23 17:05:48 2014 +0200
@@ -186,5 +186,5 @@
new java.util.concurrent.Callable[A] { def call = f() }
val default_thread_pool =
- scala.collection.parallel.ThreadPoolTasks.defaultThreadPool
+ scala.collection.parallel.ForkJoinTasks.defaultForkJoinPool
}
--- a/src/Tools/Graphview/lib/Tools/graphview Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/Graphview/lib/Tools/graphview Wed Apr 23 17:05:48 2014 +0200
@@ -139,7 +139,7 @@
rm -rf classes && mkdir classes
(
- #workaround for scalac 2.10.2
+ #FIXME workaround for scalac 2.11.0
function stty() { :; }
export -f stty
--- a/src/Tools/Graphview/src/graphview.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/Graphview/src/graphview.scala Wed Apr 23 17:05:48 2014 +0200
@@ -34,7 +34,7 @@
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}
- catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
+ catch { case exn: Throwable => println(Exn.error_message(exn)); sys.exit(1) }
val top = new MainFrame {
iconImage = GUI.isabelle_image()
--- a/src/Tools/Graphview/src/mutator_event.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/Graphview/src/mutator_event.scala Wed Apr 23 17:05:48 2014 +0200
@@ -28,8 +28,8 @@
{
private val receivers = new mutable.ListBuffer[Receiver]
- def += (r: Receiver) { Swing_Thread.require(); receivers += r }
- def -= (r: Receiver) { Swing_Thread.require(); receivers -= r }
- def event(x: Message) { Swing_Thread.require(); receivers.foreach(r => r(x)) }
+ def += (r: Receiver) { Swing_Thread.require {}; receivers += r }
+ def -= (r: Receiver) { Swing_Thread.require {}; receivers -= r }
+ def event(x: Message) { Swing_Thread.require {}; receivers.foreach(r => r(x)) }
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Apr 23 17:05:48 2014 +0200
@@ -312,7 +312,7 @@
cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
(
- #workaround for scalac 2.10.2
+ #FIXME workaround for scalac 2.11.0
function stty() { :; }
export -f stty
--- a/src/Tools/jEdit/src/active.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala Wed Apr 23 17:05:48 2014 +0200
@@ -16,7 +16,7 @@
{
def action(view: View, text: String, elem: XML.Elem)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
Document_View(view.getTextArea) match {
case Some(doc_view) =>
--- a/src/Tools/jEdit/src/completion_popup.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Wed Apr 23 17:05:48 2014 +0200
@@ -49,7 +49,7 @@
def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
text_area.getClientProperty(key) match {
case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
case _ => None
@@ -75,7 +75,7 @@
def exit(text_area: JEditTextArea)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
apply(text_area) match {
case None =>
case Some(text_area_completion) =>
@@ -95,7 +95,7 @@
def dismissed(text_area: TextArea): Boolean =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
apply(text_area) match {
case Some(text_area_completion) => text_area_completion.dismissed()
case None => false
@@ -194,7 +194,7 @@
private def insert(item: Completion.Item)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val buffer = text_area.getBuffer
val range = item.range
@@ -358,7 +358,7 @@
def input(evt: KeyEvent)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
if (PIDE.options.bool("jedit_completion")) {
if (!evt.isConsumed) {
@@ -391,7 +391,7 @@
def dismissed(): Boolean =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
completion_popup match {
case Some(completion) =>
@@ -460,7 +460,7 @@
private def insert(item: Completion.Item)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val range = item.range
if (text_field.isEditable && range.length > 0) {
@@ -574,7 +574,7 @@
{
completion =>
- Swing_Thread.require()
+ Swing_Thread.require {}
require(!items.isEmpty)
val multi = items.length > 1
--- a/src/Tools/jEdit/src/document_model.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Apr 23 17:05:48 2014 +0200
@@ -25,7 +25,7 @@
def apply(buffer: Buffer): Option[Document_Model] =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
buffer.getProperty(key) match {
case model: Document_Model => Some(model)
case _ => None
@@ -34,7 +34,7 @@
def exit(buffer: Buffer)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
apply(buffer) match {
case None =>
case Some(model) =>
@@ -46,7 +46,7 @@
def init(session: Session, buffer: Buffer, node_name: Document.Node.Name): Document_Model =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
apply(buffer).map(_.deactivate)
val model = new Document_Model(session, buffer, node_name)
buffer.setProperty(key, model)
@@ -65,7 +65,7 @@
def node_header(): Document.Node.Header =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
if (is_theory) {
JEdit_Lib.buffer_lock(buffer) {
@@ -88,7 +88,7 @@
def node_required: Boolean = _node_required
def node_required_=(b: Boolean)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
if (_node_required != b && is_theory) {
_node_required = b
PIDE.options_changed()
@@ -101,7 +101,7 @@
def node_perspective(doc_blobs: Document.Blobs): (Boolean, Document.Node.Perspective_Text) =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
if (Isabelle.continuous_checking && is_theory) {
val snapshot = this.snapshot()
--- a/src/Tools/jEdit/src/document_view.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Apr 23 17:05:48 2014 +0200
@@ -29,7 +29,7 @@
def apply(text_area: TextArea): Option[Document_View] =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
text_area.getClientProperty(key) match {
case doc_view: Document_View => Some(doc_view)
case _ => None
@@ -38,7 +38,7 @@
def exit(text_area: JEditTextArea)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
apply(text_area) match {
case None =>
case Some(doc_view) =>
@@ -73,7 +73,7 @@
def perspective(snapshot: Document.Snapshot): Text.Perspective =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val active_command =
{
@@ -127,7 +127,7 @@
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
rich_text_area.robust_body(()) {
- Swing_Thread.assert()
+ Swing_Thread.assert {}
val gutter = text_area.getGutter
val width = GutterOptionPane.getSelectionAreaWidth
--- a/src/Tools/jEdit/src/find_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -54,7 +54,7 @@
private def handle_resize()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
--- a/src/Tools/jEdit/src/font_info.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/font_info.scala Wed Apr 23 17:05:48 2014 +0200
@@ -42,7 +42,7 @@
{
private def change_size(change: Float => Float)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val size0 = main_size()
val size = restrict_size(change(size0)).round
--- a/src/Tools/jEdit/src/graphview_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -29,7 +29,7 @@
private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
{
- Swing_Thread.require()
+ Swing_Thread.require {}
implicit_snapshot = snapshot
implicit_graph = graph
--- a/src/Tools/jEdit/src/info_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -30,7 +30,7 @@
private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
implicit_snapshot = snapshot
implicit_results = results
@@ -74,7 +74,7 @@
private def handle_resize()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
--- a/src/Tools/jEdit/src/isabelle.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Wed Apr 23 17:05:48 2014 +0200
@@ -153,7 +153,7 @@
def continuous_checking_=(b: Boolean)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
if (continuous_checking != b) {
PIDE.options.bool(CONTINUOUS_CHECKING) = b
@@ -179,7 +179,7 @@
private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
PIDE.document_model(view.getBuffer) match {
case Some(model) =>
model.node_required = (if (toggle) !model.node_required else set)
--- a/src/Tools/jEdit/src/isabelle_logic.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Wed Apr 23 17:05:48 2014 +0200
@@ -29,7 +29,7 @@
def logic_selector(autosave: Boolean): Option_Component =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val entries =
new Logic_Entry("", "default (" + jedit_logic() + ")") ::
--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Apr 23 17:05:48 2014 +0200
@@ -24,7 +24,7 @@
override def flush()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val doc_blobs = PIDE.document_blobs()
val edits = PIDE.document_models().flatMap(_.flushed_edits(doc_blobs))
@@ -50,7 +50,7 @@
override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
@@ -64,7 +64,7 @@
override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val text_area = view.getTextArea
val buffer = view.getBuffer
@@ -125,7 +125,7 @@
def goto_file(view: View, name: String, line: Int = 0, column: Int = 0)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
push_position(view)
--- a/src/Tools/jEdit/src/jedit_lib.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Apr 23 17:05:48 2014 +0200
@@ -74,7 +74,7 @@
def window_geometry(outer: Container, inner: Component): Window_Geometry =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val old_content = dummy_window.getContentPane
--- a/src/Tools/jEdit/src/jedit_options.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Wed Apr 23 17:05:48 2014 +0200
@@ -36,7 +36,7 @@
def make_color_component(opt: Options.Opt): Option_Component =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val opt_name = opt.name
val opt_title = opt.title("jedit")
@@ -55,7 +55,7 @@
def make_component(opt: Options.Opt): Option_Component =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val opt_name = opt.name
val opt_title = opt.title("jedit")
--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 23 17:05:48 2014 +0200
@@ -85,26 +85,26 @@
/* file content */
- def file_content(buffer: Buffer): Bytes =
+ private class File_Content_Output(buffer: Buffer) extends
+ ByteArrayOutputStream(buffer.getLength + 1)
+ {
+ def content(): Bytes = Bytes(this.buf, 0, this.count)
+ }
+
+ private class File_Content(buffer: Buffer) extends
+ BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath)
{
- val path = buffer.getPath
- val vfs = VFSManager.getVFSForPath(path)
- val content =
- new BufferIORequest(null, buffer, null, vfs, path) {
- def _run() { }
- def apply(): Bytes =
- {
- val out =
- new ByteArrayOutputStream(buffer.getLength + 1) {
- def content(): Bytes = Bytes(this.buf, 0, this.count)
- }
- write(buffer, out)
- out.content()
- }
- }
- content()
+ def _run() { }
+ def content(): Bytes =
+ {
+ val out = new File_Content_Output(buffer)
+ write(buffer, out)
+ out.content()
+ }
}
+ def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
+
/* theory text edits */
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -40,7 +40,7 @@
private def handle_resize()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
@@ -48,7 +48,7 @@
private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val (new_snapshot, new_command, new_results) =
PIDE.editor.current_node_snapshot(view) match {
--- a/src/Tools/jEdit/src/plugin.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Apr 23 17:05:48 2014 +0200
@@ -278,7 +278,7 @@
override def handleMessage(message: EBMessage)
{
- Swing_Thread.assert()
+ Swing_Thread.assert {}
if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
message match {
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Apr 23 17:05:48 2014 +0200
@@ -59,7 +59,7 @@
{
text_area =>
- Swing_Thread.require()
+ Swing_Thread.require {}
private var current_font_info: Font_Info = Font_Info.main()
private var current_body: XML.Body = Nil
@@ -77,7 +77,7 @@
def refresh()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val font = current_font_info.font
getPainter.setFont(font)
@@ -142,7 +142,7 @@
def resize(font_info: Font_Info)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
current_font_info = font_info
refresh()
@@ -150,7 +150,7 @@
def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
require(!base_snapshot.is_outdated)
current_base_snapshot = base_snapshot
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Wed Apr 23 17:05:48 2014 +0200
@@ -30,7 +30,7 @@
private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
if (stack.contains(tip)) Some(stack.span(_ != tip))
else None
@@ -47,7 +47,7 @@
results: Command.Results,
info: Text.Info[XML.Body])
{
- Swing_Thread.require()
+ Swing_Thread.require {}
stack match {
case top :: _ if top.results == results && top.info == info =>
@@ -173,7 +173,7 @@
{
tip =>
- Swing_Thread.require()
+ Swing_Thread.require {}
/* controls */
--- a/src/Tools/jEdit/src/process_indicator.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/process_indicator.scala Wed Apr 23 17:05:48 2014 +0200
@@ -25,7 +25,8 @@
space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
JEdit_Lib.load_image_icon(name).getImage)
- private val animation = new ImageIcon(passive_icon) {
+ private class Animation extends ImageIcon(passive_icon)
+ {
private var current_frame = 0
private val timer =
new Timer(0, new ActionListener {
@@ -52,6 +53,8 @@
}
}
}
+
+ private val animation = new Animation
label.icon = animation
def component: Component = label
--- a/src/Tools/jEdit/src/rich_text_area.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Apr 23 17:05:48 2014 +0200
@@ -40,7 +40,7 @@
def robust_body[A](default: A)(body: => A): A =
{
try {
- Swing_Thread.require()
+ Swing_Thread.require {}
if (buffer == text_area.getBuffer) body
else {
Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -21,7 +21,7 @@
class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
/* component state -- owned by Swing thread */
@@ -61,7 +61,7 @@
private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val questions = context.questions.values
if (do_auto_reply && !questions.isEmpty)
{
@@ -147,7 +147,7 @@
override def init()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
PIDE.session.global_options += main_actor
PIDE.session.commands_changed += main_actor
@@ -158,7 +158,7 @@
override def exit()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
PIDE.session.global_options -= main_actor
PIDE.session.commands_changed -= main_actor
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Wed Apr 23 17:05:48 2014 +0200
@@ -150,7 +150,7 @@
class Simplifier_Trace_Window(
view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val area = new Pretty_Text_Area(view)
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -55,7 +55,7 @@
private def handle_resize()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
--- a/src/Tools/jEdit/src/spell_checker.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala Wed Apr 23 17:05:48 2014 +0200
@@ -105,7 +105,7 @@
def dictionaries_selector(): Option_Component =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val option_name = "spell_checker_dictionary"
val opt = PIDE.options.value.check_name(option_name)
--- a/src/Tools/jEdit/src/syslog_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -23,7 +23,7 @@
private def update_syslog()
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val text = PIDE.session.current_syslog()
if (text != syslog.text) syslog.text = text
--- a/src/Tools/jEdit/src/text_overview.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Wed Apr 23 17:05:48 2014 +0200
@@ -64,7 +64,7 @@
override def paintComponent(gfx: Graphics)
{
super.paintComponent(gfx)
- Swing_Thread.assert()
+ Swing_Thread.assert {}
doc_view.rich_text_area.robust_body(()) {
JEdit_Lib.buffer_lock(buffer) {
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -74,7 +74,7 @@
private def handle_phase(phase: Session.Phase)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
session_phase.text = " " + phase_text(phase) + " "
}
@@ -193,7 +193,7 @@
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val snapshot = PIDE.session.snapshot()
--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Apr 23 17:05:48 2014 +0200
@@ -152,7 +152,7 @@
private def make_entries(): List[Entry] =
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val name =
Document_View(view.getTextArea) match {
@@ -175,7 +175,7 @@
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
{
- Swing_Thread.require()
+ Swing_Thread.require {}
val snapshot = PIDE.session.snapshot()
--- a/src/Tools/jEdit/src/token_markup.scala Wed Apr 23 11:29:39 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala Wed Apr 23 17:05:48 2014 +0200
@@ -42,7 +42,7 @@
def edit_control_style(text_area: TextArea, control: String)
{
- Swing_Thread.assert()
+ Swing_Thread.assert {}
val buffer = text_area.getBuffer