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