# HG changeset patch
# User wenzelm
# Date 1260278969 -3600
# Node ID 710e3a9a4c9548983db3d2d591181276983b6424
# Parent  adf4e0f27d54bdbc72c1fe29d0756585e0562172
removed remains of Flying Saucer;

diff -r adf4e0f27d54 -r 710e3a9a4c95 src/Tools/jEdit/nbproject/project.properties
--- a/src/Tools/jEdit/nbproject/project.properties	Tue Dec 08 12:10:55 2009 +0100
+++ b/src/Tools/jEdit/nbproject/project.properties	Tue Dec 08 14:29:29 2009 +0100
@@ -30,7 +30,6 @@
 jar.compress=false
 java.platform.active=java_default_platform
 javac.classpath=\
-    ${libs.Flying-Saucer.classpath}:\
     ${reference.jEdit.build}:\
     ${libs.Isabelle-Pure.classpath}:\
     ${libs.Sidekick.classpath}:\
diff -r adf4e0f27d54 -r 710e3a9a4c95 src/Tools/jEdit/src/jedit/SelectionActions.scala
--- a/src/Tools/jEdit/src/jedit/SelectionActions.scala	Tue Dec 08 12:10:55 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-/*
- * Text selection for XHTML renderer
- *
- * @author Fabian Immler, TU Munich
- */
-
-package isabelle.jedit
-
-import org.w3c.dom.ranges.Range
-import org.w3c.dom.DocumentFragment
-import org.xhtmlrenderer.swing.SelectionHighlighter
-import org.xhtmlrenderer.simple.XHTMLPanel
-
-import java.awt.event.{KeyListener, KeyEvent}
-
-import org.gjt.sp.jedit.gui._
-
-class SelectionActions extends SelectionHighlighter with KeyListener{
-
-  override def install(panel: XHTMLPanel) {
-    super.install(panel)
-    panel.addKeyListener(this)
-  }
-  
-
-  def copyaction {
-      val selected_string = getSelectionRange.toString
-      val encoded = Isabelle.symbols.encode(selected_string)
-      val clipboard = java.awt.Toolkit.getDefaultToolkit().getSystemClipboard;
-      val transferable = new java.awt.datatransfer.StringSelection(selected_string)
-      clipboard.setContents(transferable, null)
-  }
-  
-  override def keyPressed(e: KeyEvent) {
-    if (e.getKeyCode == KeyEvent.VK_ENTER) {
-      copyaction
-      e.consume
-    }
-  }
-  
-  override def keyReleased(e: KeyEvent) {
-  }
-
-  override def keyTyped(e: KeyEvent) {
-  }
-}