src/Tools/jEdit/src/jedit_lib.scala

 import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator}
 import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
 
 
-object JEdit_Lib
-{
+object JEdit_Lib {
   /* jEdit directories */
 
   def directories: List[JFile] =
     (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_))
 
 
   /* window geometry measurement */
 
   private lazy val dummy_window = new JWindow
 
-  final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int)
-  {
+  final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int) {
     def deco_width: Int = width - inner_width
     def deco_height: Int = height - inner_height
   }
 
-  def window_geometry(outer: Container, inner: Component): Window_Geometry =
-  {
+  def window_geometry(outer: Container, inner: Component): Window_Geometry = {
     GUI_Thread.require {}
 
     val old_content = dummy_window.getContentPane
 
     dummy_window.setContentPane(outer)

     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 
   def buffer_reader(buffer: JEditBuffer): CharSequenceReader =
     Scan.char_reader(buffer.getSegment(0, buffer.getLength))
 
-  def buffer_mode(buffer: JEditBuffer): String =
-  {
+  def buffer_mode(buffer: JEditBuffer): String = {
     val mode = buffer.getMode
     if (mode == null) ""
     else {
       val name = mode.getName
       if (name == null) "" else name

 
   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
 
   def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer))
 
-  def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A =
-  {
+  def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A = {
     val undo_in_progress = buffer.isUndoInProgress
     def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b)
     try { set(true); body } finally { set(undo_in_progress) }
   }
 

     jedit_views().flatMap(jedit_text_areas)
 
   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
     jedit_text_areas().filter(_.getBuffer == buffer)
 
-  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
-  {
+  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = {
     try { buffer.readLock(); body }
     finally { buffer.readUnlock() }
   }
 
-  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A =
-  {
+  def buffer_edit[A](buffer: JEditBuffer)(body: => A): A = {
     try { buffer.beginCompoundEdit(); body }
     finally { buffer.endCompoundEdit() }
   }
 
 

     Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength)
 
   def caret_range(text_area: TextArea): Text.Range =
     point_range(text_area.getBuffer, text_area.getCaretPosition)
 
-  def visible_range(text_area: TextArea): Option[Text.Range] =
-  {
+  def visible_range(text_area: TextArea): Option[Text.Range] = {
     val buffer = text_area.getBuffer
     val n = text_area.getVisibleLines
     if (n > 0) {
       val start = text_area.getScreenLineStartOffset(0)
       val raw_end = text_area.getScreenLineEndOffset(n - 1)

       Some(Text.Range(start, end))
     }
     else None
   }
 
-  def invalidate_range(text_area: TextArea, range: Text.Range): Unit =
-  {
+  def invalidate_range(text_area: TextArea, range: Text.Range): Unit = {
     val buffer = text_area.getBuffer
     buffer_range(buffer).try_restrict(range) match {
       case Some(range1) if !range1.is_singularity =>
         try {
           text_area.invalidateLineRange(

         catch { case _: ArrayIndexOutOfBoundsException => }
       case _ =>
     }
   }
 
-  def invalidate(text_area: TextArea): Unit =
-  {
+  def invalidate(text_area: TextArea): Unit = {
     val visible_lines = text_area.getVisibleLines
     if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines)
   }
 
 

 
   case class Gfx_Range(x: Int, y: Int, length: Int)
 
   // NB: jEdit always normalizes \r\n and \r to \n
   // NB: last line lacks \n
-  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
-  {
+  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = {
     val metric = pretty_metric(text_area.getPainter)
     val char_width = (metric.unit * metric.average).round.toInt
 
     val buffer = text_area.getBuffer
 

   }
 
 
   /* pixel range */
 
-  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] =
-  {
+  def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] = {
     // coordinates wrt. inner painter component
     val painter = text_area.getPainter
     if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) {
       val offset = text_area.xyToOffset(x, y, false)
       if (offset >= 0) {

   }
 
 
   /* pretty text metric */
 
-  abstract class Pretty_Metric extends Pretty.Metric
-  {
+  abstract class Pretty_Metric extends Pretty.Metric {
     def average: Double
   }
 
   def pretty_metric(painter: TextAreaPainter): Pretty_Metric =
     new Pretty_Metric {

     }
 
 
   /* icons */
 
-  def load_icon(name: String): Icon =
-  {
+  def load_icon(name: String): Icon = {
     val name1 =
       if (name.startsWith("idea-icons/")) {
         val file = Path.explode("$ISABELLE_IDEA_ICONS").file.toURI.toASCIIString
         "jar:" + file + "!/" + name
       }

     }
 
 
   /* key event handling */
 
-  def request_focus_view(alt_view: View = null): Unit =
-  {
+  def request_focus_view(alt_view: View = null): Unit = {
     val view = if (alt_view != null) alt_view else jEdit.getActiveView()
     if (view != null) {
       val text_area = view.getTextArea
       if (text_area != null) text_area.requestFocus()
     }
   }
 
-  def propagate_key(view: View, evt: KeyEvent): Unit =
-  {
+  def propagate_key(view: View, evt: KeyEvent): Unit = {
     if (view != null && !evt.isConsumed)
       view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false)
   }
 
   def key_listener(
     key_typed: KeyEvent => Unit = _ => (),
     key_pressed: KeyEvent => Unit = _ => (),
-    key_released: KeyEvent => Unit = _ => ()): KeyListener =
-  {
-    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit): Unit =
-    {
+    key_released: KeyEvent => Unit = _ => ()
+  ): KeyListener = {
+    def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit): Unit = {
       val evt = KeyEventWorkaround.processKeyEvent(evt0)
       if (evt != null) handle(evt)
     }
 
-    new KeyListener
-    {
+    new KeyListener {
       def keyTyped(evt: KeyEvent): Unit = process_key_event(evt, key_typed)
       def keyPressed(evt: KeyEvent): Unit = process_key_event(evt, key_pressed)
       def keyReleased(evt: KeyEvent): Unit = process_key_event(evt, key_released)
     }
   }
 
-  def special_key(evt: KeyEvent): Boolean =
-  {
+  def special_key(evt: KeyEvent): Boolean = {
     // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java
     val mod = evt.getModifiersEx
     (mod & InputEvent.CTRL_DOWN_MASK) != 0 && (mod & InputEvent.ALT_DOWN_MASK) == 0 ||
     (mod & InputEvent.CTRL_DOWN_MASK) == 0 && (mod & InputEvent.ALT_DOWN_MASK) != 0 &&
       !Debug.ALT_KEY_PRESSED_DISABLED ||