src/Tools/jEdit/src/jedit_lib.scala
author wenzelm
Mon Aug 05 23:57:29 2013 +0200 (2013-08-05)
changeset 52874 91032244e4ca
parent 52873 9e934d4fff00
child 53003 39da27fc6101
permissions -rw-r--r--
query process animation;
     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}
    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   /* GUI components */
    38 
    39   def get_parent(component: Component): Option[Container] =
    40     component.getParent match {
    41       case null => None
    42       case parent => Some(parent)
    43     }
    44 
    45   def ancestors(component: Component): Iterator[Container] = new Iterator[Container] {
    46     private var next_elem = get_parent(component)
    47     def hasNext(): Boolean = next_elem.isDefined
    48     def next(): Container =
    49       next_elem match {
    50         case Some(parent) =>
    51           next_elem = get_parent(parent)
    52           parent
    53         case None => Iterator.empty.next()
    54       }
    55   }
    56 
    57   def parent_window(component: Component): Option[Window] =
    58     ancestors(component).collectFirst({ case x: Window => x })
    59 
    60 
    61   /* basic tooltips, with multi-line support */
    62 
    63   def wrap_tooltip(text: String): String =
    64     if (text == "") null
    65     else "<html><pre>" + HTML.encode(text) + "</pre></html>"
    66 
    67 
    68   /* buffers */
    69 
    70   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    71     Swing_Thread.now { buffer_lock(buffer) { body } }
    72 
    73   def buffer_text(buffer: JEditBuffer): String =
    74     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    75 
    76   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
    77 
    78 
    79   /* main jEdit components */
    80 
    81   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
    82 
    83   def jedit_buffer(name: String): Option[Buffer] =
    84     jedit_buffers().find(buffer => buffer_name(buffer) == name)
    85 
    86   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
    87 
    88   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
    89     view.getEditPanes().iterator.map(_.getTextArea)
    90 
    91   def jedit_text_areas(): Iterator[JEditTextArea] =
    92     jedit_views().flatMap(jedit_text_areas(_))
    93 
    94   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
    95     jedit_text_areas().filter(_.getBuffer == buffer)
    96 
    97   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
    98   {
    99     try { buffer.readLock(); body }
   100     finally { buffer.readUnlock() }
   101   }
   102 
   103   def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
   104   {
   105     try { buffer.beginCompoundEdit(); body }
   106     finally { buffer.endCompoundEdit() }
   107   }
   108 
   109 
   110   /* get text */
   111 
   112   def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
   113     try { Some(buffer.getText(range.start, range.length)) }
   114     catch { case _: ArrayIndexOutOfBoundsException => None }
   115 
   116 
   117   /* buffer range */
   118 
   119   def buffer_range(buffer: JEditBuffer): Text.Range =
   120     Text.Range(0, (buffer.getLength - 1) max 0)
   121 
   122 
   123   /* point range */
   124 
   125   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
   126     buffer_lock(buffer) {
   127       def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
   128       try {
   129         val c = text(offset)
   130         if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
   131           Text.Range(offset, offset + 2)
   132         else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
   133           Text.Range(offset - 1, offset + 1)
   134         else Text.Range(offset, offset + 1)
   135       }
   136       catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
   137     }
   138 
   139 
   140   /* visible text range */
   141 
   142   def visible_range(text_area: TextArea): Option[Text.Range] =
   143   {
   144     val buffer = text_area.getBuffer
   145     val n = text_area.getVisibleLines
   146     if (n > 0) {
   147       val start = text_area.getScreenLineStartOffset(0)
   148       val raw_end = text_area.getScreenLineEndOffset(n - 1)
   149       val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength
   150       Some(Text.Range(start, end))
   151     }
   152     else None
   153   }
   154 
   155   def invalidate_range(text_area: TextArea, range: Text.Range)
   156   {
   157     val buffer = text_area.getBuffer
   158     text_area.invalidateLineRange(
   159       buffer.getLineOfOffset(range.start),
   160       buffer.getLineOfOffset(range.stop))
   161   }
   162 
   163 
   164   /* graphics range */
   165 
   166   case class Gfx_Range(val x: Int, val y: Int, val length: Int)
   167 
   168   // NB: jEdit always normalizes \r\n and \r to \n
   169   // NB: last line lacks \n
   170   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   171   {
   172     val metric = pretty_metric(text_area.getPainter)
   173     val char_width = (metric.unit * metric.average).round.toInt
   174 
   175     val buffer = text_area.getBuffer
   176 
   177     val end = buffer.getLength
   178     val stop = range.stop
   179 
   180     val (p, q, r) =
   181       try {
   182         val p = text_area.offsetToXY(range.start)
   183         val (q, r) =
   184           if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end))
   185           else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
   186             (text_area.offsetToXY(stop - 1), char_width)
   187           else (text_area.offsetToXY(stop), 0)
   188         (p, q, r)
   189       }
   190       catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) }
   191 
   192     if (p != null && q != null && p.x < q.x + r && p.y == q.y)
   193       Some(Gfx_Range(p.x, p.y, q.x + r - p.x))
   194     else None
   195   }
   196 
   197 
   198   /* pixel range */
   199 
   200   def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
   201   {
   202     val range = point_range(text_area.getBuffer, text_area.xyToOffset(x, y, false))
   203     gfx_range(text_area, range) match {
   204       case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
   205       case _ => None
   206     }
   207   }
   208 
   209 
   210   /* pretty text metric */
   211 
   212   abstract class Pretty_Metric extends Pretty.Metric
   213   {
   214     def average: Double
   215   }
   216 
   217   def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
   218     new Pretty_Metric {
   219       def string_width(s: String): Double =
   220         painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
   221 
   222       val unit = string_width(Pretty.space)
   223       val average = string_width("mix") / (3 * unit)
   224       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
   225     }
   226 
   227 
   228   /* icons */
   229 
   230   def load_icon(name: String): Icon =
   231   {
   232     val name1 =
   233       if (name.startsWith("idea-icons/")) {
   234         val file =
   235           Isabelle_System.platform_file_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
   236         "jar:" + file + "!/" + name
   237       }
   238       else name
   239     val icon = GUIUtilities.loadIcon(name1)
   240     if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name)
   241     else icon
   242   }
   243 
   244   def load_image_icon(name: String): ImageIcon =
   245     load_icon(name) match {
   246       case icon: ImageIcon => icon
   247       case _ => error("Bad image icon: " + name)
   248     }
   249 }
   250