unused;
authorwenzelm
Fri Apr 25 20:07:39 2014 +0200 (2014-04-25)
changeset 567286dc97c5aaf5e
parent 56722 ba1ac087b3a7
child 56729 1da2272a06a4
unused;
src/Pure/Thy/thy_info.scala
src/Pure/library.scala
     1.1 --- a/src/Pure/Thy/thy_info.scala	Fri Apr 25 17:54:54 2014 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Apr 25 20:07:39 2014 +0200
     1.3 @@ -7,9 +7,6 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.util.concurrent.{Future => JFuture}
     1.8 -
     1.9 -
    1.10  class Thy_Info(resources: Resources)
    1.11  {
    1.12    /* messages */
     2.1 --- a/src/Pure/library.scala	Fri Apr 25 17:54:54 2014 +0200
     2.2 +++ b/src/Pure/library.scala	Fri Apr 25 20:07:39 2014 +0200
     2.3 @@ -159,18 +159,6 @@
     2.4    def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
     2.5    def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
     2.6    def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
     2.7 -
     2.8 -
     2.9 -  /* Java futures */
    2.10 -
    2.11 -  def future_value[A](x: A) = new JFuture[A]
    2.12 -  {
    2.13 -    def cancel(may_interrupt: Boolean): Boolean = false
    2.14 -    def isCancelled(): Boolean = false
    2.15 -    def isDone(): Boolean = true
    2.16 -    def get(): A = x
    2.17 -    def get(timeout: Long, time_unit: TimeUnit): A = x
    2.18 -  }
    2.19  }
    2.20  
    2.21