From 0a061a12fca96e7e3f1bd66f48db5780a98eecb4 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 11 Dec 2012 17:15:15 +0100
Subject: [PATCH] websocket URL no longer needed
---
web/README | 7 +++++++
web/app/controllers/Application.scala | 3 +--
web/app/models/LeonConsole.scala | 2 ++
web/app/views/index.scala.html | 11 +++++++----
web/conf/application.conf | 5 +----
web/public/javascripts/leon.js | 4 ++--
6 files changed, 20 insertions(+), 12 deletions(-)
create mode 100644 web/README
diff --git a/web/README b/web/README
new file mode 100644
index 000000000..fc63a7c7b
--- /dev/null
+++ b/web/README
@@ -0,0 +1,7 @@
+## HOWTO RUN LEON ONLINE
+
+1) go to leon-2.0 main directory
+2) sbt package
+3) cd web
+4) export LD_LIBRARY_PATH=../lib-bin/64
+4) play run
diff --git a/web/app/controllers/Application.scala b/web/app/controllers/Application.scala
index ccec9b1ad..1d2269a49 100644
--- a/web/app/controllers/Application.scala
+++ b/web/app/controllers/Application.scala
@@ -16,9 +16,8 @@ object Application extends Controller {
def index = Action { implicit request =>
val prefix = Play.current.configuration.getString("app.prefix").getOrElse("")
- val wsURL = Play.current.configuration.getString("app.wsURL").getOrElse(routes.Application.openConsole().webSocketURL())
- Ok(views.html.index(examples, VerificationExamples.default, prefix, wsURL))
+ Ok(views.html.index(examples, VerificationExamples.default, prefix))
}
def getExample(id: Int) = Action {
diff --git a/web/app/models/LeonConsole.scala b/web/app/models/LeonConsole.scala
index ad26ea4f0..04da86e2a 100644
--- a/web/app/models/LeonConsole.scala
+++ b/web/app/models/LeonConsole.scala
@@ -109,6 +109,8 @@ class ConsoleSession extends Actor {
pipeline.run(ctx)((code, "--timeout=2" :: Nil))
+ event("stopped")
+
case "synthesis" =>
event("started")
isStarted = true
diff --git a/web/app/views/index.scala.html b/web/app/views/index.scala.html
index 66848e7e1..1f132f0a5 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, prefix: String, websocketURL: String)(implicit request: RequestHeader)
+@(exs: List[examples.Example], default: examples.Example, prefix: String)(implicit request: RequestHeader)
@main("Leon Online", prefix) {
<div id="allcontent">
@@ -19,7 +19,7 @@
<div id="selectcolumn">
<h3>Load an Example:</h3>
<div>We provide you with a list of code-examples, select one from the list below to load it:</div>
- <select id="example-loader" name="codeexample" onchange="loadExample();">
+ <select id="example-loader" name="codeexample" onchange="loadExample('@prefix');">
<option value="">-- Load Example --</option>
@exs.zipWithIndex.map{ case (ex, i) =>
<option value="@i">@ex.title</option>
@@ -30,7 +30,7 @@
<script>
$(document).ready(function() {
var WS = window['MozWebSocket'] ? MozWebSocket : WebSocket
- var leonSocket = new WS("@websocketURL")
+ var leonSocket = new WS("@leon.web.controllers.routes.Application.openConsole().webSocketURL()")
var sendMessage = function() {
}
@@ -40,7 +40,10 @@
if (data.kind == "error") {
alert(data.message);
} else if (data.kind == "log") {
- $("#consolebox").val($("#consolebox").val()+"\n"+data.message);
+ var txt = $("#consolebox")
+
+ txt.val(txt.val()+"\n"+data.message);
+ txt.scrollTop(txt[0].scrollHeight - txt.height())
} else if (data.kind == "event") {
if (data.event == "started") {
$("#askbutton").val("... processing ...")
diff --git a/web/conf/application.conf b/web/conf/application.conf
index 4b8aada8e..ab89b5b5b 100644
--- a/web/conf/application.conf
+++ b/web/conf/application.conf
@@ -46,7 +46,4 @@ logger.play=INFO
logger.application=DEBUG
# This specifies the prefix under which the web page lies, used almost exclusively for the laraserver setup
-# app.prefix=/leon
-
-# Defines a specific URL to the websocket service
-# app.wsURL="ws://laraserver.epfl.ch:9000/openConsole"
+app.prefix=/leon
diff --git a/web/public/javascripts/leon.js b/web/public/javascripts/leon.js
index eaeea4e50..301629a40 100644
--- a/web/public/javascripts/leon.js
+++ b/web/public/javascripts/leon.js
@@ -4,12 +4,12 @@ function appendError(title, msg) {
alert(title+": "+msg)
}
-function loadExample() {
+function loadExample(prefix) {
var value = $("#example-loader").val()
if (value) {
$.ajax({
- url: '/ajax/getExample/'+value,
+ url: prefix+'/ajax/getExample/'+value,
dataType: "json",
success: function(data, textStatus, jqXHR) {
if (data.status == "success") {
--
GitLab