/*

 * Document view connected to jEdit text area

 *

 * @author Fabian Immler, TU Munich

 * @author Makarius

 */

package isabelle.jedit

import isabelle.proofdocument.{Command, Document, Session}

import scala.actors.Actor._

import java.awt.event.{MouseAdapter, MouseEvent}

import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}

import javax.swing.{JPanel, ToolTipManager}

import javax.swing.event.{CaretListener, CaretEvent}

import org.gjt.sp.jedit.gui.RolloverButton

import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}

object Document_View

{

  def choose_color(command: Command, doc: Document): Color =

  {

    doc.current_state(command).map(_.status) match {

      case Some(Command.Status.UNPROCESSED) => new Color(255, 228, 225)

      case Some(Command.Status.FINISHED) => new Color(234, 248, 255)

      case Some(Command.Status.FAILED) => new Color(255, 193, 193)

      case _ => Color.red

    }

  }

  /* document view of text area */

  private val key = new Object

  def init(model: Document_Model, text_area: TextArea): Document_View =

  {

    Swing_Thread.assert()

    val doc_view = new Document_View(model, text_area)

    text_area.putClientProperty(key, doc_view)

    doc_view.activate()

    doc_view

  }

  def apply(text_area: TextArea): Option[Document_View] =

  {

    Swing_Thread.assert()

    text_area.getClientProperty(key) match {

      case doc_view: Document_View => Some(doc_view)

      case _ => None

    }

  }

  def exit(text_area: TextArea)

  {

    Swing_Thread.assert()

    apply(text_area) match {

      case None => error("No document view for text area: " + text_area)

      case Some(doc_view) =>

        doc_view.deactivate()

        text_area.putClientProperty(key, null)

    }

  }

}

class Document_View(model: Document_Model, text_area: TextArea)

{

  private val session = model.session

  /* visible document -- owned by Swing thread */

  @volatile private var document = model.recent_document()

  /* buffer of changed commands -- owned by Swing thread */

  @volatile private var changed_commands: Set[Command] = Set()

  private val changed_delay = Swing_Thread.delay_first(100) {

    if (!changed_commands.isEmpty) {

      document = model.recent_document()

      for (cmd <- changed_commands if document.commands.contains(cmd)) { // FIXME cover doc states as well!!?

        update_syntax(cmd)

        invalidate_line(cmd)

        overview.repaint()

      }

      changed_commands = Set()

    }

  }

  /* command change actor */

  private case object Exit

  private val command_change_actor = actor {

    loop {

      react {

        case command: Command =>  // FIXME rough filtering according to document family!?

          Swing_Thread.now {

            changed_commands += command

            changed_delay()

          }

        case Exit => reply(()); exit()

        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)

      }

    }

  }

  /* text_area_extension */

  private val text_area_extension = new TextAreaExtension

  {

    override def paintValidLine(gfx: Graphics2D,

      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)

    {

      def from_current(pos: Int) = model.from_current(document, pos)

      def to_current(pos: Int) = model.to_current(document, pos)

      val metrics = text_area.getPainter.getFontMetrics

      val saved_color = gfx.getColor

      try {

        for ((command, command_start) <-

          document.command_range(from_current(start), from_current(end)))

        {

          val begin = start max to_current(command_start)

          val finish = (end - 1) min to_current(command_start + command.length)

          encolor(gfx, y, metrics.getHeight, begin, finish,

            Document_View.choose_color(command, document), true)

        }

      }

      finally { gfx.setColor(saved_color) }

    }

    override def getToolTipText(x: Int, y: Int): String =

    {

      val offset = model.from_current(document, text_area.xyToOffset(x, y))

      document.command_at(offset) match {

        case Some((command, command_start)) =>

          document.current_state(command).get.type_at(offset - command_start).getOrElse(null)

        case None => null

      }

    }

  }

  /* caret_listener */

  private var _selected_command: Command = null

  private def selected_command = _selected_command

  private def selected_command_=(cmd: Command)

  {

    _selected_command = cmd

    session.results.event(cmd)

  }

  private val caret_listener = new CaretListener

  {

    override def caretUpdate(e: CaretEvent)

    {

      document.command_at(e.getDot) match {

        case Some((command, command_start)) if (selected_command != command) =>

          selected_command = command

        case _ =>

      }

    }

  }

  /* (re)painting */

  private val update_delay = Swing_Thread.delay_first(500) { model.buffer.propertiesChanged() }

  private def update_syntax(cmd: Command)

  {

    val (line1, line2) = model.lines_of_command(document, cmd)

    if (line2 >= text_area.getFirstLine &&

      line1 <= text_area.getFirstLine + text_area.getVisibleLines)

        update_delay()

  }

  private def invalidate_line(cmd: Command) =

  {

    val (start, stop) = model.lines_of_command(document, cmd)

    text_area.invalidateLineRange(start, stop)

    if (selected_command == cmd)

      session.results.event(cmd)

  }

  private def invalidate_all() =

    text_area.invalidateLineRange(text_area.getFirstPhysicalLine,

      text_area.getLastPhysicalLine)

  private def encolor(gfx: Graphics2D,

    y: Int, height: Int, begin: Int, finish: Int, color: Color, fill: Boolean)

  {

    val start = text_area.offsetToXY(begin)

    val stop =

      if (finish < model.buffer.getLength) text_area.offsetToXY(finish)

      else {

        val p = text_area.offsetToXY(finish - 1)

        val metrics = text_area.getPainter.getFontMetrics

        p.x = p.x + (metrics.charWidth(' ') max metrics.getMaxAdvance)

        p

      }

    if (start != null && stop != null) {

      gfx.setColor(color)

      if (fill) gfx.fillRect(start.x, y, stop.x - start.x, height)

      else gfx.drawRect(start.x, y, stop.x - start.x, height)

    }

  }

  /* overview of command status left of scrollbar */

  private val overview = new JPanel(new BorderLayout)

  {

    private val WIDTH = 10

    private val HEIGHT = 2

    setPreferredSize(new Dimension(WIDTH, 0))

    setRequestFocusEnabled(false)

    addMouseListener(new MouseAdapter {

      override def mousePressed(event: MouseEvent) {

        val line = y_to_line(event.getY)

        if (line >= 0 && line < text_area.getLineCount)

          text_area.setCaretPosition(text_area.getLineStartOffset(line))

      }

    })

    override def addNotify() {

      super.addNotify()

      ToolTipManager.sharedInstance.registerComponent(this)

    }

    override def removeNotify() {

      ToolTipManager.sharedInstance.unregisterComponent(this)

      super.removeNotify

    }

    override def getToolTipText(event: MouseEvent): String =

    {

      val line = y_to_line(event.getY())

      if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"

      else ""

    }

    override def paintComponent(gfx: Graphics)

    {

      super.paintComponent(gfx)

      val buffer = model.buffer

      for ((command, start) <- document.command_range(0)) {

        val line1 = buffer.getLineOfOffset(model.to_current(document, start))

        val line2 = buffer.getLineOfOffset(model.to_current(document, start + command.length)) + 1

        val y = line_to_y(line1)

        val height = HEIGHT * (line2 - line1)

        gfx.setColor(Document_View.choose_color(command, document))

        gfx.fillRect(0, y, getWidth - 1, height)

      }

    }

    private def line_to_y(line: Int): Int =

      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)

    private def y_to_line(y: Int): Int =

      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight

  }

  /* activation */

  private def activate()

  {

    text_area.getPainter.

      addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)

    text_area.addCaretListener(caret_listener)

    text_area.addLeftOfScrollBar(overview)

    session.command_change += command_change_actor

  }

  private def deactivate()

  {

    session.command_change -= command_change_actor

    command_change_actor !? Exit

    text_area.removeLeftOfScrollBar(overview)

    text_area.removeCaretListener(caret_listener)

    text_area.getPainter.removeExtension(text_area_extension)

  }

}