unused;
authorwenzelm
Fri, 25 Apr 2014 20:07:39 +0200
changeset 56728 6dc97c5aaf5e
parent 56722 ba1ac087b3a7
child 56729 1da2272a06a4
unused;
src/Pure/Thy/thy_info.scala
src/Pure/library.scala
--- 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
-  }
 }