# HG changeset patch
# User wenzelm
# Date 1398246042 -7200
# Node ID 229309cbc50843d2813c14c5e221024a709d5970
# Parent  27778363775d413631c6bf970b36f528acaf57b6
avoid accidental use of scala.language.reflectiveCalls;

diff -r 27778363775d -r 229309cbc508 src/Pure/System/isabelle_system.scala
--- 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))
diff -r 27778363775d -r 229309cbc508 src/Tools/jEdit/src/jedit_resources.scala
--- 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 */
 
diff -r 27778363775d -r 229309cbc508 src/Tools/jEdit/src/process_indicator.scala
--- 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