eliminated explicit method equals, which is always behind == / != anyway in Scala;
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Mon Jan 19 21:38:50 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala Mon Jan 19 21:58:38 2009 +0100
@@ -75,11 +75,11 @@
val list = new java.util.LinkedList[String]
val descriptions = new java.util.LinkedList[String]
// compute suggestions
- val (suggs,text) = suggestions(1)
+ val (suggs, text) = suggestions(1)
for(s <- suggs) {
val decoded = Isabelle.symbols.decode(s)
list.add(decoded)
- if(!decoded.equals(s)) descriptions.add(s) else descriptions.add(null)
+ if(decoded != s) descriptions.add(s) else descriptions.add(null)
}
return new IsabelleSideKickCompletion(pane.getView, text, list, descriptions)
} else return null
--- a/src/Tools/jEdit/src/prover/Command.scala Mon Jan 19 21:38:50 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala Mon Jan 19 21:58:38 2009 +0100
@@ -85,7 +85,7 @@
def proper_start = start
def proper_stop = {
var i = last
- while (i != first && i.kind.equals(Token.Kind.COMMENT))
+ while (i != first && i.kind == Token.Kind.COMMENT)
i = i.prev
i.stop
}
--- a/src/Tools/jEdit/src/prover/Document.scala Mon Jan 19 21:38:50 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala Mon Jan 19 21:58:38 2009 +0100
@@ -76,7 +76,7 @@
before = first.prev
}
else if (next != null && next != stop) {
- if (next.kind.equals(Token.Kind.COMMAND_START)) {
+ if (next.kind == Token.Kind.COMMAND_START) {
before = start.command
scan = next
}
@@ -115,14 +115,14 @@
var finished = false
while (scan != null && !finished) {
if (scan == stopScan) {
- if (scan.kind.equals(Token.Kind.COMMAND_START))
+ if (scan.kind == Token.Kind.COMMAND_START)
finished = true
else
overrun = true
}
- if (scan.kind.equals(Token.Kind.COMMAND_START) && cmdStart != null && !finished) {
- if (! overrun) {
+ if (scan.kind == Token.Kind.COMMAND_START && cmdStart != null && !finished) {
+ if (!overrun) {
addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
cmdStart = scan
cmdStop = scan
@@ -130,7 +130,7 @@
else
finished = true
}
- else if (! finished) {
+ else if (!finished) {
if (cmdStart == null)
cmdStart = scan
cmdStop = scan