From ac08433ead2e2998cdfe184c7ab3d967e56c9600 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 25 Oct 2012 17:42:21 +0200
Subject: [PATCH] No need for this anymore

---
 src/main/scala/leon/LeonPhase.scala           |  4 +-
 src/main/scala/leon/Main.scala                | 22 ++++-----
 src/main/scala/leon/Pipeline.scala            |  2 -
 .../scala/leon/synthesis/SynthesisPhase.scala | 45 ++-----------------
 4 files changed, 17 insertions(+), 56 deletions(-)

diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index 9130639d5..d81b8eea7 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -34,8 +34,8 @@ case class NoopPhase[T]() extends LeonPhase[T, T] {
   override def run(ctx: LeonContext)(v: T) = v
 }
 
-case class ExitPhase[T]() extends LeonPhase[T, PipelineControl] {
+case class ExitPhase[T]() extends LeonPhase[T, Unit] {
   val name = "end";
   val description = "end"
-  override def run(ctx: LeonContext)(v: T) = PipelineControl(restart = false)
+  override def run(ctx: LeonContext)(v: T) = ()
 }
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index c2ea3d878..e52ea1ccf 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -92,7 +92,7 @@ object Main {
 
   implicit def phaseToPipeline[F, T](phase: LeonPhase[F, T]): Pipeline[F, T] = new PipeCons(phase, new PipeNil())
 
-  def computePipeline(settings: Settings): Pipeline[List[String], PipelineControl] = {
+  def computePipeline(settings: Settings): Pipeline[List[String], Unit] = {
     import purescala.Definitions.Program
 
     val pipeBegin = phaseToPipeline(plugin.ExtractionPhase)
@@ -107,10 +107,15 @@ object Main {
         NoopPhase[Program]()
       }
 
-    val pipeAction: Pipeline[Program, PipelineControl]=
+    val pipeSynthesis: Pipeline[Program, Program]=
       if (settings.synthesis) {
         synthesis.SynthesisPhase
-      } else if (settings.analyze) {
+      } else {
+        NoopPhase[Program]()
+      }
+
+    val pipeAnalysis: Pipeline[Program, Unit] =
+      if (settings.analyze) {
         AnalysisPhase andThen
         ExitPhase[Program]()
       } else {
@@ -119,7 +124,8 @@ object Main {
 
     pipeBegin followedBy
     pipeTransforms followedBy
-    pipeAction
+    pipeSynthesis followedBy
+    pipeAnalysis
   }
 
   def main(args : Array[String]) {
@@ -131,11 +137,7 @@ object Main {
     // Compute leon pipeline
     val pipeline = computePipeline(ctx.settings)
 
-    var exec = PipelineControl()
-    do {
-      exec = pipeline.run(ctx)(args.toList)
-    } while(exec.restart)
-
-    sys.exit(exec.exitcode)
+    // Run pipeline
+    pipeline.run(ctx)(args.toList)
   }
 }
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index ce2677d41..477a08c31 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -24,5 +24,3 @@ class PipeNil[T]() extends Pipeline[T,T] {
     "|"
   }
 }
-
-case class PipelineControl(exitcode: Int = 0, restart: Boolean = false)
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index b21f87ae3..62e004d22 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -3,11 +3,11 @@ package synthesis
 
 import purescala.Definitions.Program
 
-object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
+object SynthesisPhase extends LeonPhase[Program, Program] {
   val name        = "Synthesis"
   val description = "Synthesis"
 
-  def run(ctx: LeonContext)(p: Program): PipelineControl = {
+  def run(ctx: LeonContext)(p: Program): Program = {
     val quietReporter = new QuietReporter
     val solvers  = List(
       new TrivialSolver(quietReporter),
@@ -17,46 +17,7 @@ object SynthesisPhase extends LeonPhase[Program, PipelineControl] {
     val synth = new Synthesizer(ctx.reporter, solvers)
     val solutions = synth.synthesizeAll(p)
 
-    detectEditor match {
-      case Some(program) => 
-        openEditor(program, "/home/ekneuss/plop")
-        PipelineControl(restart = false)
-      case None =>
-        ctx.reporter.fatalError("Cannot open editor, $EDITOR / $VISUAL missing")
-        PipelineControl(restart = false)
-    }
+    p
   }
 
-  def detectEditor: Option[String] = {
-    Option(System.getenv("EDITOR")) orElse Option(System.getenv("VISUAL"))
-  }
-
-  def openEditor(program: String, path: String) {
-    val proc = Runtime.getRuntime().exec(program+" "+path)
-
-    val errGobbler = new StreamGobbler(proc.getErrorStream(), System.err)
-    val outGobbler = new StreamGobbler(proc.getInputStream(), System.out)
-    val inGobbler  = new StreamGobbler(System.in, proc.getOutputStream())
-
-    errGobbler.start()
-    outGobbler.start()
-    inGobbler.start()
-
-    proc.waitFor()
-    errGobbler.join()
-    outGobbler.join()
-  }
-
-  import java.io.{InputStream, OutputStream}
-  class StreamGobbler(is: InputStream, os: OutputStream) extends Thread {
-    override def run() {
-      var c: Int = is.read()
-      while(c != 1) {
-        os.write(c);
-        os.flush();
-
-        c = is.read()
-      }
-    }
-  }
 }
-- 
GitLab