clarified signature: global_theories is always required;
authorwenzelm
Tue Oct 31 17:15:49 2017 +0100 (19 months ago)
changeset 66962e1bde71bace6
parent 66961 f855f9aed72f
child 66963 1c3d0c12bb51
clarified signature: global_theories is always required;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 17:03:57 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 17:15:49 2017 +0100
     1.3 @@ -171,12 +171,12 @@
     1.4    }
     1.5  
     1.6    def deps(sessions: T,
     1.7 +      global_theories: Map[String, String],
     1.8        progress: Progress = No_Progress,
     1.9        inlined_files: Boolean = false,
    1.10        verbose: Boolean = false,
    1.11        list_files: Boolean = false,
    1.12 -      check_keywords: Set[String] = Set.empty,
    1.13 -      global_theories: Map[String, String] = Map.empty): Deps =
    1.14 +      check_keywords: Set[String] = Set.empty): Deps =
    1.15    {
    1.16      var cache_sources = Map.empty[JFile, SHA1.Digest]
    1.17      def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] =
    1.18 @@ -330,8 +330,7 @@
    1.19      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    1.20  
    1.21      val sessions: T = if (all_known) full_sessions else selected_sessions
    1.22 -    val deps =
    1.23 -      Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories)
    1.24 +    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
    1.25      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    1.26      (deps.errors, base)
    1.27    }
     2.1 --- a/src/Pure/Tools/build.scala	Tue Oct 31 17:03:57 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Tue Oct 31 17:15:49 2017 +0100
     2.3 @@ -398,9 +398,9 @@
     2.4                exclude_sessions, session_groups, sessions) ++ selection)
     2.5  
     2.6        val deps0 =
     2.7 -        Sessions.deps(selected_sessions0, progress = progress, inlined_files = true,
     2.8 -          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
     2.9 -          global_theories = full_sessions.global_theories).check_errors
    2.10 +        Sessions.deps(selected_sessions0, full_sessions.global_theories,
    2.11 +          progress = progress, inlined_files = true, verbose = verbose,
    2.12 +          list_files = list_files, check_keywords = check_keywords).check_errors
    2.13  
    2.14        if (soft_build && !fresh_build) {
    2.15          val outdated =
    2.16 @@ -417,8 +417,8 @@
    2.17          val (selected, selected_sessions) =
    2.18            full_sessions.selection(Sessions.Selection(sessions = outdated))
    2.19          val deps =
    2.20 -          Sessions.deps(selected_sessions, inlined_files = true,
    2.21 -            global_theories = full_sessions.global_theories).check_errors
    2.22 +          Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
    2.23 +            .check_errors
    2.24          (selected, selected_sessions, deps)
    2.25        }
    2.26        else (selected0, selected_sessions0, deps0)
     3.1 --- a/src/Pure/Tools/imports.scala	Tue Oct 31 17:03:57 2017 +0100
     3.2 +++ b/src/Pure/Tools/imports.scala	Tue Oct 31 17:15:49 2017 +0100
     3.3 @@ -103,8 +103,8 @@
     3.4      val (selected, selected_sessions) = full_sessions.selection(selection)
     3.5  
     3.6      val deps =
     3.7 -      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
     3.8 -        global_theories = full_sessions.global_theories).check_errors
     3.9 +      Sessions.deps(selected_sessions, full_sessions.global_theories,
    3.10 +        progress = progress, verbose = verbose).check_errors
    3.11  
    3.12      val root_keywords = Sessions.root_syntax.keywords
    3.13