tuned signature;
authorwenzelm
Mon Mar 11 16:47:22 2019 +0100 (3 months ago ago)
changeset 70078a9849222844d
parent 70077 be7243b97c41
child 70079 990c6e8faf2c
tuned signature;
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Mon Mar 11 16:23:30 2019 +0100
     1.2 +++ b/src/Pure/Tools/dump.scala	Mon Mar 11 16:47:22 2019 +0100
     1.3 @@ -91,7 +91,10 @@
     1.4    /* session */
     1.5  
     1.6    sealed case class Args(
     1.7 -    deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status)
     1.8 +    session: Headless.Session,
     1.9 +    deps: Sessions.Deps,
    1.10 +    snapshot: Document.Snapshot,
    1.11 +    status: Document_Status.Node_Status)
    1.12    {
    1.13      def print_node: String = snapshot.node_name.toString
    1.14  
    1.15 @@ -105,6 +108,9 @@
    1.16      process_theory: Args => Unit,
    1.17      progress: Progress = No_Progress)
    1.18    {
    1.19 +    val session = resources.start_session(progress = progress)
    1.20 +
    1.21 +
    1.22      /* asynchronous consumer */
    1.23  
    1.24      object Consumer
    1.25 @@ -123,7 +129,7 @@
    1.26                val (snapshot, status) = args
    1.27                val name = snapshot.node_name
    1.28                if (status.ok) {
    1.29 -                try { process_theory(Args(deps, snapshot, status)) }
    1.30 +                try { process_theory(Args(session, deps, snapshot, status)) }
    1.31                  catch {
    1.32                    case exn: Throwable if !Exn.is_interrupt(exn) =>
    1.33                    val msg = Exn.message(exn)
    1.34 @@ -159,7 +165,6 @@
    1.35  
    1.36      /* run session */
    1.37  
    1.38 -    val session = resources.start_session(progress = progress)
    1.39      try {
    1.40        val use_theories = resources.used_theories(deps).map(_.theory)
    1.41        val use_theories_result =