tuned signature;
authorwenzelm
Sun Mar 03 18:45:08 2019 +0100 (7 weeks ago ago)
changeset 70037bb41977edb7e
parent 70036 60b924cda764
child 70038 a4b430ad848a
tuned signature;
src/Pure/Tools/dump.scala
src/Pure/Tools/update.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Sun Mar 03 16:00:14 2019 +0100
     1.2 +++ b/src/Pure/Tools/dump.scala	Sun Mar 03 18:45:08 2019 +0100
     1.3 @@ -75,28 +75,22 @@
     1.4  
     1.5    /* dependencies */
     1.6  
     1.7 -  def used_theories(options: Options, deps: Sessions.Deps, progress: Progress = No_Progress)
     1.8 -    : List[Document.Node.Name] =
     1.9 -  {
    1.10 -    deps.used_theories_condition(options, progress.echo_warning).map(_._2)
    1.11 -  }
    1.12 -
    1.13    def dependencies(
    1.14      options: Options,
    1.15      progress: Progress = No_Progress,
    1.16      dirs: List[Path] = Nil,
    1.17      select_dirs: List[Path] = Nil,
    1.18 -    selection: Sessions.Selection = Sessions.Selection.empty)
    1.19 -      : (Sessions.Deps, List[Document.Node.Name]) =
    1.20 +    selection: Sessions.Selection = Sessions.Selection.empty): Sessions.Deps =
    1.21    {
    1.22 -    val deps =
    1.23 -      Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
    1.24 -        selection_deps(options, selection, progress = progress,
    1.25 -          uniform_session = true, loading_sessions = true)
    1.26 +    Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
    1.27 +      selection_deps(options, selection, progress = progress,
    1.28 +        uniform_session = true, loading_sessions = true)
    1.29 +  }
    1.30  
    1.31 -    val theories = used_theories(options, deps, progress = progress)
    1.32 -
    1.33 -    (deps, theories)
    1.34 +  def used_theories(options: Options, deps: Sessions.Deps, progress: Progress = No_Progress)
    1.35 +    : List[Document.Node.Name] =
    1.36 +  {
    1.37 +    deps.used_theories_condition(options, progress.echo_warning).map(_._2)
    1.38    }
    1.39  
    1.40  
    1.41 @@ -218,7 +212,7 @@
    1.42  
    1.43      val deps =
    1.44        dependencies(dump_options, progress = progress,
    1.45 -        dirs = dirs, select_dirs = select_dirs, selection = selection)._1
    1.46 +        dirs = dirs, select_dirs = select_dirs, selection = selection)
    1.47  
    1.48      val resources =
    1.49        Headless.Resources.make(dump_options, logic, progress = progress, log = log,
     2.1 --- a/src/Pure/Tools/update.scala	Sun Mar 03 16:00:14 2019 +0100
     2.2 +++ b/src/Pure/Tools/update.scala	Sun Mar 03 18:45:08 2019 +0100
     2.3 @@ -23,7 +23,7 @@
     2.4  
     2.5      val deps =
     2.6        Dump.dependencies(dump_options, progress = progress,
     2.7 -        dirs = dirs, select_dirs = select_dirs, selection = selection)._1
     2.8 +        dirs = dirs, select_dirs = select_dirs, selection = selection)
     2.9  
    2.10      val resources =
    2.11        Headless.Resources.make(dump_options, logic, progress = progress, log = log,