removed remains of Flying Saucer;
authorwenzelm
Tue Dec 08 14:29:29 2009 +0100 (2009-12-08)
changeset 34758710e3a9a4c95
parent 34757 adf4e0f27d54
child 34759 bfea7839d9e1
removed remains of Flying Saucer;
src/Tools/jEdit/nbproject/project.properties
src/Tools/jEdit/src/jedit/SelectionActions.scala
     1.1 --- a/src/Tools/jEdit/nbproject/project.properties	Tue Dec 08 12:10:55 2009 +0100
     1.2 +++ b/src/Tools/jEdit/nbproject/project.properties	Tue Dec 08 14:29:29 2009 +0100
     1.3 @@ -30,7 +30,6 @@
     1.4  jar.compress=false
     1.5  java.platform.active=java_default_platform
     1.6  javac.classpath=\
     1.7 -    ${libs.Flying-Saucer.classpath}:\
     1.8      ${reference.jEdit.build}:\
     1.9      ${libs.Isabelle-Pure.classpath}:\
    1.10      ${libs.Sidekick.classpath}:\
     2.1 --- a/src/Tools/jEdit/src/jedit/SelectionActions.scala	Tue Dec 08 12:10:55 2009 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,46 +0,0 @@
     2.4 -/*
     2.5 - * Text selection for XHTML renderer
     2.6 - *
     2.7 - * @author Fabian Immler, TU Munich
     2.8 - */
     2.9 -
    2.10 -package isabelle.jedit
    2.11 -
    2.12 -import org.w3c.dom.ranges.Range
    2.13 -import org.w3c.dom.DocumentFragment
    2.14 -import org.xhtmlrenderer.swing.SelectionHighlighter
    2.15 -import org.xhtmlrenderer.simple.XHTMLPanel
    2.16 -
    2.17 -import java.awt.event.{KeyListener, KeyEvent}
    2.18 -
    2.19 -import org.gjt.sp.jedit.gui._
    2.20 -
    2.21 -class SelectionActions extends SelectionHighlighter with KeyListener{
    2.22 -
    2.23 -  override def install(panel: XHTMLPanel) {
    2.24 -    super.install(panel)
    2.25 -    panel.addKeyListener(this)
    2.26 -  }
    2.27 -  
    2.28 -
    2.29 -  def copyaction {
    2.30 -      val selected_string = getSelectionRange.toString
    2.31 -      val encoded = Isabelle.symbols.encode(selected_string)
    2.32 -      val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard;
    2.33 -      val transferable = new java.awt.datatransfer.StringSelection(selected_string)
    2.34 -      clipboard.setContents(transferable, null)
    2.35 -  }
    2.36 -  
    2.37 -  override def keyPressed(e: KeyEvent) {
    2.38 -    if (e.getKeyCode == KeyEvent.VK_ENTER) {
    2.39 -      copyaction
    2.40 -      e.consume
    2.41 -    }
    2.42 -  }
    2.43 -  
    2.44 -  override def keyReleased(e: KeyEvent) {
    2.45 -  }
    2.46 -
    2.47 -  override def keyTyped(e: KeyEvent) {
    2.48 -  }
    2.49 -}