avoid accidental use of scala.language.reflectiveCalls;
authorwenzelm
Wed Apr 23 11:40:42 2014 +0200 (2014-04-23)
changeset 56666229309cbc508
parent 56665 27778363775d
child 56667 65e84b0ef974
avoid accidental use of scala.language.reflectiveCalls;
src/Pure/System/isabelle_system.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/process_indicator.scala
     1.1 --- a/src/Pure/System/isabelle_system.scala	Wed Apr 23 10:49:30 2014 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Wed Apr 23 11:40:42 2014 +0200
     1.3 @@ -446,6 +446,19 @@
     1.4      def set_rc(i: Int): Bash_Result = copy(rc = i)
     1.5    }
     1.6  
     1.7 +  private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
     1.8 +  {
     1.9 +    private var count = 0L
    1.10 +    def apply(progress: String => Unit)(line: String): Unit = synchronized {
    1.11 +      progress(line)
    1.12 +      count = count + line.length + 1
    1.13 +      progress_limit match {
    1.14 +        case Some(limit) if count > limit => proc.terminate
    1.15 +        case _ =>
    1.16 +      }
    1.17 +    }
    1.18 +  }
    1.19 +
    1.20    def bash_env(cwd: JFile, env: Map[String, String], script: String,
    1.21      progress_stdout: String => Unit = (_: String) => (),
    1.22      progress_stderr: String => Unit = (_: String) => (),
    1.23 @@ -456,17 +469,7 @@
    1.24        val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
    1.25        proc.stdin.close
    1.26  
    1.27 -      val limited = new Object {
    1.28 -        private var count = 0L
    1.29 -        def apply(progress: String => Unit)(line: String): Unit = synchronized {
    1.30 -          progress(line)
    1.31 -          count = count + line.length + 1
    1.32 -          progress_limit match {
    1.33 -            case Some(limit) if count > limit => proc.terminate
    1.34 -            case _ =>
    1.35 -          }
    1.36 -        }
    1.37 -      }
    1.38 +      val limited = new Limited_Progress(proc, progress_limit)
    1.39        val (_, stdout) =
    1.40          Simple_Thread.future("bash_stdout") {
    1.41            File.read_lines(proc.stdout, limited(progress_stdout))
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 23 10:49:30 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 23 11:40:42 2014 +0200
     2.3 @@ -85,26 +85,26 @@
     2.4  
     2.5    /* file content */
     2.6  
     2.7 -  def file_content(buffer: Buffer): Bytes =
     2.8 +  private class File_Content_Output(buffer: Buffer) extends
     2.9 +    ByteArrayOutputStream(buffer.getLength + 1)
    2.10 +  {
    2.11 +    def content(): Bytes = Bytes(this.buf, 0, this.count)
    2.12 +  }
    2.13 +
    2.14 +  private class File_Content(buffer: Buffer) extends
    2.15 +    BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath)
    2.16    {
    2.17 -    val path = buffer.getPath
    2.18 -    val vfs = VFSManager.getVFSForPath(path)
    2.19 -    val content =
    2.20 -      new BufferIORequest(null, buffer, null, vfs, path) {
    2.21 -        def _run() { }
    2.22 -        def apply(): Bytes =
    2.23 -        {
    2.24 -          val out =
    2.25 -            new ByteArrayOutputStream(buffer.getLength + 1) {
    2.26 -              def content(): Bytes = Bytes(this.buf, 0, this.count)
    2.27 -            }
    2.28 -          write(buffer, out)
    2.29 -          out.content()
    2.30 -        }
    2.31 -      }
    2.32 -    content()
    2.33 +    def _run() { }
    2.34 +    def content(): Bytes =
    2.35 +    {
    2.36 +      val out = new File_Content_Output(buffer)
    2.37 +      write(buffer, out)
    2.38 +      out.content()
    2.39 +    }
    2.40    }
    2.41  
    2.42 +  def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
    2.43 +
    2.44  
    2.45    /* theory text edits */
    2.46  
     3.1 --- a/src/Tools/jEdit/src/process_indicator.scala	Wed Apr 23 10:49:30 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/process_indicator.scala	Wed Apr 23 11:40:42 2014 +0200
     3.3 @@ -25,7 +25,8 @@
     3.4      space_explode(':', PIDE.options.string("process_active_icons")).map(name =>
     3.5        JEdit_Lib.load_image_icon(name).getImage)
     3.6  
     3.7 -  private val animation = new ImageIcon(passive_icon) {
     3.8 +  private class Animation extends ImageIcon(passive_icon)
     3.9 +  {
    3.10      private var current_frame = 0
    3.11      private val timer =
    3.12        new Timer(0, new ActionListener {
    3.13 @@ -52,6 +53,8 @@
    3.14        }
    3.15      }
    3.16    }
    3.17 +
    3.18 +  private val animation = new Animation
    3.19    label.icon = animation
    3.20  
    3.21    def component: Component = label