products/sources/formale Sprachen/Isabelle/Tools/jEdit/src/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Advanced.thy   Sprache: Scala

Untersuchung Isabelle©
/*  Title:      Tools/jEdit/src/scala_console.scala
    Author:     Makarius

Scala instance of Console plugin.
*/

package isabelle.jedit


import isabelle._

import console.{Console, ConsolePane, Shell, Output}
import org.gjt.sp.jedit.JARClassLoader
import java.io.{OutputStream, Writer, PrintWriter}


class Scala_Console extends Shell("Scala")
{
  /* global state -- owned by GUI thread */

  @volatile private var interpreters = Map.empty[Console, Interpreter]

  @volatile private var global_console: Console = null
  @volatile private var global_out: Output = null
  @volatile private var global_err: Output = null

  private val console_stream = new OutputStream
  {
    val buf = new StringBuilder(100)

    override def flush()
    {
      val s = buf.synchronized { val s = buf.toString; buf.clear; s }
      val str = UTF8.decode_permissive(s)
      GUI_Thread.later {
        if (global_out == null) System.out.print(str)
        else global_out.writeAttrs(null, str)
      }
      Time.seconds(0.01).sleep  // FIXME adhoc delay to avoid loosing output
    }

    override def close() { flush () }

    def write(byte: Int)
    {
      val c = byte.toChar
      buf.synchronized { buf.append(c) }
      if (c == '\n') flush()
    }
  }

  private val console_writer = new Writer
  {
    def flush() { console_stream.flush() }
    def close() { console_stream.flush() }

    def write(cbuf: Array[Char], off: Int, len: Int)
    {
      if (len > 0) {
        UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
      }
    }
  }

  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
  {
    global_console = console
    global_out = out
    global_err = if (err == null) out else err
    try {
      scala.Console.withErr(console_stream) {
        scala.Console.withOut(console_stream) { e }
      }
    }
    finally {
      console_stream.flush
      global_console = null
      global_out = null
      global_err = null
    }
  }

  private def report_error(str: String)
  {
    if (global_console == null || global_err == null) isabelle.Output.writeln(str)
    else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
  }


  /* interpreter thread */

  private abstract class Request
  private case class Start(console: Console) extends Request
  private case class Execute(console: Console, out: Output, err: Output, command: String)
    extends Request

  private class Interpreter
  {
    private val running = Synchronized[Option[Thread]](None)
    def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }

    private val interp =
      Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
        interpreter(
          print_writer = new PrintWriter(console_writer, true),
          class_loader = new JARClassLoader)

    val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
    {
      case Start(console) =>
        interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
        interp.bind("console", "console.Console", console)
        interp.interpret("import isabelle._; import isabelle.jedit._")
        true

      case Execute(console, out, err, command) =>
        with_console(console, out, err) {
          try {
            running.change(_ => Some(Thread.currentThread()))
            interp.interpret(command)
          }
          finally {
            running.change(_ => None)
            Exn.Interrupt.dispose()
          }
          GUI_Thread.later {
            if (err != null) err.commandDone()
            out.commandDone()
          }
          true
        }
    }
  }


  /* jEdit console methods */

  override def openConsole(console: Console)
  {
    val interp = new Interpreter
    interp.thread.send(Start(console))
    interpreters += (console -> interp)
  }

  override def closeConsole(console: Console)
  {
    interpreters.get(console) match {
      case Some(interp) =>
        interp.interrupt
        interp.thread.shutdown
        interpreters -= console
      case None =>
    }
  }

  override def printInfoMessage(out: Output)
  {
    out.print(null,
     "This shell evaluates Isabelle/Scala expressions.\n\n" +
     "The contents of package isabelle and isabelle.jedit are imported.\n" +
     "The following special toplevel bindings are provided:\n" +
     " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
     " console -- jEdit Console plugin\n" +
     " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
  }

  override def printPrompt(console: Console, out: Output)
  {
    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
    out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
  }

  override def execute(console: Console, input: String, out: Output, err: Output, command: String)
  {
    interpreters(console).thread.send(Execute(console, out, err, command))
  }

  override def stop(console: Console)
  {
    interpreters.get(console).foreach(_.interrupt)
  }
}

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.21Angebot  (vorverarbeitet)  ¤



Begriffe der Konzeptbildung
Was zu einem Entwurf gehört
Begriffe der Konzeptbildung
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff