1 package isabelle.jedit |
1 package isabelle.jedit |
2 |
2 |
3 |
3 |
4 import java.awt.GridLayout |
4 import java.awt.BorderLayout |
5 import javax.swing.{ JPanel, JScrollPane } |
5 import javax.swing.{ JButton, JPanel, JScrollPane } |
6 |
6 |
7 import isabelle.IsabelleSystem.getenv |
7 import isabelle.IsabelleSystem.getenv |
8 |
8 |
9 import org.w3c.dom.Document |
9 import org.w3c.dom.Document |
10 |
10 |
11 import org.xhtmlrenderer.simple.XHTMLPanel |
11 import org.xhtmlrenderer.simple.XHTMLPanel |
12 import org.xhtmlrenderer.context.AWTFontResolver |
12 import org.xhtmlrenderer.context.AWTFontResolver |
13 |
13 |
14 import org.gjt.sp.jedit.View |
14 import org.gjt.sp.jedit.View |
15 |
15 |
|
16 //Copy-Paste-support |
|
17 import org.w3c.dom.ranges.Range |
|
18 import org.w3c.dom.DocumentFragment |
|
19 import org.xhtmlrenderer.swing.SelectionHighlighter |
|
20 |
16 class StateViewDockable(view : View, position : String) extends JPanel { |
21 class StateViewDockable(view : View, position : String) extends JPanel { |
17 { |
22 { |
18 val panel = new XHTMLPanel(new UserAgent()) |
23 val panel = new XHTMLPanel(new UserAgent()) |
19 setLayout(new GridLayout(1, 1)) |
24 setLayout(new BorderLayout) |
20 add(new JScrollPane(panel)) |
25 |
|
26 //Copy-paste-support |
|
27 val sel_highlighter = new SelectionHighlighter |
|
28 |
|
29 val copyaction = new SelectionHighlighter.CopyAction { |
|
30 override def actionPerformed(e: java.awt.event.ActionEvent) { |
|
31 System.err.println (sel_highlighter.getSelectionRange) |
|
32 } |
|
33 } |
|
34 copyaction.install(sel_highlighter) |
|
35 sel_highlighter.install(panel) |
|
36 add(new JButton(copyaction), BorderLayout.SOUTH) |
|
37 |
|
38 add(new JScrollPane(panel), BorderLayout.CENTER) |
21 |
39 |
22 val fontResolver = |
40 val fontResolver = |
23 panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver] |
41 panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver] |
24 if (Plugin.plugin.viewFont != null) |
42 if (Plugin.plugin.viewFont != null) |
25 fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |
43 fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont) |