1/* Title: Tools/jEdit/src/pretty_text_area.scala 2 Author: Makarius 3 4GUI component for pretty-printed text with markup, rendered like jEdit 5text area. 6*/ 7 8package isabelle.jedit 9 10 11import isabelle._ 12 13import java.awt.{Color, Font, Toolkit, Window} 14import java.awt.event.KeyEvent 15import java.awt.im.InputMethodRequests 16import javax.swing.JTextField 17import javax.swing.event.{DocumentListener, DocumentEvent} 18 19import scala.swing.{Label, Component} 20import scala.util.matching.Regex 21 22import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction} 23import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler} 24import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea} 25import org.gjt.sp.jedit.syntax.SyntaxStyle 26import org.gjt.sp.jedit.gui.KeyEventTranslator 27import org.gjt.sp.util.{SyntaxUtilities, Log} 28 29 30object 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, 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 66class 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, Font_Info.main_family(), 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} 280