Introduce a "PowerMode" for the web interface.

Add ?powermode=1 to the URL to access PowerMode. For now, all you can do
is set the flags manually. This allows you to run the synthesis or
termination phases from the web, for instance. Remember, with great
power comes great responsibility!

web/README

@@ -14,7 +14,7 @@ $ source ../setupenv
 ** On laraserver **
 
     $ export LD_LIBRARY_PATH=/localhome/leonweb/git/z3/build/
-    $ play "run -Dapp.prefix=/leon"
+    $ play "start -Dapp.prefix=/leon"
 
 ** Locally **
 

web/app/controllers/Application.scala

@@ -14,10 +14,10 @@ object Application extends Controller {
 
   val examples = VerificationExamples.allExamples ++ SynthesisExamples.allExamples
 
-  def index = Action { implicit request =>
+  def index(powermode : Boolean) = Action { implicit request =>
     val prefix = Play.current.configuration.getString("app.prefix").getOrElse("")
 
-    Ok(views.html.index(examples, VerificationExamples.default, prefix))
+    Ok(views.html.index(examples, VerificationExamples.default, prefix, powermode))
   }
 
   def getExample(id: Int) = Action { 

web/app/models/LeonConsole.scala

@@ -35,6 +35,8 @@ object LeonConsole {
           (event \ "action").as[String] match {
             case "start" =>
               session ! Start((event \ "mode").as[String], (event \ "code").as[String])
+            case "startpower" =>
+              session ! StartPower((event \ "flags").asOpt[String].getOrElse(""), (event \ "code").as[String])
             case "stop" =>
               session ! Stop
             case _ =>
@@ -102,7 +104,9 @@ class ConsoleSession extends Actor {
 
           val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen AnalysisPhase
 
-          pipeline.run(ctx)((code, Nil))
+          val analysisResults = pipeline.run(ctx)((code, Nil))
+
+          log(analysisResults.summaryString)
 
           event("stopped")
 
@@ -123,6 +127,30 @@ class ConsoleSession extends Actor {
           error("Invalid request mode: "+mode)
       }
 
+    case StartPower(flags, code) =>
+      val classPath = Play.current.configuration.getString("app.classpath").map(_.split(":").toList).getOrElse(Settings.defaultClassPath())
+
+      event("started")
+      isStarted = true
+
+      log(""">     ____                          __  __           _        _ 
+             > __ |  _ \ _____      _____ _ __  |  \/  | ___   __| | ___  | | __
+             > __ | |_) / _ \ \ /\ / / _ \ '__| | |\/| |/ _ \ / _` |/ _ \ | | __
+             > __ |  __/ (_) \ V  V /  __/ |    | |  | | (_) | (_| |  __/ |_| __
+             >    |_|   \___/ \_/\_/ \___|_|    |_|  |_|\___/ \__,_|\___| (_)""".stripMargin('>'))
+
+      var ctx = leon.Main.processOptions(reporter, flags.split(" ").filterNot(_.isEmpty).toList)
+      ctx = ctx.copy(settings = ctx.settings.copy(classPath = classPath))
+
+      val pipeline = TemporaryInputPhase andThen leon.Main.computePipeline(ctx.settings)
+
+      pipeline.run(ctx)((code, Nil)) match {
+        case report: leon.verification.VerificationReport => log(report.summaryString)
+        case report: leon.termination.TerminationReport   => log(report.summaryString)
+        case _ => 
+      }
+
+      event("stopped")
 
     case Stop =>
       isStarted = false
@@ -140,6 +168,7 @@ object ConsoleProtocol {
 
 
   case class Start(mode: String, code: String)
+  case class StartPower(flags : String, code : String)
 
   case object Stop
 

web/app/views/index.scala.html

-@(exs: List[examples.Example], default: examples.Example, prefix: String)(implicit request: RequestHeader)
+@(exs: List[examples.Example], default: examples.Example, prefix: String, powermode : Boolean)(implicit request: RequestHeader)
 
 @main("Leon Online", prefix) {
   <div id="allcontent">
@@ -12,8 +12,13 @@
     <div id="leonmain" class="contentbox">
       <form id="leoninput" method="POST" action="">
         <div id="codecolumn">
-          <div id="codebox">@default.code</div>
-          <input type="submit" id="askbutton" value="Ask Leon !">
+            <div id="codebox">@default.code</div>
+            <div id="subcodebox">
+                @if(powermode) {
+                  <input type="text" id="powerflags" value="--timeout=2" placeholder="add any flags here">
+                }
+                <input type="submit" id="askbutton" value="Run Leon !">
+            </div>
           <div><textarea id="consolebox"></textarea></div>
         </div>
         <div id="selectcolumn">
@@ -51,16 +56,24 @@
                 }
             }
 
-            leonSocket.onmessage = receiveEvent
+            leonSocket.onmessage = receiveEvent;
 
-            var leonStatus = "stopped"
+            var leonStatus = "stopped";
 
             $("#leoninput").submit(function () {
+                $("#consolebox").val("");
+
+                @if(!powermode) {
                 var msg = JSON.stringify(
                   {action: "start", mode: $("#leon-mode").val(), code: editor.getValue()}
-                )
+                );
+                } else {
+                var msg = JSON.stringify(
+                  {action: "startpower", flags: $("#powerflags").val(), code: editor.getValue()}
+                );
+                }
 
-                leonSocket.send(msg)
+                leonSocket.send(msg);
                 return false;
             });
         });

web/conf/routes

@@ -3,7 +3,7 @@
 # ~~~~
 
 # Home page
-GET     /                        leon.web.controllers.Application.index
+GET     /                        leon.web.controllers.Application.index(powermode : Boolean ?= false)
 
 GET     /ajax/getExample/:id     leon.web.controllers.Application.getExample(id: Int)
 GET     /openConsole             leon.web.controllers.Application.openConsole

web/public/stylesheets/leon.css

@@ -130,8 +130,18 @@ li {
     margin-bottom: 5px;
 }
 
+#subcodebox {
+    margin: 460px 0px 0px 0px;
+}
+
+#powerflags {
+    margin: 0px 0px 5px 0px;
+    border: 1px solid #666666;
+    width: 700px;
+}
+
 #askbutton {
-    margin: 460px 0px 5px 0px;
+    margin: 0px 0px 5px 0px;
     background-color: transparent;
     border: 1px solid #666666;
     width: 700px;