ProofDocument: pass is_command_keyword directly, not via full-blown Prover object;
authorwenzelm
Tue, 27 Jan 2009 19:52:56 +0100
changeset 34505 87f4f70d61bb
parent 34504 4bd676662792
child 34506 bc22e49358f8
ProofDocument: pass is_command_keyword directly, not via full-blown Prover object;
src/Tools/jEdit/src/proofdocument/ProofDocument.scala
src/Tools/jEdit/src/prover/Prover.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
--- 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 => {