src/Pure/PIDE/session.scala
changeset 82744 0ca8b1861fa3
parent 82742 085e624a1303
child 82750 0e36478a1b6a
--- a/src/Pure/PIDE/session.scala	Mon Jun 23 14:44:59 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Jun 24 20:52:09 2025 +0200
@@ -121,9 +121,11 @@
 }
 
 
-class Session(_session_options: => Options, val resources: Resources) extends Document.Session {
+class Session(_session_options: => Options) extends Document.Session {
   session =>
 
+  def resources: Resources = Resources.bootstrap
+
   val init_time: Time = Time.now()
   def print_now(): String = (Time.now() - init_time).toString