--- a/src/Pure/System/isabelle_system.scala Wed Apr 23 10:49:30 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala Wed Apr 23 11:40:42 2014 +0200
@@ -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))
--- a/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 23 10:49:30 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala Wed Apr 23 11:40:42 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/process_indicator.scala Wed Apr 23 10:49:30 2014 +0200
+++ b/src/Tools/jEdit/src/process_indicator.scala Wed Apr 23 11:40:42 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