# HG changeset patch
# User wenzelm
# Date 1246039654 -7200
# Node ID 799a40faa4f1574493d1095f663248d9ff3b3f75
# Parent  5e4f33d033ba35f777cc208520269232667b36e3
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
tuned;

diff -r 5e4f33d033ba -r 799a40faa4f1 src/Tools/jEdit/src/jedit/IsabelleEncoding.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleEncoding.scala	Fri Jun 26 19:56:52 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleEncoding.scala	Fri Jun 26 20:07:34 2009 +0200
@@ -7,6 +7,7 @@
 package isabelle.jedit
 
 import org.gjt.sp.jedit.io.Encoding
+import org.gjt.sp.jedit.buffer.JEditBuffer
 
 import java.nio.charset.{Charset, CharsetDecoder, CodingErrorAction}
 import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
@@ -18,6 +19,9 @@
 object IsabelleEncoding
 {
   val NAME = "UTF-8-Isabelle"
+
+  def is_active(buffer: JEditBuffer): Boolean =
+    buffer.getProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
 }
 
 class IsabelleEncoding extends Encoding
diff -r 5e4f33d033ba -r 799a40faa4f1 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Fri Jun 26 19:56:52 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Fri Jun 26 20:07:34 2009 +0200
@@ -17,28 +17,28 @@
 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
 
 
-class IsabelleSideKickParser extends SideKickParser("isabelle") {
-
+class IsabelleSideKickParser extends SideKickParser("isabelle")
+{
   /* parsing */
 
-  private var stopped = false
+  @volatile private var stopped = false
   override def stop() = { stopped = true }
 
-  def parse(buffer : Buffer, error_source : DefaultErrorSource): SideKickParsedData = {
+  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
+  {
     stopped = false
-    
+
     val data = new SideKickParsedData(buffer.getName)
 
     val prover_setup = Isabelle.plugin.prover_setup(buffer)
     if (prover_setup.isDefined) {
-        val document = prover_setup.get.prover.document
-        for (command <- document.commands)
-          data.root.add(command.markup_root.swing_node(document))
-        
-        if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
-    } else {
-      data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
+      val document = prover_setup.get.prover.document
+      for (command <- document.commands)
+        data.root.add(command.markup_root.swing_node(document))
+
+      if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
     }
+    else data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
 
     data
   }
@@ -63,8 +63,11 @@
     completion.complete(text) match {
       case None => null
       case Some((word, cs)) =>
-        new SideKickCompletion(pane.getView, word,
-          cs.map(Isabelle.system.symbols.decode(_)).toArray.asInstanceOf[Array[Object]]) { }
+        val ds =
+          if (IsabelleEncoding.is_active(buffer))
+            cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _)
+          else cs
+        new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
     }
   }