# HG changeset patch
# User wenzelm
# Date 1232398718 -3600
# Node ID 920ff05ca3f348dd9c67d545f4a7c15aa888c03f
# Parent  0923926022d755d667d760fde0c092920cbaaecb
eliminated explicit method equals, which is always behind == / != anyway in Scala;

diff -r 0923926022d7 -r 920ff05ca3f3 src/Tools/jEdit/src/jedit/IsabelleSideKickParser.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
diff -r 0923926022d7 -r 920ff05ca3f3 src/Tools/jEdit/src/prover/Command.scala
--- 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
   }
diff -r 0923926022d7 -r 920ff05ca3f3 src/Tools/jEdit/src/prover/Document.scala
--- 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