src/Tools/jEdit/src/pretty_text_area.scala

 
 
 class Pretty_Text_Area(
   view: View,
   close_action: () => Unit = () => (),
-  propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
-{
+  propagate_keys: Boolean = false
+) extends JEditEmbeddedTextArea {
   text_area =>
 
   GUI_Thread.require {}
 
   private var current_font_info: Font_Info = Font_Info.main()

   private var current_search_pattern: Option[Regex] = None
   def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
 
   def get_background(): Option[Color] = None
 
-  def refresh(): Unit =
-  {
+  def refresh(): Unit = {
     GUI_Thread.require {}
 
     val font = current_font_info.font
     getPainter.setFont(font)
     getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))

           }
         })
     }
   }
 
-  def resize(font_info: Font_Info): Unit =
-  {
+  def resize(font_info: Font_Info): Unit = {
     GUI_Thread.require {}
 
     current_font_info = font_info
     refresh()
   }
 
   def update(
-    base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body): Unit =
-  {
+    base_snapshot: Document.Snapshot,
+    base_results: Command.Results,
+    body: XML.Body
+  ): Unit = {
     GUI_Thread.require {}
     require(!base_snapshot.is_outdated, "document snapshot outdated")
 
     current_base_snapshot = base_snapshot
     current_base_results = base_results
     current_body = body
     refresh()
   }
 
-  def detach: Unit =
-  {
+  def detach: Unit = {
     GUI_Thread.require {}
     Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
   }
 
   def detach_operation: Option[() => Unit] =

   val search_label: Component = new Label("Search:") {
     tooltip = "Search and highlight output via regular expression"
   }
 
   val search_field: Component =
-    Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
-      {
-        private val input_delay =
-          Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
-            search_action(this)
-          }
-        getDocument.addDocumentListener(new DocumentListener {
-          def changedUpdate(e: DocumentEvent): Unit = input_delay.invoke()
-          def insertUpdate(e: DocumentEvent): Unit = input_delay.invoke()
-          def removeUpdate(e: DocumentEvent): Unit = input_delay.invoke()
-        })
-        setColumns(20)
-        setToolTipText(search_label.tooltip)
-        setFont(GUI.imitate_font(getFont, scale = 1.2))
+    Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") {
+      private val input_delay =
+        Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
+          search_action(this)
+        }
+      getDocument.addDocumentListener(new DocumentListener {
+        def changedUpdate(e: DocumentEvent): Unit = input_delay.invoke()
+        def insertUpdate(e: DocumentEvent): Unit = input_delay.invoke()
+        def removeUpdate(e: DocumentEvent): Unit = input_delay.invoke()
       })
+      setColumns(20)
+      setToolTipText(search_label.tooltip)
+      setFont(GUI.imitate_font(getFont, scale = 1.2))
+    })
 
   private val search_field_foreground = search_field.foreground
 
-  private def search_action(text_field: JTextField): Unit =
-  {
+  private def search_action(text_field: JTextField): Unit = {
     val (pattern, ok) =
       text_field.getText match {
         case null | "" => (None, true)
         case s =>
           val re = Library.make_regex(s)

       override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean): Unit = {}
       override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false
     })
 
   addKeyListener(JEdit_Lib.key_listener(
-    key_pressed = (evt: KeyEvent) =>
-      {
-        val strict_control =
-          JEdit_Lib.command_modifier(evt) && !JEdit_Lib.shift_modifier(evt)
-
-        evt.getKeyCode match {
-          case KeyEvent.VK_C | KeyEvent.VK_INSERT
-          if strict_control && text_area.getSelectionCount != 0 =>
-            Registers.copy(text_area, '$')
-            evt.consume
-
-          case KeyEvent.VK_A
-          if strict_control =>
-            text_area.selectAll
-            evt.consume
-
-          case KeyEvent.VK_ESCAPE =>
-            if (Isabelle.dismissed_popups(view)) evt.consume
-
-          case _ =>
-        }
-        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
-      },
-    key_typed = (evt: KeyEvent) =>
-      {
-        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
+    key_pressed = (evt: KeyEvent) => {
+      val strict_control =
+        JEdit_Lib.command_modifier(evt) && !JEdit_Lib.shift_modifier(evt)
+
+      evt.getKeyCode match {
+        case KeyEvent.VK_C | KeyEvent.VK_INSERT
+        if strict_control && text_area.getSelectionCount != 0 =>
+          Registers.copy(text_area, '$')
+          evt.consume
+
+        case KeyEvent.VK_A
+        if strict_control =>
+          text_area.selectAll
+          evt.consume
+
+        case KeyEvent.VK_ESCAPE =>
+          if (Isabelle.dismissed_popups(view)) evt.consume
+
+        case _ =>
       }
-    )
+      if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
+    },
+    key_typed = (evt: KeyEvent) => {
+      if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
+    })
   )
 
 
   /* init */