--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Dec 22 17:31:31 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Tue Dec 22 19:39:17 2009 +0100
@@ -85,7 +85,7 @@
val start = buffer.getLineStartOffset(line)
val text = buffer.getSegment(start, caret - start)
- val completion = Isabelle.session.keywords().completion
+ val completion = Isabelle.session.syntax().completion
completion.complete(text) match {
case None => null
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 22 17:31:31 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 22 19:39:17 2009 +0100
@@ -114,7 +114,7 @@
while (matcher.find() && invalid_tokens != Nil) {
val kind =
- if (session.keywords.is_command(matcher.group))
+ if (session.syntax().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 Tue Dec 22 17:31:31 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala Tue Dec 22 19:39:17 2009 +0100
@@ -28,8 +28,8 @@
private case class Start(args: List[String])
private case object Stop
- @volatile private var _keywords = new Outer_Keyword(system.symbols)
- def keywords(): Outer_Keyword = _keywords
+ @volatile private var _syntax = new Outer_Syntax(system.symbols)
+ def syntax(): Outer_Syntax = _syntax
private var prover: Isabelle_Process with Isar_Document = null
private var prover_ready = false
@@ -163,9 +163,9 @@
// command and keyword declarations
case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
- _keywords += (name, kind)
+ _syntax += (name, kind)
case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
- _keywords += name
+ _syntax += name
// process ready (after initialization)
case XML.Elem(Markup.READY, _, _) => prover_ready = true