clarified signature;
authorwenzelm
Fri, 27 Mar 2020 12:46:56 +0100
changeset 71813 269dc4bf1f40
parent 71812 d025735a4090
child 71814 23d0a45a9283
clarified signature;
src/Pure/ML/ml_console.scala
src/Pure/ML/ml_process.scala
src/Pure/PIDE/headless.scala
src/Pure/System/isabelle_process.scala
src/Pure/Tools/build.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Pure/ML/ml_console.scala	Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/ML/ml_console.scala	Fri Mar 27 12:46:56 2020 +0100
@@ -51,6 +51,7 @@
 
 
       val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+      val store = Sessions.store(options)
 
       // build logic
       if (!no_build && !raw_ml_system) {
@@ -64,10 +65,10 @@
 
       // process loop
       val process =
-        ML_Process(options, sessions_structure, logic = logic, args = List("-i"), redirect = true,
+        ML_Process(options, sessions_structure, store,
+          logic = logic, args = List("-i"), redirect = true,
           modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
           raw_ml_system = raw_ml_system,
-          store = Some(Sessions.store(options)),
           session_base =
             if (raw_ml_system) None
             else Some(Sessions.base_info(
--- a/src/Pure/ML/ml_process.scala	Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/ML/ml_process.scala	Fri Mar 27 12:46:56 2020 +0100
@@ -14,6 +14,7 @@
 {
   def apply(options: Options,
     sessions_structure: Sessions.Structure,
+    store: Sessions.Store,
     logic: String = "",
     args: List[String] = Nil,
     modes: List[String] = Nil,
@@ -22,18 +23,16 @@
     env: Map[String, String] = Isabelle_System.settings(),
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
-    session_base: Option[Sessions.Base] = None,
-    store: Option[Sessions.Store] = None): Bash.Process =
+    session_base: Option[Sessions.Base] = 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 {
         sessions_structure.selection(Sessions.Selection.session(logic_name)).
           build_requirements(List(logic_name)).
-          map(a => File.platform_path(_store.the_heap(a)))
+          map(a => File.platform_path(store.the_heap(a)))
       }
 
     val eval_init =
@@ -179,9 +178,10 @@
     if (args.isEmpty || more_args.nonEmpty) getopts.usage()
 
     val sessions_structure = Sessions.load_structure(options, dirs = dirs)
+    val store = Sessions.store(options)
 
     val rc =
-      ML_Process(options, sessions_structure, logic = logic, args = eval_args, modes = modes)
+      ML_Process(options, sessions_structure, store, logic = logic, args = eval_args, modes = modes)
         .result().print_stdout.rc
     sys.exit(rc)
   })
--- a/src/Pure/PIDE/headless.scala	Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Fri Mar 27 12:46:56 2020 +0100
@@ -585,7 +585,8 @@
       session.phase_changed += session_phase
 
       progress.echo("Starting session " + session_base_info.session + " ...")
-      Isabelle_Process(session, options, session_base_info.sessions_structure,
+      val store = Sessions.store(options)
+      Isabelle_Process(session, options, session_base_info.sessions_structure, store,
         logic = session_base_info.session, modes = print_mode)
 
       session_error.join match {
--- a/src/Pure/System/isabelle_process.scala	Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/System/isabelle_process.scala	Fri Mar 27 12:46:56 2020 +0100
@@ -16,12 +16,12 @@
     session: Session,
     options: Options,
     sessions_structure: Sessions.Structure,
+    store: Sessions.Store,
     logic: String = "",
     args: List[String] = Nil,
     modes: List[String] = Nil,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
-    store: Option[Sessions.Store] = None,
     phase_changed: Session.Phase => Unit = null)
   {
     val channel = System_Channel()
@@ -30,9 +30,8 @@
         val channel_options =
           options.string.update("system_channel_address", channel.address).
             string.update("system_channel_password", channel.password)
-        ML_Process(
-          channel_options, sessions_structure, logic = logic, args = args, modes = modes,
-          cwd = cwd, env = env, store = store)
+        ML_Process(channel_options, sessions_structure, store,
+          logic = logic, args = args, modes = modes, cwd = cwd, env = env)
       }
       catch { case exn @ ERROR(_) => channel.shutdown(); throw exn }
     process.stdin.close
--- a/src/Pure/Tools/build.scala	Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Pure/Tools/build.scala	Fri Mar 27 12:46:56 2020 +0100
@@ -250,8 +250,8 @@
 
           val session_result = Future.promise[Process_Result]
 
-          Isabelle_Process(session, options, sessions_structure,
-            logic = parent, cwd = info.dir.file, env = env, store = Some(store),
+          Isabelle_Process(session, options, sessions_structure, store,
+            logic = parent, cwd = info.dir.file, env = env,
             phase_changed =
             {
               case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -280,17 +280,16 @@
 
           val process =
             if (Sessions.is_pure(name)) {
-              ML_Process(options, deps.sessions_structure, raw_ml_system = true,
+              ML_Process(options, deps.sessions_structure, store, raw_ml_system = true,
                 args =
                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
                     List("--eval", eval),
-                cwd = info.dir.file, env = env, store = Some(store),
-                cleanup = () => args_file.delete)
+                cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
             }
             else {
-              ML_Process(options, deps.sessions_structure, logic = parent, args = List("--eval", eval),
-                cwd = info.dir.file, env = env, store = Some(store),
-                cleanup = () => args_file.delete)
+              ML_Process(options, deps.sessions_structure, store, logic = parent,
+                args = List("--eval", eval),
+                cwd = info.dir.file, env = env, cleanup = () => args_file.delete)
             }
 
           process.result(
--- a/src/Tools/VSCode/src/server.scala	Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Mar 27 12:46:56 2020 +0100
@@ -318,8 +318,9 @@
         }
       session.phase_changed += session_phase
 
-      Isabelle_Process(
-        session, options, base_info.sessions_structure, modes = modes, logic = base_info.session)
+      val store = Sessions.store(options)
+      Isabelle_Process(session, options, base_info.sessions_structure, store,
+        modes = modes, logic = base_info.session)
     }
   }
 
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 27 12:28:55 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Mar 27 12:46:56 2020 +0100
@@ -136,11 +136,11 @@
   def session_start(options0: Options)
   {
     val options = session_options(options0)
+    val store = Sessions.store(options)
 
     Isabelle_Process(PIDE.session, options,
-      PIDE.resources.session_base_info.sessions_structure,
+      PIDE.resources.session_base_info.sessions_structure, store,
       logic = PIDE.resources.session_name,
-      store = Some(Sessions.store(options)),
       modes =
         (space_explode(',', options.string("jedit_print_mode")) :::
          space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,