# HG changeset patch
# User wenzelm
# Date 1751028517 -7200
# Node ID 6801c04a7a1a2dbbc0cd9e4d237b4a6346869a04
# Parent  7dd048f6ead621f93140533d8a37507663aa62db
tuned (see also 5c7652e9bc01);

diff -r 7dd048f6ead6 -r 6801c04a7a1a 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
 }