src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Tue Aug 13 16:15:31 2013 +0200 (2013-08-13)
changeset 53019 be9e94594b96
parent 53003 39da27fc6101
child 53183 018d71bee930
permissions -rw-r--r--
more general window_geometry;
     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 javax.swing.{Icon, ImageIcon, JWindow}
    14 
    15 import scala.annotation.tailrec
    16 
    17 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities}
    18 import org.gjt.sp.jedit.buffer.JEditBuffer
    19 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
    20 
    21 
    22 object JEdit_Lib
    23 {
    24   /* bounds within multi-screen environment */
    25 
    26   def screen_bounds(screen_point: Point): Rectangle =
    27   {
    28     val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
    29     (for {
    30       device <- ge.getScreenDevices.iterator
    31       config <- device.getConfigurations.iterator
    32       bounds = config.getBounds
    33     } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
    34   }
    35 
    36 
    37   /* window geometry measurement */
    38 
    39   private lazy val dummy_window = new JWindow
    40 
    41   final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
    42   {
    43     def deco_width: Int = width - inner_width
    44     def deco_height: Int = height - inner_height
    45   }
    46 
    47   def window_geometry(outer: Container, inner: Component): Window_Geometry =
    48   {
    49     Swing_Thread.require()
    50 
    51     val old_content = dummy_window.getContentPane
    52 
    53     dummy_window.setContentPane(outer)
    54     dummy_window.pack
    55     dummy_window.revalidate
    56 
    57     val geometry =
    58       Window_Geometry(
    59         dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight)
    60 
    61     dummy_window.setContentPane(old_content)
    62 
    63     geometry
    64   }
    65 
    66 
    67   /* GUI components */
    68 
    69   def get_parent(component: Component): Option[Container] =
    70     component.getParent match {
    71       case null => None
    72       case parent => Some(parent)
    73     }
    74 
    75   def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
    76     private var next_elem = get_parent(component)
    77     def hasNext(): Boolean = next_elem.isDefined
    78     def next(): Container =
    79       next_elem match {
    80         case Some(parent) =>
    81           next_elem = get_parent(parent)
    82           parent
    83         case None => Iterator.empty.next()
    84       }
    85   }
    86 
    87   def parent_window(component: Component): Option[Window] =
    88     ancestors(component).collectFirst({ case x: Window => x })
    89 
    90 
    91   /* basic tooltips, with multi-line support */
    92 
    93   def wrap_tooltip(text: String): String =
    94     if (text == "") null
    95     else "<html><pre>" + HTML.encode(text) + "</pre></html>"
    96 
    97 
    98   /* buffers */
    99 
   100   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   101     Swing_Thread.now { buffer_lock(buffer) { body } }
   102 
   103   def buffer_text(buffer: JEditBuffer): String =
   104     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
   105 
   106   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
   107 
   108 
   109   /* focus of main window */
   110 
   111   def request_focus_view: Unit =
   112   {
   113     jEdit.getActiveView() match {
   114       case null =>
   115       case view =>
   116         view.getTextArea match {
   117           case null =>
   118           case text_area => text_area.requestFocus
   119         }
   120     }
   121   }
   122 
   123 
   124   /* main jEdit components */
   125 
   126   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
   127 
   128   def jedit_buffer(name: String): Option[Buffer] =
   129     jedit_buffers().find(buffer => buffer_name(buffer) == name)
   130 
   131   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
   132 
   133   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
   134     view.getEditPanes().iterator.map(_.getTextArea)
   135 
   136   def jedit_text_areas(): Iterator[JEditTextArea] =
   137     jedit_views().flatMap(jedit_text_areas(_))
   138 
   139   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
   140     jedit_text_areas().filter(_.getBuffer == buffer)
   141 
   142   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   143   {
   144     try { buffer.readLock(); body }
   145     finally { buffer.readUnlock() }
   146   }
   147 
   148   def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
   149   {
   150     try { buffer.beginCompoundEdit(); body }
   151     finally { buffer.endCompoundEdit() }
   152   }
   153 
   154 
   155   /* get text */
   156 
   157   def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
   158     try { Some(buffer.getText(range.start, range.length)) }
   159     catch { case _: ArrayIndexOutOfBoundsException => None }
   160 
   161 
   162   /* buffer range */
   163 
   164   def buffer_range(buffer: JEditBuffer): Text.Range =
   165     Text.Range(0, (buffer.getLength - 1) max 0)
   166 
   167 
   168   /* point range */
   169 
   170   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
   171     buffer_lock(buffer) {
   172       def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
   173       try {
   174         val c = text(offset)
   175         if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
   176           Text.Range(offset, offset + 2)
   177         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
   178           Text.Range(offset - 1, offset + 1)
   179         else Text.Range(offset, offset + 1)
   180       }
   181       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
   182     }
   183 
   184 
   185   /* visible text range */
   186 
   187   def visible_range(text_area: TextArea): Option[Text.Range] =
   188   {
   189     val buffer = text_area.getBuffer
   190     val n = text_area.getVisibleLines
   191     if (n > 0) {
   192       val start = text_area.getScreenLineStartOffset(0)
   193       val raw_end = text_area.getScreenLineEndOffset(n - 1)
   194       val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
   195       Some(Text.Range(start, end))
   196     }
   197     else None
   198   }
   199 
   200   def invalidate_range(text_area: TextArea, range: Text.Range)
   201   {
   202     val buffer = text_area.getBuffer
   203     text_area.invalidateLineRange(
   204       buffer.getLineOfOffset(range.start),
   205       buffer.getLineOfOffset(range.stop))
   206   }
   207 
   208 
   209   /* graphics range */
   210 
   211   case class Gfx_Range(val x: Int, val y: Int, val length: Int)
   212 
   213   // NB: jEdit always normalizes \r\n and \r to \n
   214   // NB: last line lacks \n
   215   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   216   {
   217     val metric = pretty_metric(text_area.getPainter)
   218     val char_width = (metric.unit * metric.average).round.toInt
   219 
   220     val buffer = text_area.getBuffer
   221 
   222     val end = buffer.getLength
   223     val stop = range.stop
   224 
   225     val (p, q, r) =
   226       try {
   227         val p = text_area.offsetToXY(range.start)
   228         val (q, r) =
   229           if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
   230           else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
   231             (text_area.offsetToXY(stop - 1), char_width)
   232           else (text_area.offsetToXY(stop), 0)
   233         (p, q, r)
   234       }
   235       catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
   236 
   237     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
   238       Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
   239     else None
   240   }
   241 
   242 
   243   /* pixel range */
   244 
   245   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
   246   {
   247     val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y, false))
   248     gfx_range(text_area, range) match {
   249       case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
   250       case _ => None
   251     }
   252   }
   253 
   254 
   255   /* pretty text metric */
   256 
   257   abstract class Pretty_Metric extends Pretty.Metric
   258   {
   259     def average: Double
   260   }
   261 
   262   def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
   263     new Pretty_Metric {
   264       def string_width(s: String): Double =
   265         painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
   266 
   267       val unit = string_width(Pretty.space)
   268       val average = string_width("mix") / (3 * unit)
   269       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
   270     }
   271 
   272 
   273   /* icons */
   274 
   275   def load_icon(name: String): Icon =
   276   {
   277     val name1 =
   278       if (name.startsWith("idea-icons/")) {
   279         val file =
   280           Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
   281         "jar:" + file + "!/" + name
   282       }
   283       else name
   284     val icon = GUIUtilities.loadIcon(name1)
   285     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
   286     else icon
   287   }
   288 
   289   def load_image_icon(name: String): ImageIcon =
   290     load_icon(name) match {
   291       case icon: ImageIcon => icon
   292       case _ => error("Bad image icon: " + name)
   293     }
   294 }
   295