isabelle: src/Tools/jEdit/src/jedit

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

     2     Author:     Makarius

     4 Misc library functions for jEdit.

     5 */

     7 package isabelle.jedit

    10 import isabelle._

    12 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}

    13 import java.awt.event.{KeyEvent, KeyListener}

    14 import javax.swing.{Icon, ImageIcon, JWindow}

    16 import scala.annotation.tailrec

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

    19 import org.gjt.sp.jedit.gui.KeyEventWorkaround

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

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

    24 object JEdit_Lib

    25 {

    26   /* bounds within multi-screen environment */

    28   def screen_bounds(screen_point: Point): Rectangle =

    29   {

    30     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment

    31     (for {

    32       device <- ge.getScreenDevices.iterator

    33       config <- device.getConfigurations.iterator

    34       bounds = config.getBounds

    35     } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds

    36   }

    39   /* window geometry measurement */

    41   private lazy val dummy_window = new JWindow

    43   final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)

    44   {

    45     def deco_width: Int = width - inner_width

    46     def deco_height: Int = height - inner_height

    47   }

    49   def window_geometry(outer: Container, inner: Component): Window_Geometry =

    50   {

    51     Swing_Thread.require()

    53     val old_content = dummy_window.getContentPane

    55     dummy_window.setContentPane(outer)

    56     dummy_window.pack

    57     dummy_window.revalidate

    59     val geometry =

    60       Window_Geometry(

    61         dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)

    63     dummy_window.setContentPane(old_content)

    65     geometry

    66   }

    69   /* GUI components */

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

    72     component.getParent match {

    73       case null => None

    74       case parent => Some(parent)

    75     }

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

    78     private var next_elem = get_parent(component)

    79     def hasNext(): Boolean = next_elem.isDefined

    80     def next(): Container =

    81       next_elem match {

    82         case Some(parent) =>

    83           next_elem = get_parent(parent)

    84           parent

    85         case None => Iterator.empty.next()

    86       }

    87   }

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

    90     ancestors(component).collectFirst({ case x: Window => x })

    93   /* basic tooltips, with multi-line support */

    95   def wrap_tooltip(text: String): String =

    96     if (text == "") null

    97     else "<html><pre>" + HTML.encode(text) + "</pre></html>"

   100   /* buffers */

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

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

   105   def buffer_text(buffer: JEditBuffer): String =

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

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

   111   /* focus of main window */

   113   def request_focus_view: Unit =

   114   {

   115     jEdit.getActiveView() match {

   116       case null =>

   117       case view =>

   118         view.getTextArea match {

   119           case null =>

   120           case text_area => text_area.requestFocus

   121         }

   122     }

   123   }

   126   /* main jEdit components */

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

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

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

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

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

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

   138   def jedit_text_areas(): Iterator[JEditTextArea] =

   139     jedit_views().flatMap(jedit_text_areas(_))

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

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

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

   145   {

   146     try { buffer.readLock(); body }

   147     finally { buffer.readUnlock() }

   148   }

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

   151   {

   152     try { buffer.beginCompoundEdit(); body }

   153     finally { buffer.endCompoundEdit() }

   154   }

   157   /* get text */

   159   def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =

   160     try { Some(buffer.getText(range.start, range.length)) }

   161     catch { case _: ArrayIndexOutOfBoundsException => None }

   164   /* buffer range */

   166   def buffer_range(buffer: JEditBuffer): Text.Range =

   167     Text.Range(0, (buffer.getLength - 1) max 0)

   170   /* point range */

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

   173     buffer_lock(buffer) {

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

   175       try {

   176         val c = text(offset)

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

   178           Text.Range(offset, offset + 2)

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

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

   181         else Text.Range(offset, offset + 1)

   182       }

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

   184     }

   187   /* visible text range */

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

   190   {

   191     val buffer = text_area.getBuffer

   192     val n = text_area.getVisibleLines

   193     if (n > 0) {

   194       val start = text_area.getScreenLineStartOffset(0)

   195       val raw_end = text_area.getScreenLineEndOffset(n - 1)

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

   197       Some(Text.Range(start, end))

   198     }

   199     else None

   200   }

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

   203   {

   204     val buffer = text_area.getBuffer

   205     text_area.invalidateLineRange(

   206       buffer.getLineOfOffset(range.start),

   207       buffer.getLineOfOffset(range.stop))

   208   }

   211   /* graphics range */

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

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

   216   // NB: last line lacks \n

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

   218   {

   219     val metric = pretty_metric(text_area.getPainter)

   220     val char_width = (metric.unit * metric.average).round.toInt

   222     val buffer = text_area.getBuffer

   224     val end = buffer.getLength

   225     val stop = range.stop

   227     val (p, q, r) =

   228       try {

   229         val p = text_area.offsetToXY(range.start)

   230         val (q, r) =

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

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

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

   234           else (text_area.offsetToXY(stop), 0)

   235         (p, q, r)

   236       }

   237       catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }

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

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

   241     else None

   242   }

   245   /* pixel range */

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

   248   {

   249     // coordinates wrt. inner painter component

   250     val painter = text_area.getPainter

   251     if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {

   252       val offset = text_area.xyToOffset(x, y, false)

   253       if (offset >= 0) {

   254         val range = point_range(text_area.getBuffer, offset)

   255         gfx_range(text_area, range) match {

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

   257           case _ => None

   258         }

   259       }

   260       else None

   261     }

   262     else None

   263   }

   266   /* pretty text metric */

   268   abstract class Pretty_Metric extends Pretty.Metric

   269   {

   270     def average: Double

   271   }

   273   def pretty_metric(painter: TextAreaPainter): Pretty_Metric =

   274     new Pretty_Metric {

   275       def string_width(s: String): Double =

   276         painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth

   278       val unit = string_width(Pretty.space)

   279       val average = string_width("mix") / (3 * unit)

   280       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit

   281     }

   284   /* icons */

   286   def load_icon(name: String): Icon =

   287   {

   288     val name1 =

   289       if (name.startsWith("idea-icons/")) {

   290         val file =

   291           Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))

   292         "jar:" + file + "!/" + name

   293       }

   294       else name

   295     val icon = GUIUtilities.loadIcon(name1)

   296     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)

   297     else icon

   298   }

   300   def load_image_icon(name: String): ImageIcon =

   301     load_icon(name) match {

   302       case icon: ImageIcon => icon

   303       case _ => error("Bad image icon: " + name)

   304     }

   307   /* key listener */

   309   def key_listener(

   310     workaround: Boolean = true,

   311     key_typed: KeyEvent => Unit = _ => (),

   312     key_pressed: KeyEvent => Unit = _ => (),

   313     key_released: KeyEvent => Unit = _ => ()): KeyListener =

   314   {

   315     def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)

   316     {

   317       val evt = if (workaround) KeyEventWorkaround.processKeyEvent(evt0) else evt0

   318       if (evt != null) handle(evt)

   319     }

   321     new KeyListener

   322     {

   323       def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }

   324       def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }

   325       def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }

   326     }

   327   }

   328 }

author	wenzelm
	Tue Aug 27 12:35:32 2013 +0200 (2013-08-27)
changeset 53226	9cf8e2263ca7
parent 53183	018d71bee930
child 53231	423e29f1f304
permissions	-rw-r--r--