# HG changeset patch
# User wenzelm
# Date 1261492530 -3600
# Node ID 0330a4284a9b2ebbc711fcde16247f846176b161
# Parent  db0da30bca268c257405ac52aa89c4359e78233a
just one variable for outer syntax keywords and completion;

diff -r db0da30bca26 -r 0330a4284a9b src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Mon Dec 21 21:50:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Tue Dec 22 15:35:30 2009 +0100
@@ -85,7 +85,7 @@
     val start = buffer.getLineStartOffset(line)
     val text = buffer.getSegment(start, caret - start)
 
-    val completion = Isabelle.session.completion()
+    val completion = Isabelle.session.keywords.completion
 
     completion.complete(text) match {
       case None => null
diff -r db0da30bca26 -r 0330a4284a9b src/Tools/jEdit/src/proofdocument/proof_document.scala
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Mon Dec 21 21:50:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 22 15:35:30 2009 +0100
@@ -114,7 +114,7 @@
 
     while (matcher.find() && invalid_tokens != Nil) {
 			val kind =
-        if (session.is_command_keyword(matcher.group))
+        if (session.keywords.is_command(matcher.group))
           Token.Kind.COMMAND_START
         else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
           Token.Kind.COMMENT
diff -r db0da30bca26 -r 0330a4284a9b src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Mon Dec 21 21:50:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Tue Dec 22 15:35:30 2009 +0100
@@ -28,6 +28,9 @@
   private case class Start(args: List[String])
   private case object Stop
 
+  @volatile private var _keywords = new Outer_Keyword(system.symbols)
+  def keywords = _keywords
+
   private var prover: Isabelle_Process with Isar_Document = null
   private var prover_ready = false
 
@@ -80,20 +83,6 @@
   def selected_state_=(state: Command) { _selected_state = state; results.event(state) }
 
 
-  /* outer syntax keywords and completion */
-
-  @volatile private var _command_decls = Map[String, String]()
-  def command_decls() = _command_decls
-
-  @volatile private var _keyword_decls = Set[String]()
-  def keyword_decls() = _keyword_decls
-
-  @volatile private var _completion = new Completion + system.symbols
-  def completion() = _completion
-
-  def is_command_keyword(s: String): Boolean = command_decls().contains(s)
-
-
   /* document state information */
 
   @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
@@ -174,11 +163,9 @@
 
           // command and keyword declarations
           case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
-            _command_decls += (name -> kind)
-            _completion += name
+            _keywords += (name, kind)
           case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
-            _keyword_decls += name
-            _completion += name
+            _keywords += name
 
           // process ready (after initialization)
           case XML.Elem(Markup.READY, _, _) => prover_ready = true