author | wenzelm |
Wed, 15 Mar 2017 11:07:07 +0100 | |
changeset 65255 | d388e63a46fc |
parent 65254 | 3075aa3b40bf |
child 65256 | c3d6dd17d626 |
--- a/src/Pure/PIDE/resources.scala Wed Mar 15 11:04:46 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Wed Mar 15 11:07:07 2017 +0100 @@ -13,11 +13,6 @@ import java.io.{File => JFile} -object Resources -{ - val empty: Resources = new Resources(Sessions.Base.empty) -} - class Resources(val base: Sessions.Base, val log: Logger = No_Logger) { val thy_info = new Thy_Info(this)