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