src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Tue Aug 27 22:23:40 2013 +0200 (2013-08-27)
changeset 53237 6bfe54791591
parent 53231 423e29f1f304
child 53247 bd595338ca18
permissions -rw-r--r--
enable jEdit KeyEventWorkaround uniformly;
     1 /*  Title:      Tools/jEdit/src/jedit_lib.scala
     2     Author:     Makarius
     3 
     4 Misc library functions for jEdit.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.{Component, Container, Window, GraphicsEnvironment, Point, Rectangle}
    13 import java.awt.event.{KeyEvent, KeyListener}
    14 import javax.swing.{Icon, ImageIcon, JWindow}
    15 
    16 import scala.annotation.tailrec
    17 
    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}
    22 
    23 
    24 object JEdit_Lib
    25 {
    26   /* bounds within multi-screen environment */
    27 
    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   }
    37 
    38 
    39   /* window geometry measurement */
    40 
    41   private lazy val dummy_window = new JWindow
    42 
    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   }
    48 
    49   def window_geometry(outer: Container, inner: Component): Window_Geometry =
    50   {
    51     Swing_Thread.require()
    52 
    53     val old_content = dummy_window.getContentPane
    54 
    55     dummy_window.setContentPane(outer)
    56     dummy_window.pack
    57     dummy_window.revalidate
    58 
    59     val geometry =
    60       Window_Geometry(
    61         dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
    62 
    63     dummy_window.setContentPane(old_content)
    64 
    65     geometry
    66   }
    67 
    68 
    69   /* GUI components */
    70 
    71   def get_parent(component: Component): Option[Container] =
    72     component.getParent match {
    73       case null => None
    74       case parent => Some(parent)
    75     }
    76 
    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   }
    88 
    89   def parent_window(component: Component): Option[Window] =
    90     ancestors(component).collectFirst({ case x: Window => x })
    91 
    92 
    93   /* basic tooltips, with multi-line support */
    94 
    95   def wrap_tooltip(text: String): String =
    96     if (text == "") null
    97     else "<html><pre>" + HTML.encode(text) + "</pre></html>"
    98 
    99 
   100   /* buffers */
   101 
   102   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   103     Swing_Thread.now { buffer_lock(buffer) { body } }
   104 
   105   def buffer_text(buffer: JEditBuffer): String =
   106     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
   107 
   108   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
   109 
   110 
   111   /* main jEdit components */
   112 
   113   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
   114 
   115   def jedit_buffer(name: String): Option[Buffer] =
   116     jedit_buffers().find(buffer => buffer_name(buffer) == name)
   117 
   118   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
   119 
   120   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
   121     view.getEditPanes().iterator.map(_.getTextArea)
   122 
   123   def jedit_text_areas(): Iterator[JEditTextArea] =
   124     jedit_views().flatMap(jedit_text_areas(_))
   125 
   126   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
   127     jedit_text_areas().filter(_.getBuffer == buffer)
   128 
   129   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   130   {
   131     try { buffer.readLock(); body }
   132     finally { buffer.readUnlock() }
   133   }
   134 
   135   def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
   136   {
   137     try { buffer.beginCompoundEdit(); body }
   138     finally { buffer.endCompoundEdit() }
   139   }
   140 
   141 
   142   /* get text */
   143 
   144   def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
   145     try { Some(buffer.getText(range.start, range.length)) }
   146     catch { case _: ArrayIndexOutOfBoundsException => None }
   147 
   148 
   149   /* buffer range */
   150 
   151   def buffer_range(buffer: JEditBuffer): Text.Range =
   152     Text.Range(0, (buffer.getLength - 1) max 0)
   153 
   154 
   155   /* point range */
   156 
   157   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
   158     buffer_lock(buffer) {
   159       def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
   160       try {
   161         val c = text(offset)
   162         if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
   163           Text.Range(offset, offset + 2)
   164         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
   165           Text.Range(offset - 1, offset + 1)
   166         else Text.Range(offset, offset + 1)
   167       }
   168       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
   169     }
   170 
   171 
   172   /* visible text range */
   173 
   174   def visible_range(text_area: TextArea): Option[Text.Range] =
   175   {
   176     val buffer = text_area.getBuffer
   177     val n = text_area.getVisibleLines
   178     if (n > 0) {
   179       val start = text_area.getScreenLineStartOffset(0)
   180       val raw_end = text_area.getScreenLineEndOffset(n - 1)
   181       val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
   182       Some(Text.Range(start, end))
   183     }
   184     else None
   185   }
   186 
   187   def invalidate_range(text_area: TextArea, range: Text.Range)
   188   {
   189     val buffer = text_area.getBuffer
   190     text_area.invalidateLineRange(
   191       buffer.getLineOfOffset(range.start),
   192       buffer.getLineOfOffset(range.stop))
   193   }
   194 
   195 
   196   /* graphics range */
   197 
   198   case class Gfx_Range(val x: Int, val y: Int, val length: Int)
   199 
   200   // NB: jEdit always normalizes \r\n and \r to \n
   201   // NB: last line lacks \n
   202   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   203   {
   204     val metric = pretty_metric(text_area.getPainter)
   205     val char_width = (metric.unit * metric.average).round.toInt
   206 
   207     val buffer = text_area.getBuffer
   208 
   209     val end = buffer.getLength
   210     val stop = range.stop
   211 
   212     val (p, q, r) =
   213       try {
   214         val p = text_area.offsetToXY(range.start)
   215         val (q, r) =
   216           if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
   217           else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
   218             (text_area.offsetToXY(stop - 1), char_width)
   219           else (text_area.offsetToXY(stop), 0)
   220         (p, q, r)
   221       }
   222       catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
   223 
   224     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
   225       Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
   226     else None
   227   }
   228 
   229 
   230   /* pixel range */
   231 
   232   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
   233   {
   234     // coordinates wrt. inner painter component
   235     val painter = text_area.getPainter
   236     if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
   237       val offset = text_area.xyToOffset(x, y, false)
   238       if (offset >= 0) {
   239         val range = point_range(text_area.getBuffer, offset)
   240         gfx_range(text_area, range) match {
   241           case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
   242           case _ => None
   243         }
   244       }
   245       else None
   246     }
   247     else None
   248   }
   249 
   250 
   251   /* pretty text metric */
   252 
   253   abstract class Pretty_Metric extends Pretty.Metric
   254   {
   255     def average: Double
   256   }
   257 
   258   def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
   259     new Pretty_Metric {
   260       def string_width(s: String): Double =
   261         painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
   262 
   263       val unit = string_width(Pretty.space)
   264       val average = string_width("mix") / (3 * unit)
   265       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
   266     }
   267 
   268 
   269   /* icons */
   270 
   271   def load_icon(name: String): Icon =
   272   {
   273     val name1 =
   274       if (name.startsWith("idea-icons/")) {
   275         val file =
   276           Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
   277         "jar:" + file + "!/" + name
   278       }
   279       else name
   280     val icon = GUIUtilities.loadIcon(name1)
   281     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
   282     else icon
   283   }
   284 
   285   def load_image_icon(name: String): ImageIcon =
   286     load_icon(name) match {
   287       case icon: ImageIcon => icon
   288       case _ => error("Bad image icon: " + name)
   289     }
   290 
   291 
   292   /* key event handling */
   293 
   294   def request_focus_view
   295   {
   296     val view = jEdit.getActiveView()
   297     if (view != null) {
   298       val text_area = view.getTextArea
   299       if (text_area != null) text_area.requestFocus
   300     }
   301   }
   302 
   303   def propagate_key(view: View, evt: KeyEvent)
   304   {
   305     if (view != null && !evt.isConsumed)
   306       view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
   307   }
   308 
   309   def key_listener(
   310     key_typed: KeyEvent => Unit = _ => (),
   311     key_pressed: KeyEvent => Unit = _ => (),
   312     key_released: KeyEvent => Unit = _ => ()): KeyListener =
   313   {
   314     def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
   315     {
   316       val evt = KeyEventWorkaround.processKeyEvent(evt0)
   317       if (evt != null) handle(evt)
   318     }
   319 
   320     new KeyListener
   321     {
   322       def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }
   323       def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }
   324       def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
   325     }
   326   }
   327 }
   328