--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sat Dec 20 18:25:15 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sun Dec 21 19:51:56 2008 +0100
@@ -13,27 +13,52 @@
import isabelle.IsabelleSystem.getenv
-import org.xhtmlrenderer.simple.XHTMLPanel
+import org.xhtmlrenderer.simple.{XHTMLPanel, FSScrollPane}
import org.xhtmlrenderer.context.AWTFontResolver
+import org.xhtmlrenderer.layout.SharedContext;
+import org.xhtmlrenderer.extend.TextRenderer;
+import org.xhtmlrenderer.swing.Java2DTextRenderer;
+import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.textarea.AntiAlias
class StateViewDockable(view : View, position : String) extends JPanel {
- val panel = new XHTMLPanel(new UserAgent())
+ // outer panel
if (position == DockableWindowManager.FLOATING)
setPreferredSize(new Dimension(500, 250))
-
setLayout(new BorderLayout)
-
- //Copy-paste-support
- private val cp = new SelectionActions
- cp.install(panel)
+
+ // XHTML panel
+ val panel = new XHTMLPanel(new UserAgent)
+
- add(new JScrollPane(panel), BorderLayout.CENTER)
+ // anti-aliasing
+ // TODO: proper EditBus event handling
+ {
+ val aa = jEdit.getProperty("view.antiAlias")
+ if (aa != null && aa != AntiAlias.NONE) {
+ panel.getSharedContext.setTextRenderer(
+ {
+ val renderer = new Java2DTextRenderer
+ renderer.setSmoothingThreshold(0)
+ renderer.setSmoothingLevel(TextRenderer.HIGH)
+ renderer
+ })
+ }
+ }
+
+ // copy & paste
+ (new SelectionActions).install(panel)
+
+
+ // scrolling
+ add(new FSScrollPane(panel), BorderLayout.CENTER)
+
private val fontResolver =
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]