--- a/src/Pure/PIDE/headless.scala Fri Mar 27 12:46:56 2020 +0100
+++ b/src/Pure/PIDE/headless.scala Fri Mar 27 13:02:56 2020 +0100
@@ -396,8 +396,8 @@
object Resources
{
- def apply(base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
- new Resources(base_info, log = log)
+ def apply(options: Options, base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources =
+ new Resources(options, base_info, log = log)
def make(
options: Options,
@@ -410,7 +410,7 @@
val base_info =
Sessions.base_info(options, session_name, dirs = session_dirs,
include_sessions = include_sessions, progress = progress)
- apply(base_info, log = log)
+ apply(options, base_info, log = log)
}
final class Theory private[Headless](
@@ -554,6 +554,7 @@
}
class Resources private[Headless](
+ val options: Options,
val session_base_info: Sessions.Base_Info,
log: Logger = No_Logger)
extends isabelle.Resources(
@@ -561,8 +562,6 @@
{
resources =>
- def options: Options = session_base_info.options
-
/* session */