equal
deleted
inserted
replaced
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 |