diff --git a/web/README b/web/README new file mode 100644 index 0000000000000000000000000000000000000000..fc63a7c7b8aca5dab8e75137d9986306fefb69ed --- /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 ccec9b1ad876a0d24ed00a45e7ccc2f9ebc31147..1d2269a49e654659ef58046e79a96768770e6fac 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 ad26ea4f0c4b9db903565d2e98d5e4b31ace797f..04da86e2a92dd417b3b56eb7bce3d1e89e10bbf3 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 66848e7e198fc22ed92ea7b8d177e621b018532e..1f132f0a5a6014caf390fe1da1a3e1e066e3b92e 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 4b8aada8edc68c8a00c7a1f832886a748e2aa2b4..ab89b5b5b6cf58a8c580952a492ff41d766fdee5 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 eaeea4e508e80c4b23568f9a3324c449c0001721..301629a4020a594118ace7de553abc564bd5ab1d 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") {