# HG changeset patch
# User wenzelm
# Date 1245191134 -7200
# Node ID 44f9edc5801baf1915e1b93985f2dac51f52ebe9
# Parent  bb30b5056db63d921c8bdbfd33eebedbb218979c
basic keyword completions via isabelle.Scan.Lexicon;

diff -r bb30b5056db6 -r 44f9edc5801b src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jun 16 19:52:45 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Jun 17 00:25:34 2009 +0200
@@ -76,17 +76,10 @@
   }
 
 
-  /* completions */
+  /* completions */  // FIXME add symbols, symbol names, symbol abbrevs
 
-  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")
-  }
-  */
+  var _completions = Scan.Lexicon()
+  def completions(word: CharSequence) = _completions.completions(word)
   decl_info += (p => _completions += p._1)