/*  Title:      jedit/plugin/IsabellePlugin.scala

    ID:         $Id$

    Author:     Makarius

Isabelle/jEdit plugin -- main setup.

*/

package isabelle.jedit

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

  }

}