1.1 --- a/src/Tools/jEdit/src/jedit/scala_console.scala	Fri Jan 08 12:26:22 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala	Fri Jan 08 12:26:44 2010 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  package isabelle.jedit
     1.5  
     1.6  
     1.7 -import console.{Console, Shell, Output}
     1.8 +import console.{Console, ConsolePane, Shell, Output}
     1.9  
    1.10  import org.gjt.sp.jedit.jEdit
    1.11  import org.gjt.sp.jedit.MiscUtilities
    1.12 @@ -25,6 +25,18 @@
    1.13    private var global_out: Output = null
    1.14    private var global_err: Output = null
    1.15  
    1.16 +  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
    1.17 +  {
    1.18 +    global_console = console
    1.19 +    global_out = out
    1.20 +    global_err = if (err == null) out else err
    1.21 +    val res = Exn.capture { e }
    1.22 +    global_console = null
    1.23 +    global_out = null
    1.24 +    global_err = null
    1.25 +    Exn.release(res)
    1.26 +  }
    1.27 +
    1.28    private def report_error(str: String)
    1.29    {
    1.30      if (global_console == null || global_err == null) System.err.println(str)
    1.31 @@ -62,19 +74,16 @@
    1.32  
    1.33    override def printPrompt(console: Console, out: Output)
    1.34  	{
    1.35 -    out.print(console.getInfoColor, "scala> ")
    1.36 +    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
    1.37 +		out.writeAttrs(null," ")
    1.38  	}
    1.39  
    1.40    override def execute(console: Console, input: String, out: Output, err: Output, command: String)
    1.41    {
    1.42 -    global_console = console
    1.43 -    global_out = out
    1.44 -    global_err = (if (err == null) out else err)
    1.45 -
    1.46 -    interpreters(console).interpret(command)
    1.47 -
    1.48 -    global_console = null
    1.49 -    global_out = null
    1.50 -    global_err = null
    1.51 +    with_console(console, out, err) {
    1.52 +      interpreters(console).interpret(command)
    1.53 +    }
    1.54 +    if (err != null) err.commandDone()
    1.55 +		out.commandDone()
    1.56    }
    1.57  }