# HG changeset patch
# User immler@in.tum.de
# Date 1231789777 -3600
# Node ID f963335dbc6bcd4ac9facbb605528159f339a57c
# Parent  5f078db3cfc53b19f763c7ee6d9874d67c43f3ed
implemented IsabelleSideKickParser.complete
removed Plugin.prover (to avoid NoSuchElementException)

diff -r 5f078db3cfc5 -r f963335dbc6b src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Sun Jan 11 22:02:27 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Mon Jan 12 20:49:37 2009 +0100
@@ -7,10 +7,12 @@
 
 package isabelle.jedit
 
+import scala.collection.Set
+import scala.collection.immutable.TreeSet
 
 import javax.swing.tree.DefaultMutableTreeNode
 
-import org.gjt.sp.jedit.{Buffer, EditPane}
+import org.gjt.sp.jedit.{Buffer, EditPane, View}
 import errorlist.DefaultErrorSource
 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion}
 
@@ -26,18 +28,18 @@
     stopped = false
     
     val data = new SideKickParsedData(buffer.getName)
-    
-    Isabelle.plugin.prover_setup(buffer) match {
-      case None =>
-        data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
-      case Some(prover_setup) =>
-        val document = prover_setup.prover.document
+
+    val prover_setup = Isabelle.plugin.prover_setup(buffer)
+    if(prover_setup.isDefined){
+        val document = prover_setup.get.prover.document
         val commands = document.commands()
         while (!stopped && commands.hasNext) {
           data.root.add(commands.next.root_node.swing_node)
         }
         if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
-      }
+    } else {
+      data.root.add(new DefaultMutableTreeNode("<buffer inactive>"))
+    }
 
     data
   }
@@ -47,6 +49,48 @@
 
   override def supportsCompletion = true
   override def canCompleteAnywhere = true
+  override def getInstantCompletionTriggers = "\\"
 
-  override def complete(pane: EditPane, caret: Int): SideKickCompletion = null  // TODO
+  override def complete(pane: EditPane, caret: Int): SideKickCompletion = {
+    val buffer = pane.getBuffer
+    val ps = Isabelle.prover_setup(buffer)
+    if(ps.isDefined) {
+      val completions = ps.get.prover.completions
+      def before_caret(i : Int) = buffer.getText(0 max caret - i, i)
+      def next_nonfitting(s : String) : String = {
+        val sa = s.toCharArray
+        sa(s.length - 1) = (sa(s.length - 1) + 1).asInstanceOf[Char]
+        new String(sa)
+      }
+      def suggestions(i : Int) : (Set[String], String)= {
+        val text = before_caret(i)
+        if(!text.matches("\\s") && i < 30){
+          val larger_results = suggestions(i + 1)
+          if(larger_results._1.size > 0) larger_results
+          else (completions.range(text, next_nonfitting(text)), text)
+        } else (Set[String](), text)
+
+      }
+
+      val list = new java.util.LinkedList[String]
+      val descriptions = new java.util.LinkedList[String]
+      // compute suggestions
+      val (suggs,text) = suggestions(1)
+      for(s <- suggs) {
+        val decoded = Isabelle.symbols.decode(s)
+        list.add(decoded)
+        if(!decoded.equals(s)) descriptions.add(s) else descriptions.add(null)
+      }
+      return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
+    } else return null
+  }
+
 }
+
+private class IsabelleSideKickCompletion(view: View, text: String,
+                                         items: java.util.List[String],
+                                         descriptions : java.util.List[String])
+  extends SideKickCompletion(view, text, items : java.util.List[String]) {
+
+  override def getCompletionDescription(i : Int) : String = descriptions.get(i)
+}
diff -r 5f078db3cfc5 -r f963335dbc6b src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Jan 11 22:02:27 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Jan 12 20:49:37 2009 +0100
@@ -45,8 +45,7 @@
   var plugin: Plugin = null
 
   // provers
-  def prover(buffer: JEditBuffer) = plugin.prover_setup(buffer).get.prover
-  def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer).get
+  def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
 }
 
 
diff -r 5f078db3cfc5 -r f963335dbc6b src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Jan 11 22:02:27 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Jan 12 20:49:37 2009 +0100
@@ -71,6 +71,7 @@
     extends TextAreaExtension with Text with BufferListener {
 
   private val buffer = text_area.getBuffer
+  private val prover = Isabelle.prover_setup(buffer).get.prover
   buffer.addBufferListener(this)
 
 
@@ -84,7 +85,7 @@
   col_timer.setRepeats(true)
 
 
-  private val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
+  private val phase_overview = new PhaseOverviewPanel(prover)
 
 
   /* activation */
@@ -106,10 +107,10 @@
 
   private val selected_state_controller = new CaretListener {
     override def caretUpdate(e: CaretEvent) = {
-      val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot)
+      val cmd = prover.document.getNextCommandContaining(e.getDot)
       if (cmd != null && cmd.start <= e.getDot &&
-          Isabelle.prover_setup(buffer).selected_state != cmd)
-        Isabelle.prover_setup(buffer).selected_state = cmd
+          Isabelle.prover_setup(buffer).get.selected_state != cmd)
+        Isabelle.prover_setup(buffer).get.selected_state = cmd
     }
   }
 
@@ -131,7 +132,7 @@
   /* painting */
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
-  Isabelle.prover(buffer).command_info += (_ => repaint_delay.delay_or_ignore())
+  prover.command_info += (_ => repaint_delay.delay_or_ignore())
 
   private def from_current(pos: Int) =
     if (col != null && col.start <= pos)
@@ -153,8 +154,8 @@
       val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
       text_area.invalidateLineRange(start, stop)
 
-      if (Isabelle.prover_setup(buffer).selected_state == cmd)
-        Isabelle.prover_setup(buffer).selected_state = cmd  // update State view
+      if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
+        Isabelle.prover_setup(buffer).get.selected_state = cmd  // update State view
     }
   }
 
@@ -192,7 +193,7 @@
     val saved_color = gfx.getColor
 
     val metrics = text_area.getPainter.getFontMetrics
-    var e = Isabelle.prover(buffer).document.getNextCommandContaining(from_current(start))
+    var e = prover.document.getNextCommandContaining(from_current(start))
 
     // encolor phase
     while (e != null && to_current(e.start) < end) {
diff -r 5f078db3cfc5 -r f963335dbc6b src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sun Jan 11 22:02:27 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Jan 12 20:49:37 2009 +0100
@@ -12,6 +12,7 @@
 import java.util.Properties
 
 import scala.collection.mutable.{HashMap, HashSet}
+import scala.collection.immutable.{TreeSet}
 
 import org.gjt.sp.util.Log
 
@@ -37,6 +38,17 @@
       super.+=(name)
     }
   }
+  var _completions = new TreeSet[String]
+  def completions = _completions
+  /* // TODO: ask Makarius to make Interpretation.symbols public (here: read-only as 'symbol_map')
+  val map = isabelle.jedit.Isabelle.symbols.symbol_map
+  for(xsymb <- map.keys) {
+    _completions += xsymb
+    if(map(xsymb).get("abbrev").isDefined) _completions += map(xsymb)("abbrev")
+  }
+  */
+  decl_info += (k_v => _completions += k_v._1)
+  
   private var initialized = false
 
   val activated = new EventBus[Unit]