# HG changeset patch # User wenzelm # Date 1232397530 -3600 # Node ID 0923926022d755d667d760fde0c092920cbaaecb # Parent 0f4b34445f40b4c183e1b60866c41ab467ce4115 superficial tuning; diff -r 0f4b34445f40 -r 0923926022d7 src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- 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) diff -r 0f4b34445f40 -r 0923926022d7 src/Tools/jEdit/src/proofdocument/Token.scala --- 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 } } } diff -r 0f4b34445f40 -r 0923926022d7 src/Tools/jEdit/src/prover/Command.scala --- 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 } diff -r 0f4b34445f40 -r 0923926022d7 src/Tools/jEdit/src/prover/Document.scala --- 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 } } } diff -r 0f4b34445f40 -r 0923926022d7 src/Tools/jEdit/src/prover/Prover.scala --- 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) {