--- a/src/Pure/PIDE/session.scala Sun Feb 05 20:05:14 2023 +0100 +++ b/src/Pure/PIDE/session.scala Sun Feb 05 20:09:39 2023 +0100 @@ -122,6 +122,7 @@ session => val init_time: Time = Time.now() + def print_now(): String = (Time.now() - init_time).toString val cache: Term.Cache = Term.Cache.make()