src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Mon Sep 17 17:49:11 2012 +0200 (2012-09-17)
changeset 49406 38db4832b210
child 49407 215ba6884bdf
permissions -rw-r--r--
somewhat more general JEdit_Lib;
tuned signatures;
wenzelm@49406
     1
/*  Title:      Tools/jEdit/src/jedit_lib.scala
wenzelm@49406
     2
    Author:     Makarius
wenzelm@49406
     3
wenzelm@49406
     4
Misc library functions for jEdit.
wenzelm@49406
     5
*/
wenzelm@49406
     6
wenzelm@49406
     7
package isabelle.jedit
wenzelm@49406
     8
wenzelm@49406
     9
wenzelm@49406
    10
import isabelle._
wenzelm@49406
    11
wenzelm@49406
    12
wenzelm@49406
    13
import org.gjt.sp.jedit.{jEdit, Buffer, View}
wenzelm@49406
    14
import org.gjt.sp.jedit.buffer.JEditBuffer
wenzelm@49406
    15
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
wenzelm@49406
    16
wenzelm@49406
    17
wenzelm@49406
    18
object JEdit_Lib
wenzelm@49406
    19
{
wenzelm@49406
    20
  /* buffers */
wenzelm@49406
    21
wenzelm@49406
    22
  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@49406
    23
    Swing_Thread.now { buffer_lock(buffer) { body } }
wenzelm@49406
    24
wenzelm@49406
    25
  def buffer_text(buffer: JEditBuffer): String =
wenzelm@49406
    26
    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
wenzelm@49406
    27
wenzelm@49406
    28
  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
wenzelm@49406
    29
wenzelm@49406
    30
  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
wenzelm@49406
    31
    Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
wenzelm@49406
    32
wenzelm@49406
    33
  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
wenzelm@49406
    34
  {
wenzelm@49406
    35
    val name = buffer_name(buffer)
wenzelm@49406
    36
    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
wenzelm@49406
    37
  }
wenzelm@49406
    38
wenzelm@49406
    39
wenzelm@49406
    40
  /* main jEdit components */
wenzelm@49406
    41
wenzelm@49406
    42
  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
wenzelm@49406
    43
wenzelm@49406
    44
  def jedit_buffer(name: String): Option[Buffer] =
wenzelm@49406
    45
    jedit_buffers().find(buffer => buffer_name(buffer) == name)
wenzelm@49406
    46
wenzelm@49406
    47
  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
wenzelm@49406
    48
wenzelm@49406
    49
  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
wenzelm@49406
    50
    view.getEditPanes().iterator.map(_.getTextArea)
wenzelm@49406
    51
wenzelm@49406
    52
  def jedit_text_areas(): Iterator[JEditTextArea] =
wenzelm@49406
    53
    jedit_views().flatMap(jedit_text_areas(_))
wenzelm@49406
    54
wenzelm@49406
    55
  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
wenzelm@49406
    56
    jedit_text_areas().filter(_.getBuffer == buffer)
wenzelm@49406
    57
wenzelm@49406
    58
  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
wenzelm@49406
    59
  {
wenzelm@49406
    60
    try { buffer.readLock(); body }
wenzelm@49406
    61
    finally { buffer.readUnlock() }
wenzelm@49406
    62
  }
wenzelm@49406
    63
}
wenzelm@49406
    64