# HG changeset patch
# User wenzelm
# Date 1261507157 -3600
# Node ID 006331f2b1283671f8f02638fc870f8cf668b36a
# Parent  89fa7e0e8e69db4fe53a9b61f923354a4e3e6cde
adapted to class Outer_Syntax;

diff -r 89fa7e0e8e69 -r 006331f2b128 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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
diff -r 89fa7e0e8e69 -r 006331f2b128 src/Tools/jEdit/src/proofdocument/proof_document.scala
--- 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
diff -r 89fa7e0e8e69 -r 006331f2b128 src/Tools/jEdit/src/proofdocument/session.scala
--- 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