--- a/src/Pure/PIDE/session.scala Fri Dec 21 13:02:45 2018 +0100
+++ b/src/Pure/PIDE/session.scala Fri Dec 21 13:33:56 2018 +0100
@@ -115,7 +115,7 @@
}
-class Session(session_options: => Options, val resources: Resources) extends Document.Session
+class Session(_session_options: => Options, val resources: Resources) extends Document.Session
{
session =>
@@ -131,6 +131,8 @@
/* dynamic session options */
+ def session_options: Options = _session_options
+
def output_delay: Time = session_options.seconds("editor_output_delay")
def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay")
def prune_delay: Time = session_options.seconds("editor_prune_delay")