src/Pure/PIDE/headless.scala
changeset 69550 faf547d2834c
parent 69548 892b68f932f9
child 69576 636b3c03a61a
     1.1 --- a/src/Pure/PIDE/headless.scala	Sat Dec 29 16:13:05 2018 +0100
     1.2 +++ b/src/Pure/PIDE/headless.scala	Sat Dec 29 17:37:02 2018 +0100
     1.3 @@ -433,12 +433,13 @@
     1.4    {
     1.5      resources =>
     1.6  
     1.7 +    def options: Options = session_base_info.options
     1.8 +
     1.9  
    1.10      /* session */
    1.11  
    1.12      def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
    1.13      {
    1.14 -      val options = session_base_info.options
    1.15        val session = new Session(session_base_info.session, options, resources)
    1.16  
    1.17        val session_error = Future.promise[String]