src/Tools/jEdit/src/pretty_text_area.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 57042 5576d22abf3c
child 58766 5bab56d3dcd4
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
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@50726
    13
import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
wenzelm@53226
    14
import java.awt.event.KeyEvent
wenzelm@56883
    15
import javax.swing.JTextField
wenzelm@56885
    16
import javax.swing.event.{DocumentListener, DocumentEvent}
wenzelm@56883
    17
wenzelm@56730
    18
import java.util.concurrent.{Future => JFuture}
wenzelm@49412
    19
wenzelm@56907
    20
import scala.swing.{Label, Component}
wenzelm@56883
    21
import scala.util.matching.Regex
wenzelm@56881
    22
wenzelm@49422
    23
import org.gjt.sp.jedit.{jEdit, View, Registers}
wenzelm@49398
    24
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
wenzelm@50542
    25
import org.gjt.sp.jedit.syntax.SyntaxStyle
wenzelm@50640
    26
import org.gjt.sp.util.{SyntaxUtilities, Log}
wenzelm@49412
    27
wenzelm@49398
    28
wenzelm@49412
    29
object Pretty_Text_Area
wenzelm@49412
    30
{
wenzelm@56883
    31
  /* auxiliary */
wenzelm@56883
    32
wenzelm@50501
    33
  private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
wenzelm@50501
    34
    formatted_body: XML.Body): (String, Document.State) =
wenzelm@49412
    35
  {
wenzelm@52530
    36
    val command = Command.rich_text(Document_ID.make(), base_results, formatted_body)
wenzelm@49412
    37
    val node_name = command.node_name
wenzelm@49412
    38
    val edits: List[Document.Edit_Text] =
wenzelm@49414
    39
      List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
wenzelm@49412
    40
wenzelm@49419
    41
    val state0 = base_snapshot.state.define_command(command)
wenzelm@49419
    42
    val version0 = base_snapshot.version
wenzelm@49412
    43
    val nodes0 = version0.nodes
wenzelm@49412
    44
wenzelm@49412
    45
    val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
wenzelm@49412
    46
    val version1 = Document.Version.make(version0.syntax, nodes1)
wenzelm@49412
    47
    val state1 =
wenzelm@56711
    48
      state0.continue_history(Future.value(version0), edits, Future.value(version1))
wenzelm@49412
    49
        .define_version(version1, state0.the_assignment(version0))
wenzelm@52530
    50
        .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
wenzelm@49412
    51
wenzelm@49416
    52
    (command.source, state1)
wenzelm@49412
    53
  }
wenzelm@51495
    54
wenzelm@51495
    55
  private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
wenzelm@51495
    56
    formatted_body: XML.Body): (String, Rendering) =
wenzelm@51495
    57
  {
wenzelm@51495
    58
    val (text, state) = document_state(base_snapshot, base_results, formatted_body)
wenzelm@51495
    59
    val rendering = Rendering(state.snapshot(), PIDE.options.value)
wenzelm@51495
    60
    (text, rendering)
wenzelm@51495
    61
  }
wenzelm@49412
    62
}
wenzelm@49412
    63
wenzelm@50538
    64
class Pretty_Text_Area(
wenzelm@50538
    65
  view: View,
wenzelm@50915
    66
  close_action: () => Unit = () => (),
wenzelm@50743
    67
  propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
wenzelm@49398
    68
{
wenzelm@49446
    69
  text_area =>
wenzelm@49446
    70
wenzelm@57612
    71
  GUI_Thread.require {}
wenzelm@49398
    72
wenzelm@55826
    73
  private var current_font_info: Font_Info = Font_Info.main()
wenzelm@49398
    74
  private var current_body: XML.Body = Nil
wenzelm@52972
    75
  private var current_base_snapshot = Document.Snapshot.init
wenzelm@50507
    76
  private var current_base_results = Command.Results.empty
wenzelm@50199
    77
  private var current_rendering: Rendering =
wenzelm@50501
    78
    Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
wenzelm@56730
    79
  private var future_rendering: Option[JFuture[Unit]] = None
wenzelm@49398
    80
wenzelm@50306
    81
  private val rich_text_area =
wenzelm@50915
    82
    new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
wenzelm@56883
    83
      get_search_pattern _, caret_visible = false, enable_hovering = true)
wenzelm@56883
    84
wenzelm@56883
    85
  private var current_search_pattern: Option[Regex] = None
wenzelm@57612
    86
  def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
wenzelm@49416
    87
wenzelm@51451
    88
  def get_background(): Option[Color] = None
wenzelm@51451
    89
wenzelm@49398
    90
  def refresh()
wenzelm@49398
    91
  {
wenzelm@57612
    92
    GUI_Thread.require {}
wenzelm@49398
    93
wenzelm@55825
    94
    val font = current_font_info.font
wenzelm@50168
    95
    getPainter.setFont(font)
wenzelm@50168
    96
    getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
wenzelm@51497
    97
    getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
wenzelm@55825
    98
    getPainter.setStyles(
wenzelm@55825
    99
      SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
wenzelm@56789
   100
    getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))
wenzelm@50168
   101
wenzelm@50542
   102
    val fold_line_style = new Array[SyntaxStyle](4)
wenzelm@50542
   103
    for (i <- 0 to 3) {
wenzelm@50542
   104
      fold_line_style(i) =
wenzelm@50542
   105
        SyntaxUtilities.parseStyle(
wenzelm@50542
   106
          jEdit.getProperty("view.style.foldLine." + i),
wenzelm@55825
   107
          current_font_info.family, current_font_info.size.round, true)
wenzelm@50542
   108
    }
wenzelm@50542
   109
    getPainter.setFoldLineStyle(fold_line_style)
wenzelm@50542
   110
wenzelm@51439
   111
    getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
wenzelm@51439
   112
    getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
wenzelm@51451
   113
    get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
wenzelm@51439
   114
    getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
wenzelm@51439
   115
    getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
wenzelm@51439
   116
    getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
wenzelm@51439
   117
    getGutter.setBorder(0,
wenzelm@51439
   118
      jEdit.getColorProperty("view.gutter.focusBorderColor"),
wenzelm@51439
   119
      jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
wenzelm@51439
   120
      getPainter.getBackground)
wenzelm@51439
   121
    getGutter.setFoldPainter(getFoldPainter)
wenzelm@51439
   122
    getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
wenzelm@51439
   123
wenzelm@50166
   124
    if (getWidth > 0) {
wenzelm@51492
   125
      val metric = JEdit_Lib.pretty_metric(getPainter)
wenzelm@51493
   126
      val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0
wenzelm@49471
   127
wenzelm@50166
   128
      val base_snapshot = current_base_snapshot
wenzelm@50501
   129
      val base_results = current_base_results
wenzelm@51492
   130
      val formatted_body = Pretty.formatted(current_body, margin, metric)
wenzelm@49398
   131
wenzelm@51498
   132
      future_rendering.map(_.cancel(true))
wenzelm@56730
   133
      future_rendering =
wenzelm@56730
   134
        Some(Simple_Thread.submit_task {
wenzelm@51498
   135
          val (text, rendering) =
wenzelm@51498
   136
            try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
wenzelm@51498
   137
            catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
wenzelm@56860
   138
          Exn.Interrupt.expose()
wenzelm@49398
   139
wenzelm@57612
   140
          GUI_Thread.later {
wenzelm@51498
   141
            current_rendering = rendering
wenzelm@51498
   142
            JEdit_Lib.buffer_edit(getBuffer) {
wenzelm@51498
   143
              rich_text_area.active_reset()
wenzelm@51498
   144
              getBuffer.setReadOnly(false)
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
              getBuffer.setReadOnly(true)
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@56883
   204
        setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 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@56883
   215
          try { (Some(new Regex(s)), true) }
wenzelm@56883
   216
          catch { case ERROR(_) => (None, false) }
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@57042
   223
      if (ok) search_field_foreground else current_rendering.error_color)
wenzelm@56883
   224
  }
wenzelm@56883
   225
wenzelm@56881
   226
wenzelm@50726
   227
  /* key handling */
wenzelm@49422
   228
wenzelm@53226
   229
  addKeyListener(JEdit_Lib.key_listener(
wenzelm@53226
   230
    key_pressed = (evt: KeyEvent) =>
wenzelm@53226
   231
      {
wenzelm@53226
   232
        evt.getKeyCode match {
wenzelm@53226
   233
          case KeyEvent.VK_C
wenzelm@56323
   234
          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 &&
wenzelm@56323
   235
              text_area.getSelectionCount != 0 =>
wenzelm@53226
   236
            Registers.copy(text_area, '$')
wenzelm@53226
   237
            evt.consume
wenzelm@53227
   238
wenzelm@53226
   239
          case KeyEvent.VK_A
wenzelm@53226
   240
          if (evt.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0 =>
wenzelm@53226
   241
            text_area.selectAll
wenzelm@53226
   242
            evt.consume
wenzelm@53227
   243
wenzelm@53227
   244
          case KeyEvent.VK_ESCAPE =>
wenzelm@53244
   245
            if (PIDE.dismissed_popups(view)) evt.consume
wenzelm@53227
   246
wenzelm@53226
   247
          case _ =>
wenzelm@53226
   248
        }
wenzelm@53231
   249
        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
wenzelm@53226
   250
      },
wenzelm@53226
   251
    key_typed = (evt: KeyEvent) =>
wenzelm@53226
   252
      {
wenzelm@53231
   253
        if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
wenzelm@49422
   254
      }
wenzelm@53226
   255
    )
wenzelm@53226
   256
  )
wenzelm@49422
   257
wenzelm@49422
   258
wenzelm@49422
   259
  /* init */
wenzelm@49422
   260
wenzelm@49472
   261
  getPainter.setStructureHighlightEnabled(false)
wenzelm@49475
   262
  getPainter.setLineHighlightEnabled(false)
wenzelm@49475
   263
wenzelm@53277
   264
  getBuffer.setTokenMarker(Isabelle.token_marker("isabelle-output").get)
wenzelm@49446
   265
  getBuffer.setReadOnly(true)
wenzelm@53002
   266
  getBuffer.setStringProperty("noWordSep", "_'.?")
wenzelm@49475
   267
wenzelm@49412
   268
  rich_text_area.activate()
wenzelm@49398
   269
}
wenzelm@49398
   270