src/Pure/Thy/sessions.scala
changeset 73700 908351c8c0b1
parent 73367 77ef8bef0593
child 73701 d83e7e444b43
--- a/src/Pure/Thy/sessions.scala	Sat May 15 22:39:07 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Sun May 16 13:06:13 2021 +0200
@@ -502,6 +502,7 @@
 
     def dirs: List[Path] = dir :: directories
 
+    def timeout_ignored: Boolean = Time.seconds(options.real("timeout")) < Time.ms(1)
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
     def document_enabled: Boolean =