From eec625768fd84cbab756d0f7bff9f02948486a7f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 5 Jun 2014 16:53:44 +0200
Subject: [PATCH] Proper ordering for positions
---
src/main/scala/leon/synthesis/ChooseInfo.scala | 2 +-
src/main/scala/leon/utils/Positions.scala | 15 ++++++++++++---
2 files changed, 13 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index a9e49f10d..f0dd2d242 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -35,6 +35,6 @@ object ChooseInfo {
}
}
- results.sortBy(_.fd.id.toString)
+ results.sortBy(_.source.getPos)
}
}
diff --git a/src/main/scala/leon/utils/Positions.scala b/src/main/scala/leon/utils/Positions.scala
index 1068863b5..f5241de64 100644
--- a/src/main/scala/leon/utils/Positions.scala
+++ b/src/main/scala/leon/utils/Positions.scala
@@ -5,13 +5,22 @@ package utils
import java.io.File
-abstract class Position {
+abstract class Position extends Ordered[Position] {
val line: Int
val col: Int
val file: File
- def < (that: Position) = {
- (this.file == that.file) && (this.line < that.line || this.col < that.col)
+ def compare(that: Position) = {
+ if (this.file == that.file) {
+ val ld = this.line - that.line
+ if (ld == 0) {
+ this.col - that.col
+ } else {
+ ld
+ }
+ } else {
+ 0
+ }
}
def fullString: String
--
GitLab