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