# HG changeset patch
# User wenzelm
# Date 1233082376 -3600
# Node ID 87f4f70d61bb4058dd297c65c606a50ad09d7fb5
# Parent  4bd6766627925a1c56c576e4b3ae1fd313a93a8d
ProofDocument: pass is_command_keyword directly, not via full-blown Prover object;

diff -r 4bd676662792 -r 87f4f70d61bb src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jan 27 19:41:44 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jan 27 19:52:56 2009 +0100
@@ -37,7 +37,7 @@
 
 }
 
-class ProofDocument(text: Text, prover: Prover)
+class ProofDocument(text: Text, is_command_keyword: String => Boolean)
 {
   private var active = false 
   def activate() {
@@ -103,7 +103,7 @@
     while (matcher.find(position) && !finished) {
       position = matcher.end
 			val kind =
-        if (prover.is_command_keyword(matcher.group))
+        if (is_command_keyword(matcher.group))
           Token.Kind.COMMAND_START
         else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
           Token.Kind.COMMENT
diff -r 4bd676662792 -r 87f4f70d61bb src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 27 19:41:44 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 27 19:52:56 2009 +0100
@@ -50,7 +50,6 @@
       super.+=(entry)
     }
   }
-  def is_command_keyword(s: String): Boolean = command_decls.contains(s)
 
 
   /* completions */
@@ -178,7 +177,7 @@
   }
 
   def set_document(text: Text, path: String) {
-    this.document = new ProofDocument(text, this)
+    this.document = new ProofDocument(text, command_decls.contains(_))
     process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))
 
     document.structural_changes += (changes => {