src/Tools/jEdit/src/pretty_text_area.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 65240 fe5a96240749
permissions -rw-r--r--
tuned signature;
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@52530
    51
        .assign(version1.id, 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@64621
    60
    val rendering = JEdit_Rendering(state.snapshot(), PIDE.options.value)
wenzelm@51495
    61
    (text, rendering)
wenzelm@51495
    62
  }
wenzelm@49412
    63
}
wenzelm@49412
    64
wenzelm@50538
    65
class Pretty_Text_Area(
wenzelm@50538
    66
  view: View,
wenzelm@50915
    67
  close_action: () => Unit = () => (),
wenzelm@50743
    68
  propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
wenzelm@49398
    69
{
wenzelm@49446
    70
  text_area =>
wenzelm@49446
    71
wenzelm@57612
    72
  GUI_Thread.require {}
wenzelm@49398
    73
wenzelm@55826
    74
  private var current_font_info: Font_Info = Font_Info.main()
wenzelm@49398
    75
  private var current_body: XML.Body = Nil
wenzelm@52972
    76
  private var current_base_snapshot = Document.Snapshot.init
wenzelm@50507
    77
  private var current_base_results = Command.Results.empty
wenzelm@64621
    78
  private var current_rendering: JEdit_Rendering =
wenzelm@50501
    79
    Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
wenzelm@61561
    80
  private var future_refresh: Option[Future[Unit]] = None
wenzelm@49398
    81
wenzelm@50306
    82
  private val rich_text_area =
wenzelm@50915
    83
    new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
wenzelm@63028
    84
      get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
wenzelm@56883
    85
wenzelm@56883
    86
  private var current_search_pattern: Option[Regex] = None
wenzelm@57612
    87
  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
wenzelm@49416
    88
wenzelm@51451
    89
  def get_background(): Option[Color] = None
wenzelm@51451
    90
wenzelm@49398
    91
  def refresh()
wenzelm@49398
    92
  {
wenzelm@57612
    93
    GUI_Thread.require {}
wenzelm@49398
    94
wenzelm@55825
    95
    val font = current_font_info.font
wenzelm@50168
    96
    getPainter.setFont(font)
wenzelm@50168
    97
    getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
wenzelm@51497
    98
    getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
wenzelm@55825
    99
    getPainter.setStyles(
wenzelm@55825
   100
      SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
wenzelm@56789
   101
    getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))
wenzelm@50168
   102
wenzelm@50542
   103
    val fold_line_style = new Array[SyntaxStyle](4)
wenzelm@50542
   104
    for (i <- 0 to 3) {
wenzelm@50542
   105
      fold_line_style(i) =
wenzelm@50542
   106
        SyntaxUtilities.parseStyle(
wenzelm@50542
   107
          jEdit.getProperty("view.style.foldLine." + i),
wenzelm@55825
   108
          current_font_info.family, current_font_info.size.round, true)
wenzelm@50542
   109
    }
wenzelm@50542
   110
    getPainter.setFoldLineStyle(fold_line_style)
wenzelm@50542
   111
wenzelm@51439
   112
    getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
wenzelm@51439
   113
    getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
wenzelm@51451
   114
    get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
wenzelm@51439
   115
    getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
wenzelm@51439
   116
    getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
wenzelm@51439
   117
    getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
wenzelm@51439
   118
    getGutter.setBorder(0,
wenzelm@51439
   119
      jEdit.getColorProperty("view.gutter.focusBorderColor"),
wenzelm@51439
   120
      jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
wenzelm@51439
   121
      getPainter.getBackground)
wenzelm@60250
   122
    getGutter.setFoldPainter(view.getTextArea.getFoldPainter)
wenzelm@51439
   123
    getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
wenzelm@51439
   124
wenzelm@50166
   125
    if (getWidth > 0) {
wenzelm@51492
   126
      val metric = JEdit_Lib.pretty_metric(getPainter)
wenzelm@51493
   127
      val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0
wenzelm@49471
   128
wenzelm@50166
   129
      val base_snapshot = current_base_snapshot
wenzelm@50501
   130
      val base_results = current_base_results
wenzelm@51492
   131
      val formatted_body = Pretty.formatted(current_body, margin, metric)
wenzelm@49398
   132
wenzelm@61561
   133
      future_refresh.map(_.cancel)
wenzelm@61193
   134
      future_refresh =
wenzelm@61561
   135
        Some(Future.fork {
wenzelm@51498
   136
          val (text, rendering) =
wenzelm@51498
   137
            try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
wenzelm@51498
   138
            catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
wenzelm@56860
   139
          Exn.Interrupt.expose()
wenzelm@49398
   140
wenzelm@57612
   141
          GUI_Thread.later {
wenzelm@51498
   142
            current_rendering = rendering
wenzelm@51498
   143
            JEdit_Lib.buffer_edit(getBuffer) {
wenzelm@51498
   144
              rich_text_area.active_reset()
wenzelm@51498
   145
              getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
wenzelm@51498
   146
              setText(text)
wenzelm@51498
   147
              setCaretPosition(0)
wenzelm@51498
   148
            }
wenzelm@51498
   149
          }
wenzelm@56730
   150
        })
wenzelm@50166
   151
    }
wenzelm@49398
   152
  }
wenzelm@49398
   153
wenzelm@55825
   154
  def resize(font_info: Font_Info)
wenzelm@49398
   155
  {
wenzelm@57612
   156
    GUI_Thread.require {}
wenzelm@49398
   157
wenzelm@55825
   158
    current_font_info = font_info
wenzelm@49398
   159
    refresh()
wenzelm@49398
   160
  }
wenzelm@49398
   161
wenzelm@50501
   162
  def update(base_snapshot: Document.Snapshot, base_results: Command.Results, body: XML.Body)
wenzelm@49398
   163
  {
wenzelm@57612
   164
    GUI_Thread.require {}
wenzelm@49419
   165
    require(!base_snapshot.is_outdated)
wenzelm@49398
   166
wenzelm@49419
   167
    current_base_snapshot = base_snapshot
wenzelm@50501
   168
    current_base_results = base_results
wenzelm@49398
   169
    current_body = body
wenzelm@49398
   170
    refresh()
wenzelm@49398
   171
  }
wenzelm@49398
   172
wenzelm@56880
   173
  def detach
wenzelm@56880
   174
  {
wenzelm@57612
   175
    GUI_Thread.require {}
wenzelm@56880
   176
    Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
wenzelm@56880
   177
  }
wenzelm@56880
   178
wenzelm@56918
   179
  def detach_operation: Option[() => Unit] =
wenzelm@56918
   180
    if (current_body.isEmpty) None else Some(() => detach)
wenzelm@56918
   181
wenzelm@49422
   182
wenzelm@56881
   183
  /* common GUI components */
wenzelm@56881
   184
wenzelm@56883
   185
  val search_label: Component = new Label("Search:") {
wenzelm@56883
   186
    tooltip = "Search and highlight output via regular expression"
wenzelm@56883
   187
  }
wenzelm@56883
   188
wenzelm@57042
   189
  val search_field: Component =
wenzelm@56883
   190
    Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
wenzelm@56883
   191
      {
wenzelm@56883
   192
        private val input_delay =
wenzelm@57612
   193
          GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
wenzelm@56883
   194
            search_action(this)
wenzelm@56883
   195
          }
wenzelm@56885
   196
        getDocument.addDocumentListener(new DocumentListener {
wenzelm@56885
   197
          def changedUpdate(e: DocumentEvent) { input_delay.invoke() }
wenzelm@56885
   198
          def insertUpdate(e: DocumentEvent) { input_delay.invoke() }
wenzelm@56885
   199
          def removeUpdate(e: DocumentEvent) { input_delay.invoke() }
wenzelm@56885
   200
        })
wenzelm@56883
   201
        setColumns(20)
wenzelm@56883
   202
        setToolTipText(search_label.tooltip)
wenzelm@59286
   203
        setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
wenzelm@56883
   204
      })
wenzelm@56883
   205
wenzelm@57042
   206
  private val search_field_foreground = search_field.foreground
wenzelm@56883
   207
wenzelm@56883
   208
  private def search_action(text_field: JTextField)
wenzelm@56883
   209
  {
wenzelm@56883
   210
    val (pattern, ok) =
wenzelm@56883
   211
      text_field.getText match {
wenzelm@56883
   212
        case null | "" => (None, true)
wenzelm@56883
   213
        case s =>
wenzelm@59224
   214
          val re = Library.make_regex(s)
wenzelm@59224
   215
          (re, re.isDefined)
wenzelm@56883
   216
      }
wenzelm@56883
   217
    if (current_search_pattern != pattern) {
wenzelm@56883
   218
      current_search_pattern = pattern
wenzelm@56883
   219
      text_area.getPainter.repaint()
wenzelm@56883
   220
    }
wenzelm@56883
   221
    text_field.setForeground(
wenzelm@57042
   222
      if (ok) search_field_foreground else current_rendering.error_color)
wenzelm@56883
   223
  }
wenzelm@56883
   224
wenzelm@56881
   225
wenzelm@50726
   226
  /* key handling */
wenzelm@49422
   227
wenzelm@62214
   228
  override def getInputMethodRequests: InputMethodRequests = null
wenzelm@62214
   229
wenzelm@61570
   230
  inputHandlerProvider =
wenzelm@61570
   231
    new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) {
wenzelm@61570
   232
      override def getAction(action: String): JEditBeanShellAction =
wenzelm@61570
   233
        text_area.getActionContext.getAction(action)
wenzelm@61570
   234
      override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean) {}
wenzelm@61570
   235
      override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false
wenzelm@61570
   236
    })
wenzelm@61570
   237
wenzelm@53226
   238
  addKeyListener(JEdit_Lib.key_listener(
wenzelm@53226
   239
    key_pressed = (evt: KeyEvent) =>
wenzelm@53226
   240
      {
wenzelm@53226
   241
        evt.getKeyCode match {
wenzelm@58835
   242
          case KeyEvent.VK_C | KeyEvent.VK_INSERT
wenzelm@56323
   243
          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
wenzelm@56323
   244
              text_area.getSelectionCount != 0 =>
wenzelm@53226
   245
            Registers.copy(text_area, '$')
wenzelm@53226
   246
            evt.consume
wenzelm@53227
   247
wenzelm@53226
   248
          case KeyEvent.VK_A
wenzelm@53226
   249
          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
wenzelm@53226
   250
            text_area.selectAll
wenzelm@53226
   251
            evt.consume
wenzelm@53227
   252
wenzelm@53227
   253
          case KeyEvent.VK_ESCAPE =>
wenzelm@53244
   254
            if (PIDE.dismissed_popups(view)) evt.consume
wenzelm@53227
   255
wenzelm@53226
   256
          case _ =>
wenzelm@53226
   257
        }
wenzelm@53231
   258
        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
wenzelm@53226
   259
      },
wenzelm@53226
   260
    key_typed = (evt: KeyEvent) =>
wenzelm@53226
   261
      {
wenzelm@53231
   262
        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
wenzelm@49422
   263
      }
wenzelm@53226
   264
    )
wenzelm@53226
   265
  )
wenzelm@49422
   266
wenzelm@49422
   267
wenzelm@49422
   268
  /* init */
wenzelm@49422
   269
wenzelm@49472
   270
  getPainter.setStructureHighlightEnabled(false)
wenzelm@49475
   271
  getPainter.setLineHighlightEnabled(false)
wenzelm@49475
   272
wenzelm@59076
   273
  getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
wenzelm@63261
   274
  getBuffer.setStringProperty("noWordSep", "_'?⇩")
wenzelm@49475
   275
wenzelm@49412
   276
  rich_text_area.activate()
wenzelm@49398
   277
}