lib/jedit/plugin/isabelle/IsabellePlugin.scala

adapted to new IsabelleProcess from Pure.jar;
IsabellePlugin.result_content decodes symbols;

/*  Title:      jedit/plugin/IsabellePlugin.scala
    ID:         $Id$
    Author:     Makarius

Isabelle/jEdit plugin -- main setup.
*/

package isabelle

import org.gjt.sp.jedit.EditPlugin
import org.gjt.sp.util.Log

import errorlist.DefaultErrorSource
import errorlist.ErrorSource

import java.util.Properties
import java.lang.NumberFormatException

import scala.collection.mutable.ListBuffer
import scala.io.Source


/* Global state */

object IsabellePlugin {
  // unique ids
  @volatile
  private var idCount = 0

  def id() : String = synchronized { idCount += 1; "jedit:" + idCount }

  def idProperties(value: String) : Properties = {
     val props = new Properties
     props.setProperty(Markup.ID, value)
     props
  }

  def idProperties() : Properties = { idProperties(id()) }


  // the error source
  @volatile
  var errors: DefaultErrorSource = null

  // the Isabelle process
  @volatile
  var isabelle: IsabelleProcess = null


  // result content
  def result_content(result: IsabelleProcess.Result) =
    XML.content(isabelle.result_tree(result)).mkString("")


  // result consumers
  type consumer = IsabelleProcess.Result => Boolean
  private var consumers = new ListBuffer[consumer]

  def addConsumer(consumer: consumer) = synchronized { consumers += consumer }

  def addPermanentConsumer(consumer: IsabelleProcess.Result => Unit) = {
    addConsumer(result => { consumer(result); false })
  }

  def delConsumer(consumer: consumer) = synchronized { consumers -= consumer }

  def consume(result: IsabelleProcess.Result) : Unit = {
    synchronized { consumers.elements.toList } foreach (consumer =>
      {
        val finished =
          try { consumer(result) }
          catch { case e: Throwable => Log.log(Log.ERROR, this, e); true }
        if (finished || result == null)
          delConsumer(consumer)
      })
  }
}


/* Main plugin setup */

class IsabellePlugin extends EditPlugin {
  private var thread: Thread = null

  override def start = {
    // error source
    IsabellePlugin.errors = new DefaultErrorSource("isabelle")
    ErrorSource.registerErrorSource(IsabellePlugin.errors)

    IsabellePlugin.addPermanentConsumer (result =>
      if (result != null && result.props != null &&
          (result.kind == IsabelleProcess.Kind.WARNING ||
           result.kind == IsabelleProcess.Kind.ERROR)) {
        val typ =
          if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING
          else ErrorSource.ERROR
        (Position.line_of(result.props), Position.file_of(result.props)) match {
          case (Some(line), Some(file)) =>
            val content = IsabellePlugin.result_content(result)
            if (content.length > 0) {
              val lines = Source.fromString(content).getLines
              val err = new DefaultErrorSource.DefaultError(IsabellePlugin.errors,
                  typ, file, line - 1, 0, 0, lines.next)
              for (msg <- lines) err.addExtraMessage(msg)
              IsabellePlugin.errors.addError(err)
            }
          case _ =>
        }
      })


    // Isabelle process
    IsabellePlugin.isabelle =
      new IsabelleProcess("-mno_brackets", "-mno_type_brackets", "-mxsymbols")
    thread = new Thread (new Runnable {
      def run = {
        var result: IsabelleProcess.Result = null
        do {
          try {
            result = IsabellePlugin.isabelle.results.take
          }
          catch {
            case _: NullPointerException => result = null
            case _: InterruptedException => result = null
          }
          if (result != null) {
            System.err.println(result)   // FIXME
            IsabellePlugin.consume(result)
          }
          if (result.kind == IsabelleProcess.Kind.EXIT) {
            result = null
            IsabellePlugin.consume(null)
          }
        } while (result != null)
      }
    })
    thread.start
  }

  override def stop = {
    IsabellePlugin.isabelle.kill
    thread.interrupt; thread.join; thread = null
    IsabellePlugin.isabelle = null

    ErrorSource.unregisterErrorSource(IsabellePlugin.errors)
    IsabellePlugin.errors = null
  }
}