author | wenzelm |
Tue, 27 Jan 2009 19:27:59 +0100 | |
changeset 34503 | 7d0726f19d04 |
parent 34440 | 561a6d19bd95 |
permissions | -rw-r--r-- |
34371 | 1 |
/* |
34408 | 2 |
* Text selection for XHTML renderer |
34371 | 3 |
* |
34408 | 4 |
* @author Fabian Immler, TU Munich |
34371 | 5 |
*/ |
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
import org.w3c.dom.ranges.Range |
|
10 |
import org.w3c.dom.DocumentFragment |
|
11 |
import org.xhtmlrenderer.swing.SelectionHighlighter |
|
12 |
import org.xhtmlrenderer.simple.XHTMLPanel |
|
13 |
||
14 |
import java.awt.event.{KeyListener, KeyEvent} |
|
15 |
||
16 |
import org.gjt.sp.jedit.gui._ |
|
17 |
||
18 |
class SelectionActions extends SelectionHighlighter with KeyListener{ |
|
19 |
||
20 |
override def install(panel: XHTMLPanel) { |
|
21 |
super.install(panel) |
|
22 |
panel.addKeyListener(this) |
|
23 |
} |
|
24 |
||
25 |
||
26 |
def copyaction { |
|
27 |
val selected_string = getSelectionRange.toString |
|
34440 | 28 |
val encoded = Isabelle.symbols.encode(selected_string) |
34371 | 29 |
val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard; |
34387
d67fe0cb1106
removed xsymbol converting -> sidekick should do that
immler@in.tum.de
parents:
34371
diff
changeset
|
30 |
val transferable = new java.awt.datatransfer.StringSelection(selected_string) |
34371 | 31 |
clipboard.setContents(transferable, null) |
32 |
} |
|
33 |
||
34435 | 34 |
override def keyPressed(e: KeyEvent) { |
34503 | 35 |
if (e.getKeyCode == KeyEvent.VK_ENTER) { |
34371 | 36 |
copyaction |
37 |
e.consume |
|
38 |
} |
|
39 |
} |
|
34435 | 40 |
|
41 |
override def keyReleased(e: KeyEvent) { |
|
34371 | 42 |
} |
43 |
||
34435 | 44 |
override def keyTyped(e: KeyEvent) { |
45 |
} |
|
34371 | 46 |
} |