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

     Author:     Makarius

 Misc library functions for jEdit.

 */

 package isabelle.jedit

 import isabelle._

 import java.awt.{Component, Container, Frame, Window}

 import scala.annotation.tailrec

 import org.gjt.sp.jedit.{jEdit, Buffer, View}

 import org.gjt.sp.jedit.buffer.JEditBuffer

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

 object JEdit_Lib

 {

   /* GUI components */

   def get_parent(component: Component): Option[Container] =

     component.getParent match {

       case null => None

       case parent => Some(parent)

     }

   def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {

     private var next_elem = get_parent(component)

     def hasNext(): Boolean = next_elem.isDefined

     def next(): Container =

       next_elem match {

         case Some(parent) =>

           next_elem = get_parent(parent)

           parent

         case None => Iterator.empty.next()

       }

   }

   def parent_window(component: Component): Option[Window] =

     ancestors(component).find(_.isInstanceOf[Window]).map(_.asInstanceOf[Window])

   def parent_frame(component: Component): Option[Frame] =

     ancestors(component).find(_.isInstanceOf[Frame]).map(_.asInstanceOf[Frame])

   /* buffers */

   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =

     Swing_Thread.now { buffer_lock(buffer) { body } }

   def buffer_text(buffer: JEditBuffer): String =

     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }

   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath

   def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =

     Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))

   def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =

   {

     val name = buffer_name(buffer)

     Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))

   }

   /* main jEdit components */

   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator

   def jedit_buffer(name: String): Option[Buffer] =

     jedit_buffers().find(buffer => buffer_name(buffer) == name)

   def jedit_views(): Iterator[View] = jEdit.getViews().iterator

   def jedit_text_areas(view: View): Iterator[JEditTextArea] =

     view.getEditPanes().iterator.map(_.getTextArea)

   def jedit_text_areas(): Iterator[JEditTextArea] =

     jedit_views().flatMap(jedit_text_areas(_))

   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =

     jedit_text_areas().filter(_.getBuffer == buffer)

   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =

   {

     try { buffer.readLock(); body }

     finally { buffer.readUnlock() }

   }

   /* point range */

   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =

     buffer_lock(buffer) {

       def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)

       try {

         val c = text(offset)

         if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))

           Text.Range(offset, offset + 2)

         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))

           Text.Range(offset - 1, offset + 1)

         else Text.Range(offset, offset + 1)

       }

       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }

     }

   /* visible text range */

   def visible_range(text_area: TextArea): Option[Text.Range] =

   {

     val buffer = text_area.getBuffer

     val n = text_area.getVisibleLines

     if (n > 0) {

       val start = text_area.getScreenLineStartOffset(0)

       val raw_end = text_area.getScreenLineEndOffset(n - 1)

       val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength

       Some(Text.Range(start, end))

     }

     else None

   }

   def invalidate_range(text_area: TextArea, range: Text.Range)

   {

     val buffer = text_area.getBuffer

     text_area.invalidateLineRange(

       buffer.getLineOfOffset(range.start),

       buffer.getLineOfOffset(range.stop))

   }

   /* char width */

   def char_width(text_area: TextArea): Int =

   {

     val painter = text_area.getPainter

     val font = painter.getFont

     val font_context = painter.getFontRenderContext

     font.getStringBounds(" ", font_context).getWidth.round.toInt

   }

   /* graphics range */

   case class Gfx_Range(val x: Int, val y: Int, val length: Int)

   // NB: jEdit always normalizes \r\n and \r to \n

   // NB: last line lacks \n

   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =

   {

     val buffer = text_area.getBuffer

     val p = text_area.offsetToXY(range.start)

     val end = buffer.getLength

     val stop = range.stop

     val (q, r) =

       if (stop >= end) (text_area.offsetToXY(end), char_width(text_area) * (stop - end))

       else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")

         (text_area.offsetToXY(stop - 1), char_width(text_area))

       else (text_area.offsetToXY(stop), 0)

     if (p != null && q != null && p.x < q.x + r && p.y == q.y)

       Some(Gfx_Range(p.x, p.y, q.x + r - p.x))

     else None

   }

   /* pixel range */

   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =

   {

     val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y))

     gfx_range(text_area, range) match {

       case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)

       case _ => None

     }

   }

 }