src/Tools/jEdit/src/jedit_lib.scala
changeset 49406 38db4832b210
child 49407 215ba6884bdf
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Sep 17 17:49:11 2012 +0200
     1.3 @@ -0,0 +1,64 @@
     1.4 +/*  Title:      Tools/jEdit/src/jedit_lib.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Misc library functions for jEdit.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +
    1.16 +import org.gjt.sp.jedit.{jEdit, Buffer, View}
    1.17 +import org.gjt.sp.jedit.buffer.JEditBuffer
    1.18 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    1.19 +
    1.20 +
    1.21 +object JEdit_Lib
    1.22 +{
    1.23 +  /* buffers */
    1.24 +
    1.25 +  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    1.26 +    Swing_Thread.now { buffer_lock(buffer) { body } }
    1.27 +
    1.28 +  def buffer_text(buffer: JEditBuffer): String =
    1.29 +    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    1.30 +
    1.31 +  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    1.32 +
    1.33 +  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
    1.34 +    Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
    1.35 +
    1.36 +  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
    1.37 +  {
    1.38 +    val name = buffer_name(buffer)
    1.39 +    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
    1.40 +  }
    1.41 +
    1.42 +
    1.43 +  /* main jEdit components */
    1.44 +
    1.45 +  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    1.46 +
    1.47 +  def jedit_buffer(name: String): Option[Buffer] =
    1.48 +    jedit_buffers().find(buffer => buffer_name(buffer) == name)
    1.49 +
    1.50 +  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    1.51 +
    1.52 +  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    1.53 +    view.getEditPanes().iterator.map(_.getTextArea)
    1.54 +
    1.55 +  def jedit_text_areas(): Iterator[JEditTextArea] =
    1.56 +    jedit_views().flatMap(jedit_text_areas(_))
    1.57 +
    1.58 +  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
    1.59 +    jedit_text_areas().filter(_.getBuffer == buffer)
    1.60 +
    1.61 +  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    1.62 +  {
    1.63 +    try { buffer.readLock(); body }
    1.64 +    finally { buffer.readUnlock() }
    1.65 +  }
    1.66 +}
    1.67 +