--- a/src/Pure/Admin/build_history.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/Admin/build_history.scala Fri May 18 17:09:55 2018 +0200
@@ -243,7 +243,7 @@
/* output log */
- val store = Sessions.store()
+ val store = Sessions.store(options)
val meta_info =
Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) :::
--- a/src/Pure/Admin/isabelle_cronjob.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri May 18 17:09:55 2018 +0200
@@ -529,7 +529,7 @@
(rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
} yield remote_build_history(rev, afp_rev, i, r)))),
Logger_Task("jenkins_logs", _ =>
- Jenkins.download_logs(Jenkins.build_log_jobs, main_dir)),
+ Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)),
Logger_Task("build_log_database",
logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
Logger_Task("build_status",
--- a/src/Pure/Admin/jenkins.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/Admin/jenkins.scala Fri May 18 17:09:55 2018 +0200
@@ -40,9 +40,10 @@
} yield name
- def download_logs(job_names: List[String], dir: Path, progress: Progress = No_Progress)
+ def download_logs(
+ options: Options, job_names: List[String], dir: Path, progress: Progress = No_Progress)
{
- val store = Sessions.store()
+ val store = Sessions.store(options)
val infos = job_names.flatMap(build_job_infos(_))
Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos)
}
--- a/src/Pure/ML/ml_console.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/ML/ml_console.scala Fri May 18 17:09:55 2018 +0200
@@ -69,7 +69,8 @@
val process =
ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
- raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
+ raw_ml_system = raw_ml_system,
+ store = Some(Sessions.store(options, system_mode)),
session_base =
if (raw_ml_system) None
else Some(Sessions.base_info(options, logic, dirs = dirs).check_base))
--- a/src/Pure/ML/ml_process.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/ML/ml_process.scala Fri May 18 17:09:55 2018 +0200
@@ -25,9 +25,11 @@
channel: Option[System_Channel] = None,
sessions_structure: Option[Sessions.Structure] = None,
session_base: Option[Sessions.Base] = None,
- store: Sessions.Store = Sessions.store()): Bash.Process =
+ store: Option[Sessions.Store] = None): Bash.Process =
{
val logic_name = Isabelle_System.default_logic(logic)
+ val store_ = store.getOrElse(Sessions.store(options))
+
val heaps: List[String] =
if (raw_ml_system) Nil
else {
@@ -36,7 +38,7 @@
sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
.selection(selection)
selected_sessions.build_requirements(List(logic_name)).
- map(a => File.platform_path(store.heap(a)))
+ map(a => File.platform_path(store_.heap(a)))
}
val eval_init =
--- a/src/Pure/System/isabelle_process.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/System/isabelle_process.scala Fri May 18 17:09:55 2018 +0200
@@ -21,7 +21,7 @@
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
sessions_structure: Option[Sessions.Structure] = None,
- store: Sessions.Store = Sessions.store(),
+ store: Option[Sessions.Store] = None,
phase_changed: Session.Phase => Unit = null)
{
if (phase_changed != null)
@@ -44,7 +44,7 @@
receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
xml_cache: XML.Cache = XML.make_cache(),
sessions_structure: Option[Sessions.Structure] = None,
- store: Sessions.Store = Sessions.store()): Prover =
+ store: Option[Sessions.Store] = None): Prover =
{
val channel = System_Channel()
val process =
--- a/src/Pure/Thy/export.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/Thy/export.scala Fri May 18 17:09:55 2018 +0200
@@ -252,7 +252,7 @@
/* database */
- val store = Sessions.store(system_mode)
+ val store = Sessions.store(options, system_mode)
using(SQLite.open_database(store.the_database(session_name)))(db =>
{
--- a/src/Pure/Thy/export_theory.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala Fri May 18 17:09:55 2018 +0200
@@ -23,13 +23,11 @@
theory_graph.topological_order.map(theory_graph.get_node(_))
}
- def read_session(session_name: String,
- system_mode: Boolean = false,
+ def read_session(store: Sessions.Store,
+ session_name: String,
types: Boolean = true,
consts: Boolean = true): Session =
{
- val store = Sessions.store(system_mode)
-
val thys =
using(SQLite.open_database(store.the_database(session_name)))(db =>
{
--- a/src/Pure/Thy/sessions.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Fri May 18 17:09:55 2018 +0200
@@ -961,9 +961,10 @@
val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns)
}
- def store(system_mode: Boolean = false): Store = new Store(system_mode)
+ def store(options: Options, system_mode: Boolean = false): Store =
+ new Store(options, system_mode)
- class Store private[Sessions](system_mode: Boolean)
+ class Store private[Sessions](val options: Options, val system_mode: Boolean)
{
/* file names */
--- a/src/Pure/Tools/build.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Pure/Tools/build.scala Fri May 18 17:09:55 2018 +0200
@@ -238,7 +238,7 @@
val session_result = Future.promise[Process_Result]
Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
- sessions_structure = Some(deps.sessions_structure), store = store,
+ sessions_structure = Some(deps.sessions_structure), store = Some(store),
phase_changed =
{
case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -271,12 +271,12 @@
args =
(for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
List("--eval", eval),
- env = env, sessions_structure = Some(deps.sessions_structure), store = store,
+ env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
cleanup = () => args_file.delete)
}
else {
ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
- env = env, sessions_structure = Some(deps.sessions_structure), store = store,
+ env = env, sessions_structure = Some(deps.sessions_structure), store = Some(store),
cleanup = () => args_file.delete)
}
@@ -393,7 +393,7 @@
{
val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
- val store = Sessions.store(system_mode)
+ val store = Sessions.store(build_options, system_mode)
/* session selection and dependencies */
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri May 18 16:30:20 2018 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri May 18 17:09:55 2018 +0200
@@ -135,7 +135,7 @@
Isabelle_Process.start(PIDE.session, session_options(options),
sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
logic = PIDE.resources.session_name,
- store = Sessions.store(session_build_mode() == "system"),
+ store = Some(Sessions.store(options, session_build_mode() == "system")),
modes =
(space_explode(',', options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,