From 971da4cd49f9b7ca1e3ee880e17050dfeee1bb3c Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 26 Aug 2013 16:39:44 +0200
Subject: [PATCH] Terminate more gracefully when manual serach is interrupted
---
src/main/scala/leon/synthesis/ManualSearch.scala | 15 ++++++++++++++-
1 file changed, 14 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/ManualSearch.scala b/src/main/scala/leon/synthesis/ManualSearch.scala
index b64a83403..8e74793d6 100644
--- a/src/main/scala/leon/synthesis/ManualSearch.scala
+++ b/src/main/scala/leon/synthesis/ManualSearch.scala
@@ -84,6 +84,14 @@ class ManualSearch(synth: Synthesizer,
println("-"*80)
}
+ override def stop() {
+ super.stop()
+ cmdQueue = "q" :: Nil
+ continue = false
+ }
+
+ var continue = true
+
override def nextLeaf(): Option[g.Leaf] = {
g.tree match {
@@ -92,7 +100,7 @@ class ManualSearch(synth: Synthesizer,
case _ =>
var res: Option[g.Leaf] = None
- var continue = true
+ continue = true
while(continue) {
printGraph()
@@ -157,6 +165,11 @@ class ManualSearch(synth: Synthesizer,
}
}
} catch {
+ case e: java.lang.NumberFormatException =>
+
+ case e: java.io.IOException =>
+ continue = false
+
case e: Throwable =>
error("Woops: "+e.getMessage())
e.printStackTrace()
--
GitLab