From 7645771ee50d903a8ad5e519300689d92d78161c Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Thu, 17 Sep 2015 15:36:56 +0200 Subject: [PATCH] Make Printing a little more forgiving --- src/main/scala/leon/purescala/DefOps.scala | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala index 7a7c6b632..89c0fce81 100644 --- a/src/main/scala/leon/purescala/DefOps.scala +++ b/src/main/scala/leon/purescala/DefOps.scala @@ -91,18 +91,21 @@ object DefOps { val namesFrom = pathToNames(pathFrom, useUniqueIds) val namesOf = pathToNames(pathFromRoot(of), useUniqueIds) - def stripPrefix(of: List[String], from: List[String]) = { - val commonPrefix = (of zip from).takeWhile(p => p._1 == p._2) + def stripPrefix(off: List[String], from: List[String]) = { + val commonPrefix = (off zip from).takeWhile(p => p._1 == p._2) - val res = of.drop(commonPrefix.size) + val res = off.drop(commonPrefix.size) if (res.isEmpty) { - List(of.last) + if (off.isEmpty) List() + else List(off.last) } else { res } } + val sp = stripPrefix(namesOf, namesFrom) + if (sp.isEmpty) return "**** " + of.id.uniqueName var names: Set[List[String]] = Set(namesOf, stripPrefix(namesOf, namesFrom)) pathFrom match { -- GitLab