--- a/src/Pure/PIDE/session.scala Fri Jun 27 14:44:15 2025 +0200
+++ b/src/Pure/PIDE/session.scala Fri Jun 27 14:48:37 2025 +0200
@@ -128,9 +128,6 @@
def resources: Resources = Resources.bootstrap
- val init_time: Time = Time.now()
- def print_now(): String = (Time.now() - init_time).toString
-
val store: Store = Store(session_options)
def cache: Rich_Text.Cache = store.cache
@@ -803,4 +800,10 @@
def dialog_result(id: Document_ID.Generic, serial: Long, result: String): Unit =
manager.send(Session.Dialog_Result(id, serial, result))
+
+
+ /* diagnostics */
+
+ val init_time: Time = Time.now()
+ def print_now(): String = (Time.now() - init_time).toString
}