--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Jan 19 21:04:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Mon Jan 19 21:38:50 2009 +0100
@@ -6,16 +6,18 @@
package isabelle.proofdocument
+
import java.util.regex.Pattern
-object ProofDocument {
+object ProofDocument
+{
// Be carefully when changeing this regex. Not only must it handle the
// spurious end of a token but also:
// Bug ID: 5050507 Pattern.matches throws StackOverflow Error
// http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
- val tokenPattern =
+ val token_pattern =
Pattern.compile(
"\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
"\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
@@ -25,14 +27,12 @@
"\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
"`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
"[()\\[\\]{}:;]", Pattern.MULTILINE)
-
}
-abstract class ProofDocument(text : Text) {
- import ProofDocument._
-
- protected var firstToken : Token = null
- protected var lastToken : Token = null
+abstract class ProofDocument(text: Text)
+{
+ protected var firstToken: Token = null
+ protected var lastToken: Token = null
private var active = false
text.changes += (e => textChanged(e.start, e.added, e.removed))
@@ -44,40 +44,40 @@
}
}
- protected def tokens(start : Token, stop : Token) =
- new Iterator[Token]() {
+ protected def tokens(start: Token, stop: Token) =
+ new Iterator[Token] {
var current = start
- def hasNext() = current != stop && current != null
+ def hasNext = current != stop && current != null
def next() = { val save = current ; current = current.next ; save }
}
- protected def tokens(start : Token) : Iterator[Token] =
+ protected def tokens(start: Token): Iterator[Token] =
tokens(start, null)
- protected def tokens() : Iterator[Token] =
+ protected def tokens() : Iterator[Token] =
tokens(firstToken, null)
private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
- val checkStart = Token.checkStart _
- val checkStop = Token.checkStop _
+ val check_start = Token.check_start _
+ val check_stop = Token.check_stop _
val scan = Token.scan _
if (active == false)
return
var beforeChange =
- if (checkStop(firstToken, _ < start)) scan(firstToken, _.stop >= start)
+ if (check_stop(firstToken, _ < start)) scan(firstToken, _.stop >= start)
else null
var firstRemoved =
if (beforeChange != null) beforeChange.next
- else if (checkStart(firstToken, _ <= start + removedLen)) firstToken
+ else if (check_start(firstToken, _ <= start + removedLen)) firstToken
else null
var lastRemoved = scan(firstRemoved, _.start > start + removedLen)
var shiftToken =
if (lastRemoved != null) lastRemoved
- else if (checkStart(firstToken, _ > start)) firstToken
+ else if (check_start(firstToken, _ > start)) firstToken
else null
while(shiftToken != null) {
@@ -88,13 +88,13 @@
// scan changed tokens until the end of the text or a matching token is
// found which is beyond the changed area
val matchStart = if (beforeChange == null) 0 else beforeChange.stop
- var firstAdded : Token = null
- var lastAdded : Token = null
+ var firstAdded: Token = null
+ var lastAdded: Token = null
- val matcher = tokenPattern.matcher(text.content(matchStart, text.length))
+ val matcher = ProofDocument.token_pattern.matcher(text.content(matchStart, text.length))
var finished = false
var position = 0
- while(matcher.find(position) && ! finished) {
+ while (matcher.find(position) && ! finished) {
position = matcher.end()
val kind = if(isStartKeyword(matcher.group())) {
Token.Kind.COMMAND_START
@@ -108,17 +108,17 @@
if (firstAdded == null)
firstAdded = newToken
else {
- newToken.previous = lastAdded
+ newToken.prev = lastAdded
lastAdded.next = newToken
}
lastAdded = newToken
- while(checkStop(lastRemoved, _ < newToken.stop) &&
+ while (check_stop(lastRemoved, _ < newToken.stop) &&
lastRemoved.next != null)
lastRemoved = lastRemoved.next
if (newToken.stop >= start + addedLen &&
- checkStop(lastRemoved, _ == newToken.stop) )
+ check_stop(lastRemoved, _ == newToken.stop))
finished = true
}
@@ -156,7 +156,7 @@
lastRemoved = null
}
else {
- lastRemoved = lastRemoved.previous
+ lastRemoved = lastRemoved.prev
if (lastRemoved == null)
System.err.println("ERROR")
assert(lastRemoved != null)
@@ -167,7 +167,7 @@
firstAdded = null
}
else
- lastAdded = lastAdded.previous
+ lastAdded = lastAdded.prev
}
if (firstRemoved == null && firstAdded == null)
@@ -180,7 +180,7 @@
else {
// cut removed tokens out of list
if (firstRemoved != null)
- firstRemoved.previous = null
+ firstRemoved.prev = null
if (lastRemoved != null)
lastRemoved.next = null
@@ -198,7 +198,7 @@
// insert new tokens into list
if (firstAdded != null) {
- firstAdded.previous = beforeChange
+ firstAdded.prev = beforeChange
if (beforeChange != null)
beforeChange.next = firstAdded
else
@@ -210,12 +210,12 @@
if (lastAdded != null) {
lastAdded.next = afterChange
if (afterChange != null)
- afterChange.previous = lastAdded
+ afterChange.prev = lastAdded
else
lastToken = lastAdded
}
else if (afterChange != null)
- afterChange.previous = beforeChange
+ afterChange.prev = beforeChange
}
tokenChanged(beforeChange, afterChange, firstRemoved)
--- a/src/Tools/jEdit/src/proofdocument/Token.scala Mon Jan 19 21:04:30 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Mon Jan 19 21:38:50 2009 +0100
@@ -6,8 +6,11 @@
*/
package isabelle.proofdocument
+
+
import isabelle.prover.Command
+
object Token {
object Kind extends Enumeration {
val COMMAND_START = Value("COMMAND_START")
@@ -15,50 +18,43 @@
val OTHER = Value("OTHER")
}
- def checkStart(t : Token, P : (Int) => Boolean)
- = t != null && P(t.start)
+ def check_start(t: Token, P: Int => Boolean) = { t != null && P(t.start) }
+ def check_stop(t: Token, P: Int => Boolean) = { t != null && P(t.stop) }
- def checkStop(t : Token, P : (Int) => Boolean)
- = t != null && P(t.stop)
-
- def scan(s : Token, f : Token => Boolean) : Token = {
+ def scan(s: Token, f: Token => Boolean): Token =
+ {
var current = s
while (current != null) {
val next = current.next
- if (next == null || f(next))
- return current
+ if (next == null || f(next)) return current
current = next
}
return null
}
-
}
-class Token(var start : Int, var stop : Int, var kind : Token.Kind.Value) {
- var next : Token = null
- var previous : Token = null
- var command : Command = null
+class Token(var start: Int, var stop: Int, var kind: Token.Kind.Value)
+{
+ var next: Token = null
+ var prev: Token = null
+ var command: Command = null
def length = stop - start
- def shift(offset : Int, bottomClamp : Int) {
- start = bottomClamp max (start + offset)
- stop = bottomClamp max (stop + offset)
+ def shift(offset: Int, bottom_clamp: Int) {
+ start = bottom_clamp max (start + offset)
+ stop = bottom_clamp max (stop + offset)
}
- override def hashCode() : Int = (31 + start) * 31 + stop
+ override def hashCode: Int = (31 + start) * 31 + stop
- override def equals(obj : Any) : Boolean = {
- if (super.equals(obj))
- return true;
-
- if (null == obj)
- return false;
-
+ override def equals(obj: Any): Boolean =
+ {
+ if (super.equals(obj)) return true
+ if (null == obj) return false
obj match {
- case other: Token =>
- (start == other.start) && (stop == other.stop)
- case other: Any => false
+ case other: Token => (start == other.start) && (stop == other.stop)
+ case other: Any => false
}
}
}
--- a/src/Tools/jEdit/src/prover/Command.scala Mon Jan 19 21:04:30 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Mon Jan 19 21:38:50 2009 +0100
@@ -77,7 +77,7 @@
def content(): String = document.getContent(this)
def next = if (last.next != null) last.next.command else null
- def previous = if (first.previous != null) first.previous.command else null
+ def prev = if (first.prev != null) first.prev.command else null
def start = first.start
def stop = last.stop
@@ -86,7 +86,7 @@
def proper_stop = {
var i = last
while (i != first && i.kind.equals(Token.Kind.COMMENT))
- i = i.previous
+ i = i.prev
i.stop
}
--- a/src/Tools/jEdit/src/prover/Document.scala Mon Jan 19 21:04:30 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala Mon Jan 19 21:38:50 2009 +0100
@@ -63,7 +63,7 @@
before = start.command
}
else
- before = first.previous
+ before = first.prev
}
var addedCommands : List[Command] = Nil
@@ -73,7 +73,7 @@
if (first != null && first.first != removed) {
scan = first.first
if (before == null)
- before = first.previous
+ before = first.prev
}
else if (next != null && next != stop) {
if (next.kind.equals(Token.Kind.COMMAND_START)) {
@@ -85,12 +85,12 @@
removedCommands = first :: removedCommands
scan = first.first
if (before == null)
- before = first.previous
+ before = first.prev
}
else {
scan = first.first
if (before == null)
- before = first.previous
+ before = first.prev
}
}
}
--- a/src/Tools/jEdit/src/prover/Prover.scala Mon Jan 19 21:04:30 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Mon Jan 19 21:38:50 2009 +0100
@@ -182,7 +182,7 @@
val content = isabelle_symbols.encode(document.getContent(cmd))
process.create_command(cmd.id, content)
- process.insert_command(if (cmd.previous == null) "" else cmd.previous.id, cmd.id)
+ process.insert_command(if (cmd.prev == null) "" else cmd.prev.id, cmd.id)
}
def remove(cmd: Command) {