src/Tools/jEdit/src/jedit/SelectionActions.scala
author wenzelm
Tue, 27 Jan 2009 19:27:59 +0100
changeset 34503 7d0726f19d04
parent 34440 561a6d19bd95
permissions -rw-r--r--
tuned whitespace;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
     1
/*
34408
ad7b6c4813c8 added some headers and comments;
wenzelm
parents: 34387
diff changeset
     2
 * Text selection for XHTML renderer
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
     3
 *
34408
ad7b6c4813c8 added some headers and comments;
wenzelm
parents: 34387
diff changeset
     4
 * @author Fabian Immler, TU Munich
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
     5
 */
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
     6
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
     7
package isabelle.jedit
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
     8
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
     9
import org.w3c.dom.ranges.Range
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    10
import org.w3c.dom.DocumentFragment
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    11
import org.xhtmlrenderer.swing.SelectionHighlighter
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    12
import org.xhtmlrenderer.simple.XHTMLPanel
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    13
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    14
import java.awt.event.{KeyListener, KeyEvent}
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    15
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    16
import org.gjt.sp.jedit.gui._
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    17
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    18
class SelectionActions extends SelectionHighlighter with KeyListener{
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    19
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    20
  override def install(panel: XHTMLPanel) {
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    21
    super.install(panel)
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    22
    panel.addKeyListener(this)
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    23
  }
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    24
  
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    25
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    26
  def copyaction {
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    27
      val selected_string = getSelectionRange.toString
34440
561a6d19bd95 renamed object Plugin to Isabelle;
wenzelm
parents: 34435
diff changeset
    28
      val encoded = Isabelle.symbols.encode(selected_string)
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    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
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    31
      clipboard.setContents(transferable, null)
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    32
  }
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    33
  
34435
926272164bff renamed Plugin.plugin to Plugin.self;
wenzelm
parents: 34408
diff changeset
    34
  override def keyPressed(e: KeyEvent) {
34503
7d0726f19d04 tuned whitespace;
wenzelm
parents: 34440
diff changeset
    35
    if (e.getKeyCode == KeyEvent.VK_ENTER) {
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    36
      copyaction
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    37
      e.consume
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    38
    }
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    39
  }
34435
926272164bff renamed Plugin.plugin to Plugin.self;
wenzelm
parents: 34408
diff changeset
    40
  
926272164bff renamed Plugin.plugin to Plugin.self;
wenzelm
parents: 34408
diff changeset
    41
  override def keyReleased(e: KeyEvent) {
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    42
  }
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    43
34435
926272164bff renamed Plugin.plugin to Plugin.self;
wenzelm
parents: 34408
diff changeset
    44
  override def keyTyped(e: KeyEvent) {
926272164bff renamed Plugin.plugin to Plugin.self;
wenzelm
parents: 34408
diff changeset
    45
  }
34371
4a63526bead1 copy-paste for XHTMLPanels
immler@in.tum.de
parents:
diff changeset
    46
}