src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Tue Apr 15 13:07:59 2014 +0200 (2014-04-15)
changeset 56589 71c5d1f516c0
parent 56587 83777a91f5de
child 56592 5157f7615e99
permissions -rw-r--r--
more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
     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, GraphicsEnvironment, Point, Rectangle, Dimension}
    13 import java.awt.event.{InputEvent, KeyEvent, KeyListener}
    14 import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
    15 
    16 import scala.annotation.tailrec
    17 
    18 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
    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   /* location within multi-screen environment */
    27 
    28   final case class Screen_Location(point: Point, bounds: Rectangle)
    29   {
    30     def relative(parent: Component, size: Dimension): Point =
    31     {
    32       val w = size.width
    33       val h = size.height
    34 
    35       val x0 = parent.getLocationOnScreen.x
    36       val y0 = parent.getLocationOnScreen.y
    37       val x1 = x0 + parent.getWidth - w
    38       val y1 = y0 + parent.getHeight - h
    39       val x2 = point.x min (bounds.x + bounds.width - w)
    40       val y2 = point.y min (bounds.y + bounds.height - h)
    41 
    42       val location = new Point((x2 min x1) max x0, (y2 min y1) max y0)
    43       SwingUtilities.convertPointFromScreen(location, parent)
    44       location
    45     }
    46   }
    47 
    48   def screen_location(component: Component, point: Point): Screen_Location =
    49   {
    50     val screen_point = new Point(point.x, point.y)
    51     SwingUtilities.convertPointToScreen(screen_point, component)
    52 
    53     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
    54     val screen_bounds =
    55       (for {
    56         device <- ge.getScreenDevices.iterator
    57         config <- device.getConfigurations.iterator
    58         bounds = config.getBounds
    59       } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
    60 
    61     Screen_Location(screen_point, screen_bounds)
    62   }
    63 
    64 
    65   /* window geometry measurement */
    66 
    67   private lazy val dummy_window = new JWindow
    68 
    69   final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
    70   {
    71     def deco_width: Int = width - inner_width
    72     def deco_height: Int = height - inner_height
    73   }
    74 
    75   def window_geometry(outer: Container, inner: Component): Window_Geometry =
    76   {
    77     Swing_Thread.require()
    78 
    79     val old_content = dummy_window.getContentPane
    80 
    81     dummy_window.setContentPane(outer)
    82     dummy_window.pack
    83     dummy_window.revalidate
    84 
    85     val geometry =
    86       Window_Geometry(
    87         dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
    88 
    89     dummy_window.setContentPane(old_content)
    90 
    91     geometry
    92   }
    93 
    94 
    95   /* buffers */
    96 
    97   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    98     Swing_Thread.now { buffer_lock(buffer) { body } }
    99 
   100   def buffer_text(buffer: JEditBuffer): String =
   101     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
   102 
   103   def buffer_mode(buffer: JEditBuffer): String =
   104   {
   105     val mode = buffer.getMode
   106     if (mode == null) ""
   107     else {
   108       val name = mode.getName
   109       if (name == null) "" else name
   110     }
   111   }
   112 
   113   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
   114 
   115 
   116   /* main jEdit components */
   117 
   118   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
   119 
   120   def jedit_buffer(name: String): Option[Buffer] =
   121     jedit_buffers().find(buffer => buffer_name(buffer) == name)
   122 
   123   def jedit_buffer(name: Document.Node.Name): Option[Buffer] =
   124     jedit_buffer(name.node)
   125 
   126   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
   127 
   128   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
   129     if (view == null) Iterator.empty
   130     else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
   131 
   132   def jedit_text_areas(): Iterator[JEditTextArea] =
   133     jedit_views().flatMap(jedit_text_areas(_))
   134 
   135   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
   136     jedit_text_areas().filter(_.getBuffer == buffer)
   137 
   138   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   139   {
   140     try { buffer.readLock(); body }
   141     finally { buffer.readUnlock() }
   142   }
   143 
   144   def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
   145   {
   146     try { buffer.beginCompoundEdit(); body }
   147     finally { buffer.endCompoundEdit() }
   148   }
   149 
   150 
   151   /* get text */
   152 
   153   def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
   154     try { Some(buffer.getText(range.start, range.length)) }
   155     catch { case _: ArrayIndexOutOfBoundsException => None }
   156 
   157   def try_get_text(text: String, range: Text.Range): Option[String] =
   158     try { Some(text.substring(range.start, range.stop)) }
   159     catch { case _: IndexOutOfBoundsException => None }
   160 
   161 
   162   /* point range */
   163 
   164   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
   165     buffer_lock(buffer) {
   166       def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
   167       try {
   168         val c = text(offset)
   169         if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
   170           Text.Range(offset, offset + 2)
   171         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
   172           Text.Range(offset - 1, offset + 1)
   173         else
   174           Text.Range(offset, offset + 1)
   175       }
   176       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
   177     }
   178 
   179 
   180   /* text ranges */
   181 
   182   def buffer_range(buffer: JEditBuffer): Text.Range =
   183     Text.Range(0, buffer.getLength)
   184 
   185   def line_range(buffer: JEditBuffer, line: Int): Text.Range =
   186     Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
   187 
   188   def before_caret_range(text_area: TextArea, rendering: Rendering): Option[Text.Range] =
   189   {
   190     val range = line_range(text_area.getBuffer, text_area.getCaretLine)
   191     val snapshot = rendering.snapshot
   192     val former_caret = snapshot.revert(text_area.getCaretPosition)
   193     snapshot.convert(Text.Range(former_caret - 1, former_caret)).try_restrict(range)
   194   }
   195 
   196   def visible_range(text_area: TextArea): Option[Text.Range] =
   197   {
   198     val buffer = text_area.getBuffer
   199     val n = text_area.getVisibleLines
   200     if (n > 0) {
   201       val start = text_area.getScreenLineStartOffset(0)
   202       val raw_end = text_area.getScreenLineEndOffset(n - 1)
   203       val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
   204       Some(Text.Range(start, end))
   205     }
   206     else None
   207   }
   208 
   209   def invalidate_range(text_area: TextArea, range: Text.Range)
   210   {
   211     val buffer = text_area.getBuffer
   212     buffer_range(buffer).try_restrict(range) match {
   213       case Some(range1) if !range1.is_singularity =>
   214         text_area.invalidateLineRange(
   215           buffer.getLineOfOffset(range1.start),
   216           buffer.getLineOfOffset(range1.stop))
   217       case _ =>
   218     }
   219   }
   220 
   221 
   222   /* graphics range */
   223 
   224   case class Gfx_Range(val x: Int, val y: Int, val length: Int)
   225 
   226   // NB: jEdit always normalizes \r\n and \r to \n
   227   // NB: last line lacks \n
   228   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   229   {
   230     val metric = pretty_metric(text_area.getPainter)
   231     val char_width = (metric.unit * metric.average).round.toInt
   232 
   233     val buffer = text_area.getBuffer
   234 
   235     val end = buffer.getLength
   236     val stop = range.stop
   237 
   238     val (p, q, r) =
   239       try {
   240         val p = text_area.offsetToXY(range.start)
   241         val (q, r) =
   242           if (try_get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n"))
   243             (text_area.offsetToXY(stop - 1), char_width)
   244           else if (stop >= end)
   245             (text_area.offsetToXY(end), char_width * (stop - end))
   246           else (text_area.offsetToXY(stop), 0)
   247         (p, q, r)
   248       }
   249       catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
   250 
   251     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
   252       Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
   253     else None
   254   }
   255 
   256 
   257   /* pixel range */
   258 
   259   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
   260   {
   261     // coordinates wrt. inner painter component
   262     val painter = text_area.getPainter
   263     if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
   264       val offset = text_area.xyToOffset(x, y, false)
   265       if (offset >= 0) {
   266         val range = point_range(text_area.getBuffer, offset)
   267         gfx_range(text_area, range) match {
   268           case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
   269           case _ => None
   270         }
   271       }
   272       else None
   273     }
   274     else None
   275   }
   276 
   277 
   278   /* pretty text metric */
   279 
   280   abstract class Pretty_Metric extends Pretty.Metric
   281   {
   282     def average: Double
   283   }
   284 
   285   def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
   286     new Pretty_Metric {
   287       def string_width(s: String): Double =
   288         painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
   289 
   290       val unit = string_width(Pretty.space)
   291       val average = string_width("mix") / (3 * unit)
   292       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
   293     }
   294 
   295 
   296   /* icons */
   297 
   298   def load_icon(name: String): Icon =
   299   {
   300     val name1 =
   301       if (name.startsWith("idea-icons/")) {
   302         val file =
   303           Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
   304         "jar:" + file + "!/" + name
   305       }
   306       else name
   307     val icon = GUIUtilities.loadIcon(name1)
   308     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
   309     else icon
   310   }
   311 
   312   def load_image_icon(name: String): ImageIcon =
   313     load_icon(name) match {
   314       case icon: ImageIcon => icon
   315       case _ => error("Bad image icon: " + name)
   316     }
   317 
   318 
   319   /* key event handling */
   320 
   321   def request_focus_view
   322   {
   323     val view = jEdit.getActiveView()
   324     if (view != null) {
   325       val text_area = view.getTextArea
   326       if (text_area != null) text_area.requestFocus
   327     }
   328   }
   329 
   330   def propagate_key(view: View, evt: KeyEvent)
   331   {
   332     if (view != null && !evt.isConsumed)
   333       view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
   334   }
   335 
   336   def key_listener(
   337     key_typed: KeyEvent => Unit = _ => (),
   338     key_pressed: KeyEvent => Unit = _ => (),
   339     key_released: KeyEvent => Unit = _ => ()): KeyListener =
   340   {
   341     def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit)
   342     {
   343       val evt = KeyEventWorkaround.processKeyEvent(evt0)
   344       if (evt != null) handle(evt)
   345     }
   346 
   347     new KeyListener
   348     {
   349       def keyTyped(evt: KeyEvent) { process_key_event(evt, key_typed) }
   350       def keyPressed(evt: KeyEvent) { process_key_event(evt, key_pressed) }
   351       def keyReleased(evt: KeyEvent) { process_key_event(evt, key_released) }
   352     }
   353   }
   354 
   355   def special_key(evt: KeyEvent): Boolean =
   356   {
   357     // cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
   358     val mod = evt.getModifiers
   359     (mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 ||
   360     (mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 &&
   361       !Debug.ALT_KEY_PRESSED_DISABLED ||
   362     (mod & InputEvent.META_MASK) != 0
   363   }
   364 }
   365