# HG changeset patch # User wenzelm # Date 1526656195 -7200 # Node ID aeffd8f1f079b687520b265cc8bf67fb5aa33d5c # Parent d9f2cf4fc002ac9fc6d362377f5d6efa77163aa0 support Store with options; diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/Admin/build_history.scala --- 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) ::: diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/Admin/isabelle_cronjob.scala --- 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", diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/Admin/jenkins.scala --- 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) } diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/ML/ml_console.scala --- 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)) diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/ML/ml_process.scala --- 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 = diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/System/isabelle_process.scala --- 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 = diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/Thy/export.scala --- 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 => { diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/Thy/export_theory.scala --- 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 => { diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/Thy/sessions.scala --- 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 */ diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Pure/Tools/build.scala --- 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 */ diff -r d9f2cf4fc002 -r aeffd8f1f079 src/Tools/jEdit/src/jedit_sessions.scala --- 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,