author | wenzelm |
Sun, 06 Nov 2022 20:44:12 +0100 | |
changeset 76475 | 5c7652e9bc01 |
parent 76474 | 287c3adcdcd6 |
child 76476 | 9600720071e6 |
--- a/src/Pure/PIDE/session.scala Sun Nov 06 20:27:35 2022 +0100 +++ b/src/Pure/PIDE/session.scala Sun Nov 06 20:44:12 2022 +0100 @@ -119,6 +119,8 @@ class Session(_session_options: => Options, val resources: Resources) extends Document.Session { session => + val init_time: Time = Time.now() + val cache: Term.Cache = Term.Cache.make() def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =