# HG changeset patch
# User wenzelm
# Date 1219761371 -7200
# Node ID 116b9c1d402fac3c0ee34048674ffd4ba6124637
# Parent  0e71a3b1b39631d72eb1a4e4c7a9e6215402c87f
command: symbols.encode;

diff -r 0e71a3b1b396 -r 116b9c1d402f lib/jedit/plugin/isabelle_dock.scala
--- a/lib/jedit/plugin/isabelle_dock.scala	Tue Aug 26 16:04:22 2008 +0200
+++ b/lib/jedit/plugin/isabelle_dock.scala	Tue Aug 26 16:36:11 2008 +0200
@@ -118,7 +118,7 @@
     text.setToolTipText("Command line")
     text.addActionListener(new ActionListener {
       def actionPerformed(evt: ActionEvent): Unit = {
-        val command = text.getText
+        val command = IsabellePlugin.symbols.encode(text.getText)
         if (command.length > 0) {
           if (mode == mode_Isar)
             IsabellePlugin.isabelle.command(command)