# HG changeset patch
# User wenzelm
# Date 1285244815 -7200
# Node ID 57496c868dcccee431ac31bfb14fc008d6d3de4a
# Parent  6aae022fde9b12fcc3322dd5ee686d5de4982559
tuned Isabelle_Sidekick.complete: lock buffer, depend on document model;

diff -r 6aae022fde9b -r 57496c868dcc src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Sep 23 13:28:19 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Sep 23 14:26:55 2010 +0200
@@ -66,24 +66,28 @@
 
   override def complete(pane: EditPane, caret: Int): SideKickCompletion =
   {
-    // FIXME lock buffer (!?)
     val buffer = pane.getBuffer
-
-    val line = buffer.getLineOfOffset(caret)
-    val start = buffer.getLineStartOffset(line)
-    val text = buffer.getSegment(start, caret - start)
-
-    val completion = Isabelle.session.current_syntax().completion
+    Isabelle.swing_buffer_lock(buffer) {
+      Document_Model(buffer) match {
+        case None => null
+        case Some(model) =>
+          val line = buffer.getLineOfOffset(caret)
+          val start = buffer.getLineStartOffset(line)
+          val text = buffer.getSegment(start, caret - start)
 
-    completion.complete(text) match {
-      case None => null
-      case Some((word, cs)) =>
-        val ds =
-          (if (Isabelle_Encoding.is_active(buffer))
-            cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
-           else cs).filter(_ != word)
-        if (ds.isEmpty) null
-        else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
+          val completion = model.session.current_syntax().completion
+          completion.complete(text) match {
+            case None => null
+            case Some((word, cs)) =>
+              val ds =
+                (if (Isabelle_Encoding.is_active(buffer))
+                  cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
+                 else cs).filter(_ != word)
+              if (ds.isEmpty) null
+              else new SideKickCompletion(
+                pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
+          }
+      }
     }
   }
 }