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