tuned (see also 5c7652e9bc01);
authorwenzelm
Fri, 27 Jun 2025 14:48:37 +0200
changeset 82782 6801c04a7a1a
parent 82781 7dd048f6ead6
child 82783 98d9abefd9b0
tuned (see also 5c7652e9bc01);
src/Pure/PIDE/session.scala
--- 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
 }