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