/*  Title:      Tools/jEdit/src/isabelle_sidekick.scala

    Author:     Fabian Immler, TU Munich

    Author:     Makarius

SideKick parsers for Isabelle proof documents.

*/

package isabelle.jedit

import isabelle._

import scala.collection.Set

import scala.collection.immutable.TreeSet

import javax.swing.tree.DefaultMutableTreeNode

import javax.swing.text.Position

import javax.swing.Icon

import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}

import errorlist.DefaultErrorSource

import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}

object Isabelle_Sidekick

{

  def int_to_pos(offset: Text.Offset): Position =

    new Position { def getOffset = offset; override def toString = offset.toString }

  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset

  {

    protected var _name = name

    protected var _start = int_to_pos(start)

    protected var _end = int_to_pos(end)

    override def getIcon: Icon = null

    override def getShortString: String = _name

    override def getLongString: String = _name

    override def getName: String = _name

    override def setName(name: String) = _name = name

    override def getStart: Position = _start

    override def setStart(start: Position) = _start = start

    override def getEnd: Position = _end

    override def setEnd(end: Position) = _end = end

    override def toString = _name

  }

}

abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)

{

  /* parsing */

  @volatile protected var stopped = false

  override def stop() = { stopped = true }

  def parser(data: SideKickParsedData, model: Document_Model): Unit

  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =

  {

    stopped = false

    // FIXME lock buffer (!??)

    val data = new SideKickParsedData(buffer.getName)

    val root = data.root

    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))

    Swing_Thread.now { Document_Model(buffer) } match {

      case Some(model) =>

        parser(data, model)

        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))

      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))

    }

    data

  }

  /* completion */

  override def supportsCompletion = true

  override def canCompleteAnywhere = true

  override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =

  {

    val buffer = pane.getBuffer

    Isabelle.swing_buffer_lock(buffer) {

      Document_Model(buffer) match {

        case None => null

        case Some(model) =>

          val line = buffer.getLineOfOffset(caret)

          val start = buffer.getLineStartOffset(line)

          val text = buffer.getSegment(start, caret - start)

          val completion = model.session.current_syntax().completion

          completion.complete(text) match {

            case None => null

            case Some((word, cs)) =>

              val ds =

                (if (Isabelle_Encoding.is_active(buffer))

                  cs.map(Symbol.decode(_)).sortWith(_ < _)

                 else cs).filter(_ != word)

              if (ds.isEmpty) null

              else new SideKickCompletion(

                pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }

          }

      }

    }

  }

}

class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")

{

  import Thy_Syntax.Structure

  def parser(data: SideKickParsedData, model: Document_Model)

  {

    val syntax = model.session.current_syntax()

    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =

      entry match {

        case Structure.Block(name, body) =>

          val node =

            new DefaultMutableTreeNode(

              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))

          (offset /: body)((i, e) =>

            {

              make_tree(i, e) foreach (nd => node.add(nd))

              i + e.length

            })

          List(node)

        case Structure.Atom(command)

        if command.is_command && syntax.heading_level(command).isEmpty =>

          val node =

            new DefaultMutableTreeNode(

              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))

          List(node)

        case _ => Nil

      }

    val text = Isabelle.buffer_text(model.buffer)

    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)

    make_tree(0, structure) foreach (node => data.root.add(node))

  }

}

class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")

{

  def parser(data: SideKickParsedData, model: Document_Model)

  {

    val root = data.root

    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)

    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {

      snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>

          {

            val range = info.range + command_start

            val content = command.source(info.range).replace('\n', ' ')

            val info_text =

              info.info match {

                case elem @ XML.Elem(_, _) =>

                  Pretty.formatted(List(elem), margin = 40).mkString("\n")

                case x => x.toString

              }

            new DefaultMutableTreeNode(

              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {

                override def getShortString: String = content

                override def getLongString: String = info_text

                override def toString = "\"" + content + "\" " + range.toString

              })

          })

    }

  }

}