clarified signature;
authorwenzelm
Thu May 17 15:38:36 2018 +0200 (4 days ago)
changeset 68204a554da2811f2
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
     1.1 --- a/src/Pure/ML/ml_process.scala	Thu May 17 14:50:48 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_process.scala	Thu May 17 15:38:36 2018 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4      redirect: Boolean = false,
     1.5      cleanup: () => Unit = () => (),
     1.6      channel: Option[System_Channel] = None,
     1.7 -    sessions: Option[Sessions.Structure] = None,
     1.8 +    sessions_structure: Option[Sessions.Structure] = None,
     1.9      session_base: Option[Sessions.Base] = None,
    1.10      store: Sessions.Store = Sessions.store()): Bash.Process =
    1.11    {
    1.12 @@ -33,7 +33,8 @@
    1.13        else {
    1.14          val selection = Sessions.Selection(sessions = List(logic_name))
    1.15          val selected_sessions =
    1.16 -          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
    1.17 +          sessions_structure.getOrElse(Sessions.load_structure(options, dirs = dirs))
    1.18 +            .selection(selection)
    1.19          selected_sessions.build_requirements(List(logic_name)).
    1.20            map(a => File.platform_path(store.heap(a)))
    1.21        }
     2.1 --- a/src/Pure/System/isabelle_process.scala	Thu May 17 14:50:48 2018 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Thu May 17 15:38:36 2018 +0200
     2.3 @@ -20,7 +20,7 @@
     2.4      modes: List[String] = Nil,
     2.5      cwd: JFile = null,
     2.6      env: Map[String, String] = Isabelle_System.settings(),
     2.7 -    sessions: Option[Sessions.Structure] = None,
     2.8 +    sessions_structure: Option[Sessions.Structure] = None,
     2.9      store: Sessions.Store = Sessions.store(),
    2.10      phase_changed: Session.Phase => Unit = null)
    2.11    {
    2.12 @@ -30,7 +30,7 @@
    2.13      session.start(receiver =>
    2.14        Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
    2.15          cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
    2.16 -        sessions = sessions, store = store))
    2.17 +        sessions_structure = sessions_structure, store = store))
    2.18    }
    2.19  
    2.20    def apply(
    2.21 @@ -43,14 +43,14 @@
    2.22      env: Map[String, String] = Isabelle_System.settings(),
    2.23      receiver: Prover.Receiver = (msg: Prover.Message) => Output.writeln(msg.toString, stdout = true),
    2.24      xml_cache: XML.Cache = XML.make_cache(),
    2.25 -    sessions: Option[Sessions.Structure] = None,
    2.26 +    sessions_structure: Option[Sessions.Structure] = None,
    2.27      store: Sessions.Store = Sessions.store()): Prover =
    2.28    {
    2.29      val channel = System_Channel()
    2.30      val process =
    2.31        try {
    2.32 -        ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
    2.33 -          cwd = cwd, env = env, sessions = sessions, store = store, channel = Some(channel))
    2.34 +        ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes, cwd = cwd,
    2.35 +          env = env, sessions_structure = sessions_structure, store = store, channel = Some(channel))
    2.36        }
    2.37        catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
    2.38      process.stdin.close
     3.1 --- a/src/Pure/Thy/sessions.scala	Thu May 17 14:50:48 2018 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Thu May 17 15:38:36 2018 +0200
     3.3 @@ -168,7 +168,8 @@
     3.4      def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
     3.5    }
     3.6  
     3.7 -  sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
     3.8 +  sealed case class Deps(
     3.9 +    sessions_structure: Structure, session_bases: Map[String, Base], all_known: Known)
    3.10    {
    3.11      def is_empty: Boolean = session_bases.isEmpty
    3.12      def apply(name: String): Base = session_bases(name)
    3.13 @@ -351,7 +352,7 @@
    3.14            }
    3.15        })
    3.16  
    3.17 -    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
    3.18 +    Deps(sessions_structure, session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
    3.19    }
    3.20  
    3.21  
    3.22 @@ -448,7 +449,7 @@
    3.23      val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
    3.24      val base1 = deps1(session1).copy(known = deps1.all_known)
    3.25  
    3.26 -    Base_Info(options, dirs, session1, sessions1, deps1.errors, base1, infos1)
    3.27 +    Base_Info(options, dirs, session1, deps1.sessions_structure, deps1.errors, base1, infos1)
    3.28    }
    3.29  
    3.30  
     4.1 --- a/src/Pure/Tools/build.scala	Thu May 17 14:50:48 2018 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Thu May 17 15:38:36 2018 +0200
     4.3 @@ -174,7 +174,6 @@
     4.4    private class Job(progress: Progress,
     4.5      name: String,
     4.6      val info: Sessions.Info,
     4.7 -    sessions: Sessions.Structure,
     4.8      deps: Sessions.Deps,
     4.9      store: Sessions.Store,
    4.10      do_output: Boolean,
    4.11 @@ -238,8 +237,8 @@
    4.12  
    4.13            val session_result = Future.promise[Process_Result]
    4.14  
    4.15 -          Isabelle_Process.start(session, options, logic = parent,
    4.16 -            cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
    4.17 +          Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
    4.18 +            sessions_structure = Some(deps.sessions_structure), store = store,
    4.19              phase_changed =
    4.20              {
    4.21                case Session.Ready => session.protocol_command("build_session", args_yxml)
    4.22 @@ -272,12 +271,12 @@
    4.23                  args =
    4.24                    (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
    4.25                    List("--eval", eval),
    4.26 -                env = env, sessions = Some(sessions), store = store,
    4.27 +                env = env, sessions_structure = Some(deps.sessions_structure), store = store,
    4.28                  cleanup = () => args_file.delete)
    4.29              }
    4.30              else {
    4.31                ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
    4.32 -                env = env, sessions = Some(sessions), store = store,
    4.33 +                env = env, sessions_structure = Some(deps.sessions_structure), store = store,
    4.34                  cleanup = () => args_file.delete)
    4.35              }
    4.36  
    4.37 @@ -413,17 +412,16 @@
    4.38        Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    4.39          exclude_sessions, session_groups, sessions) ++ selection
    4.40  
    4.41 -    val (selected_sessions, deps) =
    4.42 +    val deps =
    4.43      {
    4.44 -      val selected_sessions0 = full_sessions.selection(selection1)
    4.45        val deps0 =
    4.46 -        Sessions.deps(selected_sessions0, full_sessions.global_theories,
    4.47 +        Sessions.deps(full_sessions.selection(selection1), full_sessions.global_theories,
    4.48            progress = progress, inlined_files = true, verbose = verbose,
    4.49            list_files = list_files, check_keywords = check_keywords).check_errors
    4.50  
    4.51        if (soft_build && !fresh_build) {
    4.52          val outdated =
    4.53 -          selected_sessions0.build_topological_order.flatMap(name =>
    4.54 +          deps0.sessions_structure.build_topological_order.flatMap(name =>
    4.55              store.find_database(name) match {
    4.56                case Some(database) =>
    4.57                  using(SQLite.open_database(database))(store.read_build(_, name)) match {
    4.58 @@ -433,14 +431,11 @@
    4.59                  }
    4.60                case None => Some(name)
    4.61              })
    4.62 -        val selected_sessions =
    4.63 -          full_sessions.selection(Sessions.Selection(sessions = outdated))
    4.64 -        val deps =
    4.65 -          Sessions.deps(selected_sessions, full_sessions.global_theories,
    4.66 -            progress = progress, inlined_files = true).check_errors
    4.67 -        (selected_sessions, deps)
    4.68 +
    4.69 +        Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
    4.70 +          full_sessions.global_theories, progress = progress, inlined_files = true).check_errors
    4.71        }
    4.72 -      else (selected_sessions0, deps0)
    4.73 +      else deps0
    4.74      }
    4.75  
    4.76  
    4.77 @@ -465,7 +460,7 @@
    4.78  
    4.79      /* main build process */
    4.80  
    4.81 -    val queue = Queue(progress, selected_sessions, store)
    4.82 +    val queue = Queue(progress, deps.sessions_structure, store)
    4.83  
    4.84      store.prepare_output()
    4.85  
    4.86 @@ -592,7 +587,7 @@
    4.87              pending.dequeue(running.isDefinedAt(_)) match {
    4.88                case Some((name, info)) =>
    4.89                  val ancestor_results =
    4.90 -                  selected_sessions.build_requirements(List(name)).filterNot(_ == name).
    4.91 +                  deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
    4.92                      map(results(_))
    4.93                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
    4.94  
    4.95 @@ -636,7 +631,7 @@
    4.96  
    4.97                    val numa_node = numa_nodes.next(used_node(_))
    4.98                    val job =
    4.99 -                    new Job(progress, name, info, selected_sessions, deps, store, do_output,
   4.100 +                    new Job(progress, name, info, deps, store, do_output,
   4.101                        verbose, pide, numa_node, queue.command_timings(name))
   4.102                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
   4.103                  }
     5.1 --- a/src/Pure/Tools/imports.scala	Thu May 17 14:50:48 2018 +0200
     5.2 +++ b/src/Pure/Tools/imports.scala	Thu May 17 15:38:36 2018 +0200
     5.3 @@ -100,23 +100,22 @@
     5.4      verbose: Boolean = false) =
     5.5    {
     5.6      val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
     5.7 -    val selected_sessions = full_sessions.selection(selection)
     5.8  
     5.9      val deps =
    5.10 -      Sessions.deps(selected_sessions, full_sessions.global_theories,
    5.11 +      Sessions.deps(full_sessions.selection(selection), full_sessions.global_theories,
    5.12          progress = progress, verbose = verbose).check_errors
    5.13  
    5.14      val root_keywords = Sessions.root_syntax.keywords
    5.15  
    5.16      if (operation_imports) {
    5.17        val report_imports: List[Report] =
    5.18 -        selected_sessions.build_topological_order.map((session_name: String) =>
    5.19 +        deps.sessions_structure.build_topological_order.map((session_name: String) =>
    5.20            {
    5.21 -            val info = selected_sessions(session_name)
    5.22 +            val info = deps.sessions_structure(session_name)
    5.23              val session_base = deps(session_name)
    5.24  
    5.25              val declared_imports =
    5.26 -              selected_sessions.imports_requirements(List(session_name)).toSet
    5.27 +              deps.sessions_structure.imports_requirements(List(session_name)).toSet
    5.28  
    5.29              val extra_imports =
    5.30                (for {
    5.31 @@ -128,18 +127,18 @@
    5.32                } yield qualifier).toSet
    5.33  
    5.34              val loaded_imports =
    5.35 -              selected_sessions.imports_requirements(
    5.36 +              deps.sessions_structure.imports_requirements(
    5.37                  session_base.loaded_theories.keys.map(a =>
    5.38                    session_base.theory_qualifier(session_base.known.theories(a))))
    5.39                .toSet - session_name
    5.40  
    5.41              val minimal_imports =
    5.42                loaded_imports.filter(s1 =>
    5.43 -                !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    5.44 +                !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2)))
    5.45  
    5.46              def make_result(set: Set[String]): Option[List[String]] =
    5.47                if (set.isEmpty) None
    5.48 -              else Some(selected_sessions.imports_topological_order.filter(set))
    5.49 +              else Some(deps.sessions_structure.imports_topological_order.filter(set))
    5.50  
    5.51              Report(info, declared_imports, make_result(extra_imports),
    5.52                if (loaded_imports == declared_imports - session_name) None
    5.53 @@ -173,9 +172,9 @@
    5.54      if (operation_update) {
    5.55        progress.echo("\nUpdate theory imports" + update_message + ":")
    5.56        val updates =
    5.57 -        selected_sessions.build_topological_order.flatMap(session_name =>
    5.58 +        deps.sessions_structure.build_topological_order.flatMap(session_name =>
    5.59            {
    5.60 -            val info = selected_sessions(session_name)
    5.61 +            val info = deps.sessions_structure(session_name)
    5.62              val session_base = deps(session_name)
    5.63              val session_resources = new Resources(session_base)
    5.64              val imports_base = session_base.get_imports
     6.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Thu May 17 14:50:48 2018 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu May 17 15:38:36 2018 +0200
     6.3 @@ -133,7 +133,7 @@
     6.4    def session_start(options: Options)
     6.5    {
     6.6      Isabelle_Process.start(PIDE.session, session_options(options),
     6.7 -      sessions = Some(PIDE.resources.session_base_info.sessions_structure),
     6.8 +      sessions_structure = Some(PIDE.resources.session_base_info.sessions_structure),
     6.9        logic = PIDE.resources.session_name,
    6.10        store = Sessions.store(session_build_mode() == "system"),
    6.11        modes =