ProofDocument: pass is_command_keyword directly, not via full-blown Prover object;
--- 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 => {