--- 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
--- 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
--- 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