clarified signature;
authorwenzelm
Thu, 17 May 2018 15:38:36 +0200
changeset 68204 a554da2811f2
parent 68203 cda4f24331d5
child 68205 9a8949f71fd4
clarified signature;
src/Pure/ML/ml_process.scala
src/Pure/System/isabelle_process.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/imports.scala
src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Pure/ML/ml_process.scala	Thu May 17 14:50:48 2018 +0200
+++ b/src/Pure/ML/ml_process.scala	Thu May 17 15:38:36 2018 +0200
@@ -23,7 +23,7 @@
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
     channel: Option[System_Channel] = None,
-    sessions: Option[Sessions.Structure] = None,
+    sessions_structure: Option[Sessions.Structure] = None,
     session_base: Option[Sessions.Base] = None,
     store: Sessions.Store = Sessions.store()): Bash.Process =
   {
@@ -33,7 +33,8 @@
       else {
         val selection = Sessions.Selection(sessions = List(logic_name))
         val selected_sessions =
-          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
+          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)))
       }
--- a/src/Pure/System/isabelle_process.scala	Thu May 17 14:50:48 2018 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu May 17 15:38:36 2018 +0200
@@ -20,7 +20,7 @@
     modes: List[String] = Nil,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
-    sessions: Option[Sessions.Structure] = None,
+    sessions_structure: Option[Sessions.Structure] = None,
     store: Sessions.Store = Sessions.store(),
     phase_changed: Session.Phase => Unit = null)
   {
@@ -30,7 +30,7 @@
     session.start(receiver =>
       Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
         cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
-        sessions = sessions, store = store))
+        sessions_structure = sessions_structure, store = store))
   }
 
   def apply(
@@ -43,14 +43,14 @@
     env: Map[String, String] = Isabelle_System.settings(),
     receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
     xml_cache: XML.Cache = XML.make_cache(),
-    sessions: Option[Sessions.Structure] = None,
+    sessions_structure: Option[Sessions.Structure] = None,
     store: Sessions.Store = Sessions.store()): Prover =
   {
     val channel = System_Channel()
     val process =
       try {
-        ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
-          cwd = cwd, env = env, sessions = sessions, store = store, channel = Some(channel))
+        ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, cwd = cwd,
+          env = env, sessions_structure = sessions_structure, store = store, channel = Some(channel))
       }
       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
     process.stdin.close
--- a/src/Pure/Thy/sessions.scala	Thu May 17 14:50:48 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu May 17 15:38:36 2018 +0200
@@ -168,7 +168,8 @@
     def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
   }
 
-  sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
+  sealed case class Deps(
+    sessions_structure: Structure, session_bases: Map[String, Base], all_known: Known)
   {
     def is_empty: Boolean = session_bases.isEmpty
     def apply(name: String): Base = session_bases(name)
@@ -351,7 +352,7 @@
           }
       })
 
-    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
+    Deps(sessions_structure, session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
   }
 
 
@@ -448,7 +449,7 @@
     val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
     val base1 = deps1(session1).copy(known = deps1.all_known)
 
-    Base_Info(options, dirs, session1, sessions1, deps1.errors, base1, infos1)
+    Base_Info(options, dirs, session1, deps1.sessions_structure, deps1.errors, base1, infos1)
   }
 
 
--- a/src/Pure/Tools/build.scala	Thu May 17 14:50:48 2018 +0200
+++ b/src/Pure/Tools/build.scala	Thu May 17 15:38:36 2018 +0200
@@ -174,7 +174,6 @@
   private class Job(progress: Progress,
     name: String,
     val info: Sessions.Info,
-    sessions: Sessions.Structure,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_output: Boolean,
@@ -238,8 +237,8 @@
 
           val session_result = Future.promise[Process_Result]
 
-          Isabelle_Process.start(session, options, logic = parent,
-            cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
+          Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
+            sessions_structure = Some(deps.sessions_structure), store = store,
             phase_changed =
             {
               case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -272,12 +271,12 @@
                 args =
                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
                   List("--eval", eval),
-                env = env, sessions = Some(sessions), store = store,
+                env = env, sessions_structure = Some(deps.sessions_structure), store = store,
                 cleanup = () => args_file.delete)
             }
             else {
               ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
-                env = env, sessions = Some(sessions), store = store,
+                env = env, sessions_structure = Some(deps.sessions_structure), store = store,
                 cleanup = () => args_file.delete)
             }
 
@@ -413,17 +412,16 @@
       Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
         exclude_sessions, session_groups, sessions) ++ selection
 
-    val (selected_sessions, deps) =
+    val deps =
     {
-      val selected_sessions0 = full_sessions.selection(selection1)
       val deps0 =
-        Sessions.deps(selected_sessions0, full_sessions.global_theories,
+        Sessions.deps(full_sessions.selection(selection1), full_sessions.global_theories,
           progress = progress, inlined_files = true, verbose = verbose,
           list_files = list_files, check_keywords = check_keywords).check_errors
 
       if (soft_build && !fresh_build) {
         val outdated =
-          selected_sessions0.build_topological_order.flatMap(name =>
+          deps0.sessions_structure.build_topological_order.flatMap(name =>
             store.find_database(name) match {
               case Some(database) =>
                 using(SQLite.open_database(database))(store.read_build(_, name)) match {
@@ -433,14 +431,11 @@
                 }
               case None => Some(name)
             })
-        val selected_sessions =
-          full_sessions.selection(Sessions.Selection(sessions = outdated))
-        val deps =
-          Sessions.deps(selected_sessions, full_sessions.global_theories,
-            progress = progress, inlined_files = true).check_errors
-        (selected_sessions, deps)
+
+        Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
+          full_sessions.global_theories, progress = progress, inlined_files = true).check_errors
       }
-      else (selected_sessions0, deps0)
+      else deps0
     }
 
 
@@ -465,7 +460,7 @@
 
     /* main build process */
 
-    val queue = Queue(progress, selected_sessions, store)
+    val queue = Queue(progress, deps.sessions_structure, store)
 
     store.prepare_output()
 
@@ -592,7 +587,7 @@
             pending.dequeue(running.isDefinedAt(_)) match {
               case Some((name, info)) =>
                 val ancestor_results =
-                  selected_sessions.build_requirements(List(name)).filterNot(_ == name).
+                  deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
                     map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
 
@@ -636,7 +631,7 @@
 
                   val numa_node = numa_nodes.next(used_node(_))
                   val job =
-                    new Job(progress, name, info, selected_sessions, deps, store, do_output,
+                    new Job(progress, name, info, deps, store, do_output,
                       verbose, pide, numa_node, queue.command_timings(name))
                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
                 }
--- a/src/Pure/Tools/imports.scala	Thu May 17 14:50:48 2018 +0200
+++ b/src/Pure/Tools/imports.scala	Thu May 17 15:38:36 2018 +0200
@@ -100,23 +100,22 @@
     verbose: Boolean = false) =
   {
     val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
-    val selected_sessions = full_sessions.selection(selection)
 
     val deps =
-      Sessions.deps(selected_sessions, full_sessions.global_theories,
+      Sessions.deps(full_sessions.selection(selection), full_sessions.global_theories,
         progress = progress, verbose = verbose).check_errors
 
     val root_keywords = Sessions.root_syntax.keywords
 
     if (operation_imports) {
       val report_imports: List[Report] =
-        selected_sessions.build_topological_order.map((session_name: String) =>
+        deps.sessions_structure.build_topological_order.map((session_name: String) =>
           {
-            val info = selected_sessions(session_name)
+            val info = deps.sessions_structure(session_name)
             val session_base = deps(session_name)
 
             val declared_imports =
-              selected_sessions.imports_requirements(List(session_name)).toSet
+              deps.sessions_structure.imports_requirements(List(session_name)).toSet
 
             val extra_imports =
               (for {
@@ -128,18 +127,18 @@
               } yield qualifier).toSet
 
             val loaded_imports =
-              selected_sessions.imports_requirements(
+              deps.sessions_structure.imports_requirements(
                 session_base.loaded_theories.keys.map(a =>
                   session_base.theory_qualifier(session_base.known.theories(a))))
               .toSet - session_name
 
             val minimal_imports =
               loaded_imports.filter(s1 =>
-                !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
+                !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2)))
 
             def make_result(set: Set[String]): Option[List[String]] =
               if (set.isEmpty) None
-              else Some(selected_sessions.imports_topological_order.filter(set))
+              else Some(deps.sessions_structure.imports_topological_order.filter(set))
 
             Report(info, declared_imports, make_result(extra_imports),
               if (loaded_imports == declared_imports - session_name) None
@@ -173,9 +172,9 @@
     if (operation_update) {
       progress.echo("\nUpdate theory imports" + update_message + ":")
       val updates =
-        selected_sessions.build_topological_order.flatMap(session_name =>
+        deps.sessions_structure.build_topological_order.flatMap(session_name =>
           {
-            val info = selected_sessions(session_name)
+            val info = deps.sessions_structure(session_name)
             val session_base = deps(session_name)
             val session_resources = new Resources(session_base)
             val imports_base = session_base.get_imports
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu May 17 14:50:48 2018 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu May 17 15:38:36 2018 +0200
@@ -133,7 +133,7 @@
   def session_start(options: Options)
   {
     Isabelle_Process.start(PIDE.session, session_options(options),
-      sessions = Some(PIDE.resources.session_base_info.sessions_structure),
+      sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
       logic = PIDE.resources.session_name,
       store = Sessions.store(session_build_mode() == "system"),
       modes =