src/Tools/jEdit/src/pretty_text_area.scala
author wenzelm
Sun May 19 18:10:45 2019 +0200 (5 months ago)
changeset 70284 3e17c3a5fd39
parent 69358 71ef6e6da3dc
permissions -rw-r--r--
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
wenzelm@49398
     1
/*  Title:      Tools/jEdit/src/pretty_text_area.scala
wenzelm@49398
     2
    Author:     Makarius
wenzelm@49398
     3
wenzelm@50160
     4
GUI component for pretty-printed text with markup, rendered like jEdit
wenzelm@50160
     5
text area.
wenzelm@49398
     6
*/
wenzelm@49398
     7
wenzelm@49398
     8
package isabelle.jedit
wenzelm@49398
     9
wenzelm@49398
    10
wenzelm@49398
    11
import isabelle._
wenzelm@49398
    12
wenzelm@58766
    13
import java.awt.{Color, Font, Toolkit, Window}
wenzelm@53226
    14
import java.awt.event.KeyEvent
wenzelm@62214
    15
import java.awt.im.InputMethodRequests
wenzelm@56883
    16
import javax.swing.JTextField
wenzelm@56885
    17
import javax.swing.event.{DocumentListener, DocumentEvent}
wenzelm@56883
    18
wenzelm@56907
    19
import scala.swing.{Label, Component}
wenzelm@56883
    20
import scala.util.matching.Regex
wenzelm@56881
    21
wenzelm@61570
    22
import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
wenzelm@61570
    23
import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler}
wenzelm@49398
    24
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
wenzelm@50542
    25
import org.gjt.sp.jedit.syntax.SyntaxStyle
wenzelm@61570
    26
import org.gjt.sp.jedit.gui.KeyEventTranslator
wenzelm@50640
    27
import org.gjt.sp.util.{SyntaxUtilities, Log}
wenzelm@49412
    28
wenzelm@49398
    29
wenzelm@49412
    30
object Pretty_Text_Area
wenzelm@49412
    31
{
wenzelm@56883
    32
  /* auxiliary */
wenzelm@56883
    33
wenzelm@50501
    34
  private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
wenzelm@50501
    35
    formatted_body: XML.Body): (String, Document.State) =
wenzelm@49412
    36
  {
wenzelm@52530
    37
    val command = Command.rich_text(Document_ID.make(), base_results, formatted_body)
wenzelm@49412
    38
    val node_name = command.node_name
wenzelm@49412
    39
    val edits: List[Document.Edit_Text] =
wenzelm@49414
    40
      List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
wenzelm@49412
    41
wenzelm@49419
    42
    val state0 = base_snapshot.state.define_command(command)
wenzelm@49419
    43
    val version0 = base_snapshot.version
wenzelm@49412
    44
    val nodes0 = version0.nodes
wenzelm@49412
    45
wenzelm@49412
    46
    val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
wenzelm@59077
    47
    val version1 = Document.Version.make(nodes1)
wenzelm@49412
    48
    val state1 =
wenzelm@56711
    49
      state0.continue_history(Future.value(version0), edits, Future.value(version1))
wenzelm@49412
    50
        .define_version(version1, state0.the_assignment(version0))
wenzelm@70284
    51
        .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
wenzelm@49412
    52
wenzelm@49416
    53
    (command.source, state1)
wenzelm@49412
    54
  }
wenzelm@51495
    55
wenzelm@51495
    56
  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
wenzelm@64621
    57
    formatted_body: XML.Body): (String, JEdit_Rendering) =
wenzelm@51495
    58
  {
wenzelm@51495
    59
    val (text, state) = document_state(base_snapshot, base_results, formatted_body)
wenzelm@66114
    60
    val model = File_Model.empty(PIDE.session)
wenzelm@66114
    61
    val rendering = JEdit_Rendering(state.snapshot(), model, PIDE.options.value)
wenzelm@51495
    62
    (text, rendering)
wenzelm@51495
    63
  }
wenzelm@49412
    64
}
wenzelm@49412
    65
wenzelm@50538
    66
class Pretty_Text_Area(
wenzelm@50538
    67
  view: View,
wenzelm@50915
    68
  close_action: () => Unit = () => (),
wenzelm@50743
    69
  propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
wenzelm@49398
    70
{
wenzelm@49446
    71
  text_area =>
wenzelm@49446
    72
wenzelm@57612
    73
  GUI_Thread.require {}
wenzelm@49398
    74
wenzelm@55826
    75
  private var current_font_info: Font_Info = Font_Info.main()
wenzelm@49398
    76
  private var current_body: XML.Body = Nil
wenzelm@52972
    77
  private var current_base_snapshot = Document.Snapshot.init
wenzelm@50507
    78
  private var current_base_results = Command.Results.empty
wenzelm@64621
    79
  private var current_rendering: JEdit_Rendering =
wenzelm@50501
    80
    Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
wenzelm@61561
    81
  private var future_refresh: Option[Future[Unit]] = None
wenzelm@49398
    82
wenzelm@50306
    83
  private val rich_text_area =
wenzelm@50915
    84
    new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
wenzelm@63028
    85
      get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
wenzelm@56883
    86
wenzelm@56883
    87
  private var current_search_pattern: Option[Regex] = None
wenzelm@57612
    88
  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
wenzelm@49416
    89
wenzelm@51451
    90
  def get_background(): Option[Color] = None
wenzelm@51451
    91
wenzelm@49398
    92
  def refresh()
wenzelm@49398
    93
  {
wenzelm@57612
    94
    GUI_Thread.require {}
wenzelm@49398
    95
wenzelm@55825
    96
    val font = current_font_info.font
wenzelm@50168
    97
    getPainter.setFont(font)
wenzelm@50168
    98
    getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
wenzelm@51497
    99
    getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
wenzelm@55825
   100
    getPainter.setStyles(
wenzelm@55825
   101
      SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
wenzelm@56789
   102
    getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))
wenzelm@50168
   103
wenzelm@50542
   104
    val fold_line_style = new Array[SyntaxStyle](4)
wenzelm@50542
   105
    for (i <- 0 to 3) {
wenzelm@50542
   106
      fold_line_style(i) =
wenzelm@50542
   107
        SyntaxUtilities.parseStyle(
wenzelm@50542
   108
          jEdit.getProperty("view.style.foldLine." + i),
wenzelm@55825
   109
          current_font_info.family, current_font_info.size.round, true)
wenzelm@50542
   110
    }
wenzelm@50542
   111
    getPainter.setFoldLineStyle(fold_line_style)
wenzelm@50542
   112
wenzelm@51439
   113
    getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
wenzelm@51439
   114
    getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
wenzelm@51451
   115
    get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
wenzelm@51439
   116
    getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
wenzelm@51439
   117
    getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
wenzelm@51439
   118
    getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
wenzelm@51439
   119
    getGutter.setBorder(0,
wenzelm@51439
   120
      jEdit.getColorProperty("view.gutter.focusBorderColor"),
wenzelm@51439
   121
      jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
wenzelm@51439
   122
      getPainter.getBackground)
wenzelm@60250
   123
    getGutter.setFoldPainter(view.getTextArea.getFoldPainter)
wenzelm@51439
   124
    getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
wenzelm@51439
   125
wenzelm@50166
   126
    if (getWidth > 0) {
wenzelm@51492
   127
      val metric = JEdit_Lib.pretty_metric(getPainter)
wenzelm@51493
   128
      val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0
wenzelm@49471
   129
wenzelm@50166
   130
      val base_snapshot = current_base_snapshot
wenzelm@50501
   131
      val base_results = current_base_results
wenzelm@67547
   132
      val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
wenzelm@49398
   133
wenzelm@61561
   134
      future_refresh.map(_.cancel)
wenzelm@61193
   135
      future_refresh =
wenzelm@61561
   136
        Some(Future.fork {
wenzelm@51498
   137
          val (text, rendering) =
wenzelm@51498
   138
            try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
wenzelm@51498
   139
            catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
wenzelm@56860
   140
          Exn.Interrupt.expose()
wenzelm@49398
   141
wenzelm@57612
   142
          GUI_Thread.later {
wenzelm@51498
   143
            current_rendering = rendering
wenzelm@51498
   144
            JEdit_Lib.buffer_edit(getBuffer) {
wenzelm@51498
   145
              rich_text_area.active_reset()
wenzelm@51498
   146
              getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
wenzelm@68060
   147
              JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(text))
wenzelm@51498
   148
              setCaretPosition(0)
wenzelm@51498
   149
            }
wenzelm@51498
   150
          }
wenzelm@56730
   151
        })
wenzelm@50166
   152
    }
wenzelm@49398
   153
  }
wenzelm@49398
   154
wenzelm@55825
   155
  def resize(font_info: Font_Info)
wenzelm@49398
   156
  {
wenzelm@57612
   157
    GUI_Thread.require {}
wenzelm@49398
   158
wenzelm@55825
   159
    current_font_info = font_info
wenzelm@49398
   160
    refresh()
wenzelm@49398
   161
  }
wenzelm@49398
   162
wenzelm@50501
   163
  def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
wenzelm@49398
   164
  {
wenzelm@57612
   165
    GUI_Thread.require {}
wenzelm@49419
   166
    require(!base_snapshot.is_outdated)
wenzelm@49398
   167
wenzelm@49419
   168
    current_base_snapshot = base_snapshot
wenzelm@50501
   169
    current_base_results = base_results
wenzelm@49398
   170
    current_body = body
wenzelm@49398
   171
    refresh()
wenzelm@49398
   172
  }
wenzelm@49398
   173
wenzelm@56880
   174
  def detach
wenzelm@56880
   175
  {
wenzelm@57612
   176
    GUI_Thread.require {}
wenzelm@56880
   177
    Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
wenzelm@56880
   178
  }
wenzelm@56880
   179
wenzelm@56918
   180
  def detach_operation: Option[() => Unit] =
wenzelm@56918
   181
    if (current_body.isEmpty) None else Some(() => detach)
wenzelm@56918
   182
wenzelm@49422
   183
wenzelm@56881
   184
  /* common GUI components */
wenzelm@56881
   185
wenzelm@56883
   186
  val search_label: Component = new Label("Search:") {
wenzelm@56883
   187
    tooltip = "Search and highlight output via regular expression"
wenzelm@56883
   188
  }
wenzelm@56883
   189
wenzelm@57042
   190
  val search_field: Component =
wenzelm@56883
   191
    Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
wenzelm@56883
   192
      {
wenzelm@56883
   193
        private val input_delay =
wenzelm@57612
   194
          GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
wenzelm@56883
   195
            search_action(this)
wenzelm@56883
   196
          }
wenzelm@56885
   197
        getDocument.addDocumentListener(new DocumentListener {
wenzelm@56885
   198
          def changedUpdate(e: DocumentEvent) { input_delay.invoke() }
wenzelm@56885
   199
          def insertUpdate(e: DocumentEvent) { input_delay.invoke() }
wenzelm@56885
   200
          def removeUpdate(e: DocumentEvent) { input_delay.invoke() }
wenzelm@56885
   201
        })
wenzelm@56883
   202
        setColumns(20)
wenzelm@56883
   203
        setToolTipText(search_label.tooltip)
wenzelm@69358
   204
        setFont(GUI.imitate_font(getFont, scale = 1.2))
wenzelm@56883
   205
      })
wenzelm@56883
   206
wenzelm@57042
   207
  private val search_field_foreground = search_field.foreground
wenzelm@56883
   208
wenzelm@56883
   209
  private def search_action(text_field: JTextField)
wenzelm@56883
   210
  {
wenzelm@56883
   211
    val (pattern, ok) =
wenzelm@56883
   212
      text_field.getText match {
wenzelm@56883
   213
        case null | "" => (None, true)
wenzelm@56883
   214
        case s =>
wenzelm@59224
   215
          val re = Library.make_regex(s)
wenzelm@59224
   216
          (re, re.isDefined)
wenzelm@56883
   217
      }
wenzelm@56883
   218
    if (current_search_pattern != pattern) {
wenzelm@56883
   219
      current_search_pattern = pattern
wenzelm@56883
   220
      text_area.getPainter.repaint()
wenzelm@56883
   221
    }
wenzelm@56883
   222
    text_field.setForeground(
wenzelm@65911
   223
      if (ok) search_field_foreground
wenzelm@65911
   224
      else current_rendering.color(Rendering.Color.error))
wenzelm@56883
   225
  }
wenzelm@56883
   226
wenzelm@56881
   227
wenzelm@50726
   228
  /* key handling */
wenzelm@49422
   229
wenzelm@62214
   230
  override def getInputMethodRequests: InputMethodRequests = null
wenzelm@62214
   231
wenzelm@61570
   232
  inputHandlerProvider =
wenzelm@61570
   233
    new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) {
wenzelm@61570
   234
      override def getAction(action: String): JEditBeanShellAction =
wenzelm@61570
   235
        text_area.getActionContext.getAction(action)
wenzelm@61570
   236
      override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean) {}
wenzelm@61570
   237
      override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false
wenzelm@61570
   238
    })
wenzelm@61570
   239
wenzelm@53226
   240
  addKeyListener(JEdit_Lib.key_listener(
wenzelm@53226
   241
    key_pressed = (evt: KeyEvent) =>
wenzelm@53226
   242
      {
wenzelm@53226
   243
        evt.getKeyCode match {
wenzelm@58835
   244
          case KeyEvent.VK_C | KeyEvent.VK_INSERT
wenzelm@56323
   245
          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
wenzelm@56323
   246
              text_area.getSelectionCount != 0 =>
wenzelm@53226
   247
            Registers.copy(text_area, '$')
wenzelm@53226
   248
            evt.consume
wenzelm@53227
   249
wenzelm@53226
   250
          case KeyEvent.VK_A
wenzelm@53226
   251
          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
wenzelm@53226
   252
            text_area.selectAll
wenzelm@53226
   253
            evt.consume
wenzelm@53227
   254
wenzelm@53227
   255
          case KeyEvent.VK_ESCAPE =>
wenzelm@65240
   256
            if (Isabelle.dismissed_popups(view)) evt.consume
wenzelm@53227
   257
wenzelm@53226
   258
          case _ =>
wenzelm@53226
   259
        }
wenzelm@53231
   260
        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
wenzelm@53226
   261
      },
wenzelm@53226
   262
    key_typed = (evt: KeyEvent) =>
wenzelm@53226
   263
      {
wenzelm@53231
   264
        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
wenzelm@49422
   265
      }
wenzelm@53226
   266
    )
wenzelm@53226
   267
  )
wenzelm@49422
   268
wenzelm@49422
   269
wenzelm@49422
   270
  /* init */
wenzelm@49422
   271
wenzelm@49472
   272
  getPainter.setStructureHighlightEnabled(false)
wenzelm@49475
   273
  getPainter.setLineHighlightEnabled(false)
wenzelm@49475
   274
wenzelm@59076
   275
  getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
wenzelm@63261
   276
  getBuffer.setStringProperty("noWordSep", "_'?⇩")
wenzelm@49475
   277
wenzelm@49412
   278
  rich_text_area.activate()
wenzelm@49398
   279
}