diff --git a/lib/z3.jar b/lib/z3.jar
index c17cd9902a504d41c793de541d9aa0ac0e9d7935..8c6d5d9174d449abe05cae1f8fb60768d9fea799 100644
Binary files a/lib/z3.jar and b/lib/z3.jar differ
diff --git a/web/lib/funcheck-plugin_2.8.1-1.0.jar b/web/lib/funcheck-plugin_2.8.1-1.0.jar
index bb7ec9252c9aee9c6b6204da955bf8e126a4e1ae..69448e58e9f838866f43e5f15f538d09287c075d 100644
Binary files a/web/lib/funcheck-plugin_2.8.1-1.0.jar and b/web/lib/funcheck-plugin_2.8.1-1.0.jar differ
diff --git a/web/src/main/scala/bootstrap/liftweb/Boot.scala b/web/src/main/scala/bootstrap/liftweb/Boot.scala
index c51f94acdeebd3b730660c9fd0fa51e042736aee..70630c59d03eee1308730f6670f1e5b026020465 100644
--- a/web/src/main/scala/bootstrap/liftweb/Boot.scala
+++ b/web/src/main/scala/bootstrap/liftweb/Boot.scala
@@ -31,36 +31,13 @@ class Boot {
DB.defineConnectionManager(DefaultConnectionIdentifier, vendor)
}
- // Use Lift's Mapper ORM to populate the database
- // you don't need to use Mapper to use Lift... use
- // any ORM you want
- // Schemifier.schemify(true, Schemifier.infoF _, User)
-
// where to search snippet
LiftRules.addToPackages("code")
// Build SiteMap
def sitemap = SiteMap(
- Menu.i("Home") / "index", //>> User.AddUserMenusAfter, // the simple way to declare a menu
-
- // more complex because this menu allows anything in the
- // /static path to be visible
- Menu(Loc("Static", Link(List("static"), true, "/static/index"),
- "Static Content")))
-
- //def sitemapMutators = User.sitemapMutator
-
- // set the sitemap. Note if you don't want access control for
- // each page, just comment this line out.
- //LiftRules.setSiteMapFunc(() => sitemapMutators(sitemap))
-
- //Show the spinny image when an Ajax call starts
- LiftRules.ajaxStart =
- Full(() => LiftRules.jsArtifacts.show("ajax-loader").cmd)
-
- // Make the spinny image go away when it ends
- LiftRules.ajaxEnd =
- Full(() => LiftRules.jsArtifacts.hide("ajax-loader").cmd)
+ Menu.i("Home") / "index"
+ )
// Force the request to be UTF-8
LiftRules.early.append(_.setCharacterEncoding("UTF-8"))
@@ -70,7 +47,11 @@ class Boot {
// Use HTML5 for rendering
LiftRules.htmlProperties.default.set((r: Req) =>
- new Html5Properties(r.userAgent))
+ new Html5Properties(r.userAgent))
+
+ // Make laraserver happy with itself.
+ // LiftRules.ajaxPath = "leon/ajax_request"
+ // LiftRules.cometPath = "leon/comet_request"
// Make a transaction span the whole HTTP request
S.addAround(DB.buildLoanWrapper)
diff --git a/web/src/main/scala/code/comet/CodeProcessor.scala b/web/src/main/scala/code/comet/CodeProcessor.scala
index 910e777b6837aa0157919219dec557fc58df714c..f72d0c64063395ba64e0907b0036f3cb8d72afe6 100644
--- a/web/src/main/scala/code/comet/CodeProcessor.scala
+++ b/web/src/main/scala/code/comet/CodeProcessor.scala
@@ -27,16 +27,22 @@ case object Clear
// A funcheck/purescala compliant reporter that sends the
// strings to an actor rather than printing them.
class ActorReporter(dest : CodeProcessor) extends Reporter {
- private val BUFSZ : Int = 3
+ private val BUFSZ : Int = 10
private val buffer : Array[String] = new Array[String](BUFSZ)
private var id : Int = 0
def output(msg : Any) : Unit = {
- buffer(id) = msg.toString
- id += 1
- if(id == BUFSZ) {
- send()
- id = 0
+ val str = msg.toString
+ val trimmed = str.trim
+ val exclude = trimmed.startsWith("-") || trimmed.startsWith("Trying")
+
+ if(!exclude) {
+ buffer(id) = str
+ id += 1
+ if(id == BUFSZ) {
+ send()
+ id = 0
+ }
}
}
@@ -91,23 +97,24 @@ object QueryHandler extends LiftActor {
class CodeProcessor extends CometActor {
override def defaultPrefix = Full("codeprocessor")
private var msgs : List[String] = Nil
- private var msgXML : NodeSeq = Text("Waiting.")
override def lowPriority : PartialFunction[Any,Unit] = {
case Clear => {
msgs = Nil
- msgXML = Text("Waiting.")
- reRender()
+ partialUpdate(
+ SetValById("consolebox", "Cleared.")
+ )
}
case Message(msg) => {
- msgs = msgs ::: msg.split('\n').toList
- msgXML = msgs.flatMap(m => Seq(Text(m), <br/>))
- reRender()
+ msgs = msg :: msgs
+ partialUpdate(
+ SetValById("consolebox", msgs.reverse.mkString("\n"))
+ )
}
}
- def render = bind("consolelines" -> msgXML)
+ def render = <span></span>
override def fixedRender = bind("inputbox" ->
<lift:form>
@@ -116,7 +123,12 @@ class CodeProcessor extends CometActor {
QueryHandler ! Query(this, s)
}, "id" -> "codebox")
}
- <input type="submit" onClick="editor.save();" id="clicker" value="Groar !" />
+ {
+ SHtml.submit("Verify !", () => {}, "id" -> "clicker", "onClick" -> "editor.save();")
+ }
+ {
+ SHtml.textarea("Console.\n", s => {}, "id" -> "consolebox", "onChange" -> "document.getElementById('consolebox').scrollTop=document.getElementById('consolebox').scrollHeight;")
+ }
</lift:form>
- , "consolelines" -> msgXML)
+ )
}
diff --git a/web/src/main/webapp/images/leonlogo.png b/web/src/main/webapp/images/leonlogo.png
index 665fa3e31953fa5b6c1ed09c3359e722d8e12d81..3ed2861d496fbe2a14da33a18ec4579d40280eda 100644
Binary files a/web/src/main/webapp/images/leonlogo.png and b/web/src/main/webapp/images/leonlogo.png differ
diff --git a/web/src/main/webapp/index.html b/web/src/main/webapp/index.html
index 23dce4a50dfca248b61c0a06d5478ba7bf1d03f1..e9eef3909a5dc8c7d8edc33a2b2def67e3c55742 100644
--- a/web/src/main/webapp/index.html
+++ b/web/src/main/webapp/index.html
@@ -16,24 +16,7 @@
<lift:comet type="CodeProcessor">
<div class="contentbox" id="leonmain">
- <br />
<codeprocessor:inputbox></codeprocessor:inputbox>
- <!--
- <form>
- <textarea id="codebox">
-object Main {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- def size(lst : List) : Int = (lst match {
- case Cons(_, xs) => 1 + size(xs)
- case Nil() => 0
- }) ensuring(_ >= 0)
-}
- </textarea>
- <input type="submit" id="clicker" value="Roar!" />
- </form> -->
<script type="text/javascript">
// <![CDATA[
var editor = new CodeMirror.fromTextArea("codebox", {
@@ -45,14 +28,8 @@ stylesheet: "codemirror/scalacolors.css"
});
// ]]>
</script>
- </div>
-
- <div class="contentbox" id="console">
- <div id="consoletext">
- I am the console.</br>
- <lift:snippet type="Z3Snippet:versionString"></lift:snippet></br>
- <codeprocessor:consolelines>Additional console lines</codeprocessor:consolelines>
- </div>
+<!-- Server is running <lift:snippet type="Z3Snippet:versionString"></lift:snippet>
+<codeprocessor:consolelines>Additional console lines</codeprocessor:consolelines> -->
</div>
</lift:comet>
diff --git a/web/src/main/webapp/style.css b/web/src/main/webapp/style.css
index 4d4414f3b1c99d737fa496ba2c803b60cdaf3508..d7853a8d8b180f6edc1c734805f38eb256cd3e5f 100644
--- a/web/src/main/webapp/style.css
+++ b/web/src/main/webapp/style.css
@@ -1,3 +1,7 @@
+html {
+ height: 100%;
+}
+
body {
font-family: Arial, Helvetica, Sans-serif;
margin: 0px;
@@ -6,6 +10,7 @@ body {
background-color: #FFFFFF;
background-repeat: no-repeat;
background-position: 25px 15px;
+ height: 100%;
}
h2 {
@@ -39,33 +44,24 @@ div.contentbox {
position: relative;
left: 320px;
width: 700px;
+ padding: 0px;
+ margin: 0px;
}
div#title {
- top: 10px;
- text-align: right;
- padding: 0px;
- margin: 0px;
+ height: 80px;
+ min-height: 80px;
+ max-height: 80px;
+ background-image: url('images/leonlogo.png');
+ background-repeat: no-repeat;
+ background-position: right bottom;
}
div#leonmain {
- position: absolute;
- top: 60px;
}
div#console {
- position: absolute;
- top: 550px;
- display: inline;
-}
-
-div#logo {
- position: absolute;
- top: 15px;
- left: 25px;
- width: 290px;
- height: 400px;
- background-image: url('images/lionbkg.png');
+ background-color: #EEEEEE;
}
div#contact {
@@ -75,21 +71,20 @@ div#contact {
width: 290px;
}
+div#allcontent {
+ height: 100%;
+ min-height: 100%;
+}
+
div#poweredby {
- position: absolute;
+ position: fixed;
left: 0px;
+ bottom: 0px;
width: 1020px;
+ height: 50px;
text-align: center;
display: table-cell;
-}
-
-div#ghost {
- height: 650px;
- z-index: -1000;
-}
-
-.middiv {
- vertical-align: middle;
+ background-color: #FFFFFF;
}
.smallnote {
@@ -119,35 +114,12 @@ li {
}
#clicker {
- margin-top: 5px 0px;
+ margin: 5px 0px;
background-color: transparent;
border: 1px solid #666666;
width: 100%;
}
-div#consoletext {
- background-color: #EEEEEE;
- width: 100%;
- font-family: "Lucida Console", monospace;
- font-size: 10px;
-}
-
-table.consoletable {
- width: 32%;
- margin: 0px;
- padding: 0px;
-}
-
-tr.consolerow {
- border: none;
- border-bottom: 1px dashed #000;
-}
-
-td.contacttype {
- text-align:right;
- vertical-align: top;
-}
-
td.date {
text-align:right;
}
@@ -158,3 +130,20 @@ textarea#codebox {
width: 700px;
height: 450px;
}
+
+textarea#consolebox {
+ font-family: "Lucida Console", monospace;
+ font-size: 11px;
+ width: 700px;
+ height: 250px;
+ border: none;
+ background-color: #EEEEEE;
+ padding: 0px;
+ margin: 0px;
+ resize: vertical;
+}
+
+.consoletext {
+ font-family: "Lucida Console", monospace;
+ font-size: 11px;
+}
diff --git a/web/src/main/webapp/templates-hidden/funcheck.html b/web/src/main/webapp/templates-hidden/funcheck.html
index bb661afd6250d27da5b9e99d291f337e9cb48cd3..06cf7ebc8fe379eff4d8ec02281e9a76959dc2b5 100644
--- a/web/src/main/webapp/templates-hidden/funcheck.html
+++ b/web/src/main/webapp/templates-hidden/funcheck.html
@@ -3,15 +3,14 @@
<link rel="stylesheet" href="style.css" />
<link rel="icon" type="image/png" href="images/lambda-ico.png" />
<meta content="text/html; charset=UTF-8" http-equiv="content-type" />
- <script id="jquery" src="/classpath/jquery.js" type="text/javascript"></script>
- <script id="json" src="/classpath/json.js" type="text/javascript"></script>
+ <script id="jquery" src="classpath/jquery.js" type="text/javascript"></script>
+ <script id="json" src="classpath/json.js" type="text/javascript"></script>
</head>
<body>
- <div class="contentbox" id="title">
- <img src="images/leonlogo.png" alt="LeonOnline" />
- </div>
+ <div id="allcontent">
+ <div id="beforefooter">
- <div id="logo"> </div>
+ <div class="contentbox" id="title"></div>
<div id="contact">
<p><i>Leon</i> is developed by the <a href="http://lara.epfl.ch" alt="LARA Group EPFL">LARA</a> group at <a href="http://www.epfl.ch">EPFL</a>.</p>
@@ -19,7 +18,7 @@
<div id="content">The main content will get bound here</div>
- <div class="contentbox" id="ghost"></div>
+ </div>
<div id="poweredby">
<hr />
@@ -30,5 +29,6 @@
<a href="http://codemirror.net"><img class="middiv" alt="CodeMirror" src="images/codemirrorlogo.png" /></a>
<a href="http://www.epfl.ch"><img class="middiv" alt="EPFL" src="images/epfllogo.png" /></a>
</div>
+ </div>
</body>
</html>