tuned signature;
authorwenzelm
Mon Mar 11 16:23:30 2019 +0100 (6 weeks ago ago)
changeset 70077be7243b97c41
parent 70076 6b03a8cf092d
child 70078 a9849222844d
tuned signature;
src/Pure/Tools/dump.scala
src/Pure/Tools/update.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Sun Mar 10 23:23:03 2019 +0100
     1.2 +++ b/src/Pure/Tools/dump.scala	Mon Mar 11 16:23:30 2019 +0100
     1.3 @@ -14,8 +14,8 @@
     1.4    sealed case class Aspect_Args(
     1.5      options: Options,
     1.6      progress: Progress,
     1.7 +    output_dir: Path,
     1.8      deps: Sessions.Deps,
     1.9 -    output_dir: Path,
    1.10      snapshot: Document.Snapshot,
    1.11      status: Document_Status.Node_Status)
    1.12    {
    1.13 @@ -90,10 +90,19 @@
    1.14  
    1.15    /* session */
    1.16  
    1.17 +  sealed case class Args(
    1.18 +    deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status)
    1.19 +  {
    1.20 +    def print_node: String = snapshot.node_name.toString
    1.21 +
    1.22 +    def aspect_args(options: Options, progress: Progress, output_dir: Path): Aspect_Args =
    1.23 +      Aspect_Args(options, progress, output_dir, deps, snapshot, status)
    1.24 +  }
    1.25 +
    1.26    def session(
    1.27      deps: Sessions.Deps,
    1.28      resources: Headless.Resources,
    1.29 -    process_theory: (Sessions.Deps, Document.Snapshot, Document_Status.Node_Status) => Unit,
    1.30 +    process_theory: Args => Unit,
    1.31      progress: Progress = No_Progress)
    1.32    {
    1.33      /* asynchronous consumer */
    1.34 @@ -114,7 +123,7 @@
    1.35                val (snapshot, status) = args
    1.36                val name = snapshot.node_name
    1.37                if (status.ok) {
    1.38 -                try { process_theory(deps, snapshot, status) }
    1.39 +                try { process_theory(Args(deps, snapshot, status)) }
    1.40                  catch {
    1.41                    case exn: Throwable if !Exn.is_interrupt(exn) =>
    1.42                    val msg = Exn.message(exn)
    1.43 @@ -214,12 +223,11 @@
    1.44          include_sessions = deps.sessions_structure.imports_topological_order)
    1.45  
    1.46      session(deps, resources, progress = progress,
    1.47 -      process_theory =
    1.48 -        (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) =>
    1.49 +      process_theory = (args: Args) =>
    1.50          {
    1.51 -          progress.echo("Processing theory " + snapshot.node_name + " ...")
    1.52 +          progress.echo("Processing theory " + args.print_node + " ...")
    1.53  
    1.54 -          val aspect_args = Aspect_Args(dump_options, progress, deps, output_dir, snapshot, status)
    1.55 +          val aspect_args = args.aspect_args(dump_options, progress, output_dir)
    1.56            aspects.foreach(_.operation(aspect_args))
    1.57          })
    1.58    }
     2.1 --- a/src/Pure/Tools/update.scala	Sun Mar 10 23:23:03 2019 +0100
     2.2 +++ b/src/Pure/Tools/update.scala	Mon Mar 11 16:23:30 2019 +0100
     2.3 @@ -47,11 +47,11 @@
     2.4        }
     2.5  
     2.6      Dump.session(deps, resources, progress = progress,
     2.7 -      process_theory =
     2.8 -        (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) =>
     2.9 +      process_theory = (args: Dump.Args) =>
    2.10          {
    2.11 -          progress.echo("Processing theory " + snapshot.node_name + " ...")
    2.12 +          progress.echo("Processing theory " + args.print_node + " ...")
    2.13  
    2.14 +          val snapshot = args.snapshot
    2.15            for ((node_name, node) <- snapshot.nodes) {
    2.16              val xml =
    2.17                snapshot.state.markup_to_XML(snapshot.version, node_name,