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