src/Tools/jEdit/src/jedit/SelectionActions.scala
changeset 34758 710e3a9a4c95
parent 34757 adf4e0f27d54
child 34759 bfea7839d9e1
     1.1 --- a/src/Tools/jEdit/src/jedit/SelectionActions.scala	Tue Dec 08 12:10:55 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,46 +0,0 @@
     1.4 -/*
     1.5 - * Text selection for XHTML renderer
     1.6 - *
     1.7 - * @author Fabian Immler, TU Munich
     1.8 - */
     1.9 -
    1.10 -package isabelle.jedit
    1.11 -
    1.12 -import org.w3c.dom.ranges.Range
    1.13 -import org.w3c.dom.DocumentFragment
    1.14 -import org.xhtmlrenderer.swing.SelectionHighlighter
    1.15 -import org.xhtmlrenderer.simple.XHTMLPanel
    1.16 -
    1.17 -import java.awt.event.{KeyListener, KeyEvent}
    1.18 -
    1.19 -import org.gjt.sp.jedit.gui._
    1.20 -
    1.21 -class SelectionActions extends SelectionHighlighter with KeyListener{
    1.22 -
    1.23 -  override def install(panel: XHTMLPanel) {
    1.24 -    super.install(panel)
    1.25 -    panel.addKeyListener(this)
    1.26 -  }
    1.27 -  
    1.28 -
    1.29 -  def copyaction {
    1.30 -      val selected_string = getSelectionRange.toString
    1.31 -      val encoded = Isabelle.symbols.encode(selected_string)
    1.32 -      val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard;
    1.33 -      val transferable = new java.awt.datatransfer.StringSelection(selected_string)
    1.34 -      clipboard.setContents(transferable, null)
    1.35 -  }
    1.36 -  
    1.37 -  override def keyPressed(e: KeyEvent) {
    1.38 -    if (e.getKeyCode == KeyEvent.VK_ENTER) {
    1.39 -      copyaction
    1.40 -      e.consume
    1.41 -    }
    1.42 -  }
    1.43 -  
    1.44 -  override def keyReleased(e: KeyEvent) {
    1.45 -  }
    1.46 -
    1.47 -  override def keyTyped(e: KeyEvent) {
    1.48 -  }
    1.49 -}