more args;
authorwenzelm
Sat Jun 02 22:11:09 2018 +0200 (14 months ago)
changeset 6835567a4db47e4f6
parent 68354 93d3c967802e
child 68356 46d5a9f428e1
more args;
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Sat Jun 02 21:59:11 2018 +0200
     1.2 +++ b/src/Pure/Tools/dump.scala	Sat Jun 02 22:11:09 2018 +0200
     1.3 @@ -12,7 +12,11 @@
     1.4    /* aspects */
     1.5  
     1.6    sealed case class Aspect_Args(
     1.7 -    options: Options, progress: Progress, output_dir: Path, result: Thy_Resources.Theories_Result)
     1.8 +    options: Options,
     1.9 +    progress: Progress,
    1.10 +    output_dir: Path,
    1.11 +    deps: Sessions.Deps,
    1.12 +    result: Thy_Resources.Theories_Result)
    1.13    {
    1.14      def write(node_name: Document.Node.Name, file_name: Path, bytes: Bytes)
    1.15      {
    1.16 @@ -125,7 +129,7 @@
    1.17  
    1.18      /* dump aspects */
    1.19  
    1.20 -    val aspect_args = Aspect_Args(dump_options, progress, output_dir, theories_result)
    1.21 +    val aspect_args = Aspect_Args(dump_options, progress, output_dir, deps, theories_result)
    1.22      aspects.foreach(_.operation(aspect_args))
    1.23  
    1.24      session_result