# HG changeset patch # User wenzelm # Date 1232487054 -3600 # Node ID 47f9303db81db64394d93124761cddbd57557c0b # Parent 0ffbc5ce96545134879c47e6dd7becbfa8d9ff18 misc tuning -- de-camelization; diff -r 0ffbc5ce9654 -r 47f9303db81d src/Tools/jEdit/src/proofdocument/ProofDocument.scala --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jan 20 22:29:56 2009 +0100 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Tue Jan 20 22:30:54 2009 +0100 @@ -12,10 +12,10 @@ import isabelle.prover.{Prover, Command} -class StructureChange( - val beforeChange: Command, - val addedCommands: List[Command], - val removedCommands: List[Command]) +case class StructureChange( + val before_change: Command, + val added_commands: List[Command], + val removed_commands: List[Command]) object ProofDocument { @@ -53,174 +53,174 @@ /** token view **/ - protected var firstToken: Token = null - protected var lastToken: Token = null + private var first_token: Token = null + private var last_token: Token = null - protected def tokens(start: Token, stop: Token) = new Iterator[Token] { + private def tokens(start: Token, stop: Token) = new Iterator[Token] { var current = start def hasNext = current != stop && current != null - def next() = { val save = current ; current = current.next ; save } + def next() = { val save = current; current = current.next; save } } - protected def tokens(start: Token): Iterator[Token] = tokens(start, null) - protected def tokens() : Iterator[Token] = tokens(firstToken, null) + private def tokens(start: Token): Iterator[Token] = tokens(start, null) + private def tokens(): Iterator[Token] = tokens(first_token, null) - private def text_changed(start: Int, addedLen: Int, removedLen: Int) + private def text_changed(start: Int, added_len: Int, removed_len: Int) { if (!active) return - var beforeChange = - if (Token.check_stop(firstToken, _ < start)) Token.scan(firstToken, _.stop >= start) + var before_change = + if (Token.check_stop(first_token, _ < start)) Token.scan(first_token, _.stop >= start) else null - var firstRemoved = - if (beforeChange != null) beforeChange.next - else if (Token.check_start(firstToken, _ <= start + removedLen)) firstToken + var first_removed = + if (before_change != null) before_change.next + else if (Token.check_start(first_token, _ <= start + removed_len)) first_token else null - var lastRemoved = Token.scan(firstRemoved, _.start > start + removedLen) + var last_removed = Token.scan(first_removed, _.start > start + removed_len) - var shiftToken = - if (lastRemoved != null) lastRemoved - else if (Token.check_start(firstToken, _ > start)) firstToken + var shift_token = + if (last_removed != null) last_removed + else if (Token.check_start(first_token, _ > start)) first_token else null - while (shiftToken != null) { - shiftToken.shift(addedLen - removedLen, start) - shiftToken = shiftToken.next + while (shift_token != null) { + shift_token.shift(added_len - removed_len, start) + shift_token = shift_token.next } // 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 + val match_start = if (before_change == null) 0 else before_change.stop + var first_added: Token = null + var last_added: Token = null - val matcher = ProofDocument.token_pattern.matcher(text.content(matchStart, text.length)) + val matcher = ProofDocument.token_pattern.matcher(text.content(match_start, text.length)) var finished = false var position = 0 - while (matcher.find(position) && ! finished) { - position = matcher.end() + while (matcher.find(position) && !finished) { + position = matcher.end val kind = - if (prover.is_command_keyword(matcher.group())) + if (prover.is_command_keyword(matcher.group)) Token.Kind.COMMAND_START - else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*") + else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*") Token.Kind.COMMENT else Token.Kind.OTHER - val newToken = new Token(matcher.start() + matchStart, matcher.end() + matchStart, kind) + val new_token = new Token(matcher.start + match_start, matcher.end + match_start, kind) - if (firstAdded == null) - firstAdded = newToken + if (first_added == null) + first_added = new_token else { - newToken.prev = lastAdded - lastAdded.next = newToken + new_token.prev = last_added + last_added.next = new_token } - lastAdded = newToken + last_added = new_token - while (Token.check_stop(lastRemoved, _ < newToken.stop) && - lastRemoved.next != null) - lastRemoved = lastRemoved.next + while (Token.check_stop(last_removed, _ < new_token.stop) && + last_removed.next != null) + last_removed = last_removed.next - if (newToken.stop >= start + addedLen && - Token.check_stop(lastRemoved, _ == newToken.stop)) + if (new_token.stop >= start + added_len && + Token.check_stop(last_removed, _ == new_token.stop)) finished = true } - var afterChange = if (lastRemoved != null) lastRemoved.next else null + var after_change = if (last_removed != null) last_removed.next else null // remove superflous first token-change - if (firstAdded != null && firstAdded == firstRemoved && - firstAdded.stop < start) { - beforeChange = firstRemoved - if (lastRemoved == firstRemoved) { - lastRemoved = null - firstRemoved = null + if (first_added != null && first_added == first_removed && + first_added.stop < start) { + before_change = first_removed + if (last_removed == first_removed) { + last_removed = null + first_removed = null } else { - firstRemoved = firstRemoved.next - assert(firstRemoved != null) + first_removed = first_removed.next + assert(first_removed != null) } - if (lastAdded == firstAdded) { - lastAdded = null - firstAdded = null + if (last_added == first_added) { + last_added = null + first_added = null } - if (firstAdded != null) - firstAdded = firstAdded.next + if (first_added != null) + first_added = first_added.next } // remove superflous last token-change - if (lastAdded != null && lastAdded == lastRemoved && - lastAdded.start > start + addedLen) { - afterChange = lastRemoved - if (firstRemoved == lastRemoved) { - firstRemoved = null - lastRemoved = null + if (last_added != null && last_added == last_removed && + last_added.start > start + added_len) { + after_change = last_removed + if (first_removed == last_removed) { + first_removed = null + last_removed = null } else { - lastRemoved = lastRemoved.prev - assert(lastRemoved != null) + last_removed = last_removed.prev + assert(last_removed != null) } - if (lastAdded == firstAdded) { - lastAdded = null - firstAdded = null + if (last_added == first_added) { + last_added = null + first_added = null } else - lastAdded = lastAdded.prev + last_added = last_added.prev } - if (firstRemoved == null && firstAdded == null) + if (first_removed == null && first_added == null) return - if (firstToken == null) { - firstToken = firstAdded - lastToken = lastAdded + if (first_token == null) { + first_token = first_added + last_token = last_added } else { // cut removed tokens out of list - if (firstRemoved != null) - firstRemoved.prev = null - if (lastRemoved != null) - lastRemoved.next = null + if (first_removed != null) + first_removed.prev = null + if (last_removed != null) + last_removed.next = null - if (firstToken == firstRemoved) - if (firstAdded != null) - firstToken = firstAdded + if (first_token == first_removed) + if (first_added != null) + first_token = first_added else - firstToken = afterChange + first_token = after_change - if (lastToken == lastRemoved) - if (lastAdded != null) - lastToken = lastAdded + if (last_token == last_removed) + if (last_added != null) + last_token = last_added else - lastToken = beforeChange + last_token = before_change // insert new tokens into list - if (firstAdded != null) { - firstAdded.prev = beforeChange - if (beforeChange != null) - beforeChange.next = firstAdded + if (first_added != null) { + first_added.prev = before_change + if (before_change != null) + before_change.next = first_added else - firstToken = firstAdded + first_token = first_added } - else if (beforeChange != null) - beforeChange.next = afterChange + else if (before_change != null) + before_change.next = after_change - if (lastAdded != null) { - lastAdded.next = afterChange - if (afterChange != null) - afterChange.prev = lastAdded + if (last_added != null) { + last_added.next = after_change + if (after_change != null) + after_change.prev = last_added else - lastToken = lastAdded + last_token = last_added } - else if (afterChange != null) - afterChange.prev = beforeChange + else if (after_change != null) + after_change.prev = before_change } - token_changed(beforeChange, afterChange, firstRemoved) + token_changed(before_change, after_change, first_removed) } @@ -230,7 +230,7 @@ val structural_changes = new EventBus[StructureChange] def commands = new Iterator[Command] { - var current = firstToken + var current = first_token def hasNext = current != null def next() = { val s = current.command ; current = s.last.next ; s } } @@ -242,7 +242,7 @@ private def token_changed(start: Token, stop: Token, removed: Token) { - var removedCommands: List[Command] = Nil + var removed_commands: List[Command] = Nil var first: Command = null var last: Command = null @@ -250,12 +250,12 @@ if (first == null) first = t.command if (t.command != last) - removedCommands = t.command :: removedCommands + removed_commands = t.command :: removed_commands last = t.command } var before: Command = null - if (!removedCommands.isEmpty) { + if (!removed_commands.isEmpty) { if (first.first == removed) { if (start == null) before = null @@ -266,7 +266,7 @@ before = first.prev } - var addedCommands: List[Command] = Nil + var added_commands: List[Command] = Nil var scan: Token = null if (start != null) { val next = start.next @@ -282,7 +282,7 @@ } else if (first == null || first.first == removed) { first = start.command - removedCommands = first :: removedCommands + removed_commands = first :: removed_commands scan = first.first if (before == null) before = first.prev @@ -295,7 +295,7 @@ } } else - scan = firstToken + scan = first_token var stopScan: Token = null if (stop != null) { @@ -323,7 +323,7 @@ if (scan.kind == Token.Kind.COMMAND_START && cmdStart != null && !finished) { if (!overrun) { - addedCommands = new Command(text, cmdStart, cmdStop) :: addedCommands + added_commands = new Command(text, cmdStart, cmdStop) :: added_commands cmdStart = scan cmdStop = scan } @@ -337,7 +337,7 @@ } if (overrun && !finished) { if (scan.command != last) - removedCommands = scan.command :: removedCommands + removed_commands = scan.command :: removed_commands last = scan.command } @@ -346,12 +346,12 @@ } if (cmdStart != null) - addedCommands = new Command(text, cmdStart, cmdStop) :: addedCommands + added_commands = new Command(text, cmdStart, cmdStop) :: added_commands // relink commands - addedCommands = addedCommands.reverse - removedCommands = removedCommands.reverse + added_commands = added_commands.reverse + removed_commands = removed_commands.reverse - structural_changes.event(new StructureChange(before, addedCommands, removedCommands)) + structural_changes.event(new StructureChange(before, added_commands, removed_commands)) } } diff -r 0ffbc5ce9654 -r 47f9303db81d src/Tools/jEdit/src/prover/Prover.scala --- a/src/Tools/jEdit/src/prover/Prover.scala Tue Jan 20 22:29:56 2009 +0100 +++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Jan 20 22:30:54 2009 +0100 @@ -183,8 +183,8 @@ process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path)) document.structural_changes += (changes => { - for (cmd <- changes.removedCommands) remove(cmd) - for (cmd <- changes.addedCommands) send(cmd) + for (cmd <- changes.removed_commands) remove(cmd) + for (cmd <- changes.added_commands) send(cmd) }) if (initialized) { document.activate()