src/Pure/PIDE/resources.scala
changeset 65255 d388e63a46fc
parent 65250 13a6c81534a8
child 65355 403eabd73c9a
     1.1 --- a/src/Pure/PIDE/resources.scala	Wed Mar 15 11:04:46 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Wed Mar 15 11:07:07 2017 +0100
     1.3 @@ -13,11 +13,6 @@
     1.4  import java.io.{File => JFile}
     1.5  
     1.6  
     1.7 -object Resources
     1.8 -{
     1.9 -  val empty: Resources = new Resources(Sessions.Base.empty)
    1.10 -}
    1.11 -
    1.12  class Resources(val base: Sessions.Base, val log: Logger = No_Logger)
    1.13  {
    1.14    val thy_info = new Thy_Info(this)