diff -r f78730341c87 -r af2d0e07493b src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sun Dec 20 13:20:09 2020 +0100 +++ b/src/Pure/PIDE/resources.scala Sun Dec 20 15:47:54 2020 +0100 @@ -12,6 +12,12 @@ import java.io.{File => JFile} +object Resources +{ + def empty: Resources = + new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) +} + class Resources( val sessions_structure: Sessions.Structure, val session_base: Sessions.Base,