# HG changeset patch # User wenzelm # Date 1348068457 -7200 # Node ID b8d8f738bf6323790428635e7468b5a56d8e8496 # Parent 638cefe3ee99d4517480eae03d459bd1973c8488 more direct GUI component; diff -r 638cefe3ee99 -r b8d8f738bf63 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Sep 19 17:07:25 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Sep 19 17:27:37 2012 +0200 @@ -17,8 +17,6 @@ import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea} import org.gjt.sp.util.SyntaxUtilities -import scala.swing.{BorderPanel, Component} - object Pretty_Text_Area { @@ -47,8 +45,10 @@ } } -class Pretty_Text_Area(view: View) extends BorderPanel +class Pretty_Text_Area(view: View) extends JEditEmbeddedTextArea { + text_area => + Swing_Thread.require() private var current_font_metrics: FontMetrics = null @@ -59,9 +59,7 @@ private var current_base_snapshot = Document.State.init.snapshot() private var current_rendering: Isabelle_Rendering = text_rendering()._2 - private val text_area = new JEditEmbeddedTextArea private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering) - private val buffer = text_area.getBuffer private def text_rendering(): (String, Isabelle_Rendering) = { @@ -81,26 +79,25 @@ val font = new Font(current_font_family, Font.PLAIN, current_font_size) - val painter = text_area.getPainter - painter.setFont(font) - painter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias"))) - painter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) + getPainter.setFont(font) + getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias"))) + getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) current_font_metrics = painter.getFontMetrics(font) - current_margin = (size.width / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20 + current_margin = (getWidth / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20 val (text, rendering) = text_rendering() current_rendering = rendering try { - buffer.beginCompoundEdit - buffer.setReadOnly(false) - text_area.setText(text) - text_area.setCaretPosition(0) - buffer.setReadOnly(true) + getBuffer.beginCompoundEdit + getBuffer.setReadOnly(false) + setText(text) + setCaretPosition(0) + getBuffer.setReadOnly(true) } finally { - buffer.endCompoundEdit + getBuffer.endCompoundEdit } } @@ -135,18 +132,17 @@ } } - text_area.registerKeyboardAction(action_listener, "copy", + registerKeyboardAction(action_listener, "copy", KeyStroke.getKeyStroke(KeyEvent.VK_COPY, 0), JComponent.WHEN_FOCUSED) - text_area.registerKeyboardAction(action_listener, "copy", + registerKeyboardAction(action_listener, "copy", KeyStroke.getKeyStroke(KeyEvent.VK_C, Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()), JComponent.WHEN_FOCUSED) /* init */ - buffer.setTokenMarker(new Token_Markup.Marker(true, None)) - buffer.setReadOnly(true) - layout(Component.wrap(text_area)) = BorderPanel.Position.Center + getBuffer.setTokenMarker(new Token_Markup.Marker(true, None)) + getBuffer.setReadOnly(true) rich_text_area.activate() }