# HG changeset patch # User wenzelm # Date 1399064765 -7200 # Node ID 69531d86d77e9f665877e25233db4c7c49ab8ea6 # Parent f05dadddf0956cc90a6e75d8bb026d22ea715205 more sensible interrupt of interpreter, when the user pushes Cancel button; diff -r f05dadddf095 -r 69531d86d77e src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala Fri May 02 22:33:34 2014 +0200 +++ b/src/Tools/jEdit/src/scala_console.scala Fri May 02 23:06:05 2014 +0200 @@ -59,8 +59,7 @@ /* global state -- owned by Swing thread */ - private abstract class Request - private var interpreters = Map[Console, Consumer_Thread[Request]]() + private var interpreters = Map.empty[Console, Interpreter] private var global_console: Console = null private var global_out: Output = null @@ -130,22 +129,27 @@ /* 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 def fork_interpreter(): Consumer_Thread[Request] = + private class Interpreter { - val settings = new GenericRunnerSettings(report_error) + 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() - val interp = new IMain(settings, new PrintWriter(console_writer, true)) + private val interp = new IMain(settings, new PrintWriter(console_writer, true)) { override def parentClassLoader = new JARClassLoader } interp.setContextClassLoader - Consumer_Thread.fork[Request]("Scala_Console") { + 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) @@ -154,7 +158,14 @@ case Execute(console, out, err, command) => with_console(console, out, err) { - interp.interpret(command) + 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() @@ -169,8 +180,8 @@ override def openConsole(console: Console) { - val interp = fork_interpreter() - interp.send(Start(console)) + val interp = new Interpreter + interp.thread.send(Start(console)) interpreters += (console -> interp) } @@ -178,7 +189,8 @@ { interpreters.get(console) match { case Some(interp) => - interp.shutdown + interp.interrupt + interp.thread.shutdown interpreters -= console case None => } @@ -202,16 +214,11 @@ override def execute(console: Console, input: String, out: Output, err: Output, command: String) { - interpreters(console).send(Execute(console, out, err, command)) + 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) } }