src/Pure/PIDE/headless.scala
changeset 69538 faf547d2834c
parent 69536 892b68f932f9
child 69562 636b3c03a61a
--- a/src/Pure/PIDE/headless.scala	Sat Dec 29 16:13:05 2018 +0100
+++ b/src/Pure/PIDE/headless.scala	Sat Dec 29 17:37:02 2018 +0100
@@ -433,12 +433,13 @@
   {
     resources =>
 
+    def options: Options = session_base_info.options
+
 
     /* session */
 
     def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
     {
-      val options = session_base_info.options
       val session = new Session(session_base_info.session, options, resources)
 
       val session_error = Future.promise[String]