# HG changeset patch
# User wenzelm
# Date 1545395636 -3600
# Node ID b4b4d3ec55b31e606ccd4c3fd266a2ac9f9d4f5b
# Parent  1ec777ac098254402258d6b188d4dbf2d910e061
tuned signature;

diff -r 1ec777ac0982 -r b4b4d3ec55b3 src/Pure/PIDE/session.scala
--- 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")