websocket URL no longer needed

web/README

+## 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

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 { 

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

web/app/views/index.scala.html

-@(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 ...")

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

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") {