Works on web with hardcoded classPath **TO FIX**

src/main/scala/leon/Settings.scala

@@ -12,5 +12,10 @@ object Settings {
 case class Settings(
   val synthesis: Boolean    = false,
   val xlang: Boolean        = false,
-  val verify: Boolean       = true
+  val verify: Boolean       = true,
+  val classPath: String     = 
+    List(
+      "/home/ekneuss/scala/scala-2.9.2/lib/",
+      "/home/ekneuss/git/leon-2.0/library/target/scala-2.9.2/"
+    ).mkString(":")
 )

src/main/scala/leon/plugin/ExtractionPhase.scala

@@ -12,7 +12,7 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
   def run(ctx: LeonContext)(args: List[String]): Program = {
 
     val settings = new NSCSettings
-    settings.usejavacp.value = true
+    settings.extdirs.value = ctx.settings.classPath
 
     val compilerOpts = args.filterNot(_.startsWith("--"))
 
@@ -21,6 +21,12 @@ object ExtractionPhase extends LeonPhase[List[String], Program] {
     }
 
     if(command.ok) {
+      // Debugging code for classpath crap
+      //new scala.tools.util.PathResolver(settings).Calculated.basis.foreach { cp =>
+      //  cp.foreach( p => 
+      //    ctx.reporter.info(" => "+p.toString)
+      //  )
+      //}
       val runner = new PluginRunner(settings, ctx, None)
       val run = new runner.Run
       run.compile(command.files)

web/app/examples/VerificationExamples.scala

@@ -9,8 +9,8 @@ object VerificationExamples {
 
   val default = Example("Default", """
 import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
 
 object Example {
   sealed abstract class List
@@ -34,8 +34,8 @@ object Example {
 
   newExample("Amortized Queue", """
 import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
 
 object AmortizedQueue {
   sealed abstract class List
@@ -139,8 +139,8 @@ object AmortizedQueue {
 
   newExample("Associative List", """
 import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
 
 object AssociativeList { 
   sealed abstract class KeyValuePairAbs
@@ -192,8 +192,8 @@ object AssociativeList {
 
   newExample("Insertion Sort", """
 import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
 
 object InsertionSort {
   sealed abstract class List
@@ -274,8 +274,8 @@ object InsertionSort {
 
   newExample("List Operations", """
 import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
 
 object ListOperations {
     sealed abstract class List
@@ -384,8 +384,8 @@ object ListOperations {
 
   newExample("Propositional Logic", """
 import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
 
 object PropositionalLogic { 
 
@@ -488,8 +488,8 @@ object PropositionalLogic {
 
   newExample("Red-Black Tree", """
 import scala.collection.immutable.Set
-import funcheck.Annotations._
-import funcheck.Utils._
+import leon.Annotations._
+import leon.Utils._
 
 object RedBlackTree { 
   sealed abstract class Color
@@ -607,8 +607,8 @@ object RedBlackTree {
 
   newExample("Search Linked-List", """
 import scala.collection.immutable.Set
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
 
 object SearchLinkedList {
   sealed abstract class List
@@ -657,8 +657,8 @@ object SearchLinkedList {
   """.trim)
 
   newExample("Sum and Max", """
-import funcheck.Utils._
-import funcheck.Annotations._
+import leon.Utils._
+import leon.Annotations._
 
 object SumAndMax {
   sealed abstract class List

web/app/models/LeonConsole.scala

@@ -20,6 +20,8 @@ import leon.{LeonContext, Settings, Reporter}
 import leon.plugin.{TemporaryInputPhase, ExtractionPhase}
 import leon.verification.AnalysisPhase
 
+import scala.tools.util.PathResolver
+
 
 object LeonConsole {
   def open: Promise[(Iteratee[JsValue,_],Enumerator[JsValue])] = {

web/lib/cafebabe_2.9.2-1.2.jar

+../../unmanaged/64/cafebabe_2.9.2-1.2.jar
\ No newline at end of file

web/lib/scalaz3.jar

+../../unmanaged/64/scalaz3.jar
\ No newline at end of file

web/public/stylesheets/leon.css

@@ -143,7 +143,7 @@ td.date {
 
 div#codebox {
     border-style: none;
-    background-color: rgba(255,255,255,0.5);
+    background-color: rgba(255,255,255,0.8);
     border: 1px dashed #333;
     width: 700px;
     height: 450px;