equal
deleted
inserted
replaced
4 * @author Makarius |
4 * @author Makarius |
5 */ |
5 */ |
6 |
6 |
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
|
9 |
|
10 import isabelle._ |
9 |
11 |
10 import console.{Console, ConsolePane, Shell, Output} |
12 import console.{Console, ConsolePane, Shell, Output} |
11 |
13 |
12 import org.gjt.sp.jedit.{jEdit, JARClassLoader} |
14 import org.gjt.sp.jedit.{jEdit, JARClassLoader} |
13 import org.gjt.sp.jedit.MiscUtilities |
15 import org.gjt.sp.jedit.MiscUtilities |
61 def flush() {} |
63 def flush() {} |
62 def close() {} |
64 def close() {} |
63 |
65 |
64 def write(cbuf: Array[Char], off: Int, len: Int) |
66 def write(cbuf: Array[Char], off: Int, len: Int) |
65 { |
67 { |
66 if (len > 0) write(new String(cbuf.subArray(off, off + len))) |
68 if (len > 0) write(new String(cbuf.slice(off, off + len))) |
67 } |
69 } |
68 |
70 |
69 override def write(str: String) |
71 override def write(str: String) |
70 { |
72 { |
71 if (global_out == null) System.out.println(str) |
73 if (global_out == null) System.out.println(str) |