diff --git a/web/app/controllers/Application.scala b/web/app/controllers/Application.scala
index 3d16ab315d8b267ced021d5f9a4078b2ed24dffd..dbff3fa47832c96343da12872e4b5460af15a600 100644
--- a/web/app/controllers/Application.scala
+++ b/web/app/controllers/Application.scala
@@ -1,3 +1,4 @@
+package leon.web
package controllers
import play.api._
@@ -7,12 +8,13 @@ import play.api.libs.json.Json._
import play.api.libs.json.Writes._
import examples._
+import models.LeonConsole
object Application extends Controller {
val examples = VerificationExamples.allExamples
- def index = Action {
+ def index = Action { implicit request =>
Ok(views.html.index(examples, VerificationExamples.default))
}
@@ -25,4 +27,8 @@ object Application extends Controller {
}
}
+ def openConsole() = WebSocket.async[JsValue] { request =>
+ LeonConsole.open
+ }
+
}
diff --git a/web/app/models/LeonConsole.scala b/web/app/models/LeonConsole.scala
new file mode 100644
index 0000000000000000000000000000000000000000..76ef94140165f917db1a37c4320acb8f5bf64f0e
--- /dev/null
+++ b/web/app/models/LeonConsole.scala
@@ -0,0 +1,161 @@
+package leon.web
+package models
+
+import akka.actor._
+import akka.util.duration._
+
+import play.api._
+import play.api.libs.json._
+import play.api.libs.iteratee._
+import play.api.libs.concurrent._
+import play.api.libs.json.Json._
+import play.api.libs.json.Writes._
+
+import akka.util.Timeout
+import akka.pattern.ask
+
+import play.api.Play.current
+
+import leon.{LeonContext, Settings, Reporter}
+import leon.plugin.{TemporaryInputPhase, ExtractionPhase}
+import leon.verification.AnalysisPhase
+
+
+object LeonConsole {
+ def open: Promise[(Iteratee[JsValue,_],Enumerator[JsValue])] = {
+ import ConsoleProtocol._
+
+ val session = Akka.system.actorOf(Props[ConsoleSession])
+ implicit val timeout = Timeout(1.seconds)
+
+ (session ? Init).asPromise.map {
+ case InitSuccess(enumerator) =>
+ // Create an Iteratee to consume the feed
+ val iteratee = Iteratee.foreach[JsValue] { event =>
+ (event \ "action").as[String] match {
+ case "start" =>
+ session ! Start((event \ "mode").as[String], (event \ "code").as[String])
+ case "stop" =>
+ session ! Stop
+ case _ =>
+ }
+ }.mapDone { _ =>
+ session ! Quit
+ }
+
+ (iteratee,enumerator)
+
+ case InitFailure(error: String) =>
+ // Connection error
+
+ // A finished Iteratee sending EOF
+ val iteratee = Done[JsValue,Unit]((),Input.EOF)
+
+ // Send an error and close the socket
+ val enumerator = Enumerator[JsValue](toJson(
+ Map("kind" -> "error", "message" -> error)
+ )).andThen(Enumerator.enumInput(Input.EOF))
+
+ (iteratee,enumerator)
+ }
+ }
+}
+
+class ConsoleSession extends Actor {
+ import ConsoleProtocol._
+
+ var isStarted = false
+ var channel: PushEnumerator[JsValue] = _
+ var reporter: WSReporter = _
+
+ def log(msg: String) = {
+ channel.push(toJson(Map("kind" -> "log", "message" -> msg)))
+ }
+
+ def error(msg: String) = {
+ channel.push(toJson(Map("kind" -> "error", "message" -> msg)))
+ }
+
+ def event(kind: String) = {
+ channel.push(toJson(Map("kind" -> "event", "event" -> kind)))
+ }
+
+ def receive = {
+ case Init =>
+ channel = Enumerator.imperative[JsValue]()
+ reporter = WSReporter(channel)
+ sender ! InitSuccess(channel)
+
+ case Start(mode, code) =>
+ log("Welcome to LeonOnline!")
+ log("Processing request...")
+
+
+ mode match {
+ case "verification" =>
+ event("started")
+ isStarted = true
+
+ val ctx = LeonContext(
+ settings = Settings(
+ synthesis = false,
+ xlang = false,
+ verify = true
+ ),
+ files = Nil,
+ reporter = new WSReporter(channel)
+ )
+
+ val pipeline = TemporaryInputPhase andThen ExtractionPhase andThen AnalysisPhase
+
+ pipeline.run(ctx)((code, "--timeout=2" :: Nil))
+
+ case "synthesis" =>
+ event("started")
+ isStarted = true
+
+ case _ =>
+ error("Invalid request mode: "+mode)
+ }
+
+
+ case Stop =>
+ isStarted = false
+
+ event("stopped")
+ case Quit =>
+
+ }
+}
+
+object ConsoleProtocol {
+ case object Init
+ case class InitSuccess(enum: Enumerator[JsValue])
+ case class InitFailure(error: String)
+
+
+ case class Start(mode: String, code: String)
+
+ case object Stop
+
+ case object Quit
+}
+
+case class WSReporter(channel: PushEnumerator[JsValue]) extends Reporter {
+ def infoFunction(msg: Any) : Unit = {
+ channel.push(toJson(Map("kind" -> "log", "message" -> (msg.toString))))
+ }
+
+ def warningFunction(msg: Any) : Unit = {
+ channel.push(toJson(Map("kind" -> "log", "message" -> ("Warning: "+msg.toString))))
+ }
+
+ def errorFunction(msg: Any) : Unit = {
+ channel.push(toJson(Map("kind" -> "log", "message" -> ("Error: "+msg.toString))))
+ }
+
+ def fatalErrorFunction(msg: Any) : Nothing = {
+ sys.error("FATAL: "+msg)
+ }
+}
+
diff --git a/web/app/views/index.scala.html b/web/app/views/index.scala.html
index cc8688d98aa889189bce0107c2b3e8f1f49e112b..09e192c5e9ca3f183f9001ffbeb5c271d6803dc6 100644
--- a/web/app/views/index.scala.html
+++ b/web/app/views/index.scala.html
@@ -1,4 +1,4 @@
-@(exs: List[examples.Example], default: examples.Example)
+@(exs: List[examples.Example], default: examples.Example)(implicit request: RequestHeader)
@main("Leon Online") {
<div id="allcontent">
@@ -27,6 +27,43 @@
</select>
</div>
</form>
+ <script>
+ $(document).ready(function() {
+ var WS = window['MozWebSocket'] ? MozWebSocket : WebSocket
+ var leonSocket = new WS("@leon.web.controllers.routes.Application.openConsole().webSocketURL()")
+
+ var sendMessage = function() {
+ }
+
+ var receiveEvent = function(event) {
+ var data = JSON.parse(event.data)
+ if (data.kind == "error") {
+ alert(data.message);
+ } else if (data.kind == "log") {
+ $("#consolebox").val($("#consolebox").val()+"\n"+data.message);
+ } else if (data.kind == "event") {
+ if (data.event == "started") {
+ $("#askbutton").val("... processing ...")
+ } else if (data.event == "stopped") {
+ $("#askbutton").val("Ask Leon!")
+ }
+ }
+ }
+
+ leonSocket.onmessage = receiveEvent
+
+ var leonStatus = "stopped"
+
+ $("#leoninput").submit(function () {
+ var msg = JSON.stringify(
+ {action: "start", mode: "verification", code: editor.getValue()}
+ )
+
+ leonSocket.send(msg)
+ return false;
+ });
+ });
+ </script>
</div>
</div>
}
diff --git a/web/conf/routes b/web/conf/routes
index 99e563d06079d86c15f62164e11c74c55392dfec..38891796ce33ffa79c2251b73ceef644ce2fc2dc 100644
--- a/web/conf/routes
+++ b/web/conf/routes
@@ -3,9 +3,10 @@
# ~~~~
# Home page
-GET / controllers.Application.index
+GET / leon.web.controllers.Application.index
-GET /ajax/getExample/:id controllers.Application.getExample(id: Int)
+GET /ajax/getExample/:id leon.web.controllers.Application.getExample(id: Int)
+GET /openConsole leon.web.controllers.Application.openConsole
# Map static resources from the /public folder to the /assets URL path
GET /assets/*file controllers.Assets.at(path="/public", file)
diff --git a/web/lib/leon_2.9.2-2.0.jar b/web/lib/leon_2.9.2-2.0.jar
new file mode 120000
index 0000000000000000000000000000000000000000..b9d4360f109610c3db80dba7a6c4d3e1747f6981
--- /dev/null
+++ b/web/lib/leon_2.9.2-2.0.jar
@@ -0,0 +1 @@
+../../target/scala-2.9.2/leon_2.9.2-2.0.jar
\ No newline at end of file
diff --git a/web/public/javascripts/leon.js b/web/public/javascripts/leon.js
index 765aa2ade4b9ecf1fd8fe43f1fdaa35f0904114d..eaeea4e508e80c4b23568f9a3324c449c0001721 100644
--- a/web/public/javascripts/leon.js
+++ b/web/public/javascripts/leon.js
@@ -32,9 +32,5 @@ $(document).ready(function() {
editor.getSession().setMode("ace/mode/scala");
editor.getSession().setUseWrapMode(true);
- $("#leoninput").submit(function () {
-
- return false;
- });
});