| changeset 72962 | af2d0e07493b |
| parent 72957 | 75fc90edc0a8 |
| child 73340 | 0ffcad1f6130 |
--- 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,