--- a/src/Pure/Thy/thy_info.scala Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/Thy/thy_info.scala Fri Apr 25 20:07:39 2014 +0200
@@ -7,9 +7,6 @@
package isabelle
-import java.util.concurrent.{Future => JFuture}
-
-
class Thy_Info(resources: Resources)
{
/* messages */
--- a/src/Pure/library.scala Fri Apr 25 17:54:54 2014 +0200
+++ b/src/Pure/library.scala Fri Apr 25 20:07:39 2014 +0200
@@ -159,18 +159,6 @@
def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
-
-
- /* Java futures */
-
- def future_value[A](x: A) = new JFuture[A]
- {
- def cancel(may_interrupt: Boolean): Boolean = false
- def isCancelled(): Boolean = false
- def isDone(): Boolean = true
- def get(): A = x
- def get(timeout: Long, time_unit: TimeUnit): A = x
- }
}