src/Pure/PIDE/headless.scala
changeset 76665 7530d49d928a
parent 76664 bb8692acdcf4
child 76702 94cdf6513f01
equal deleted inserted replaced
76664:bb8692acdcf4 76665:7530d49d928a
   600       }
   600       }
   601     }
   601     }
   602   }
   602   }
   603 
   603 
   604   class Resources private[Headless](
   604   class Resources private[Headless](
   605       val options: Options,
   605     val options: Options,
   606       session_background: Sessions.Background,
   606     session_background: Sessions.Background,
   607       log: Logger = No_Logger)
   607     log: Logger = No_Logger)
   608     extends isabelle.Resources(session_background.check_errors, log = log) {
   608   extends isabelle.Resources(session_background.check_errors, log = log) {
   609     resources =>
   609     resources =>
   610 
   610 
   611     val store: Sessions.Store = Sessions.store(options)
   611     val store: Sessions.Store = Sessions.store(options)
   612 
   612 
   613 
   613