dump aspects asynchronously;
authorwenzelm
Fri Sep 07 17:08:47 2018 +0200 (10 months ago)
changeset 689265129fcc1b6c0
parent 68925 76ce16eefab9
child 68927 01f46a4b22b4
dump aspects asynchronously;
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Fri Sep 07 17:05:02 2018 +0200
     1.2 +++ b/src/Pure/Tools/dump.scala	Fri Sep 07 17:08:47 2018 +0200
     1.3 @@ -115,34 +115,56 @@
     1.4          flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
     1.5  
     1.6  
     1.7 +    /* dump aspects asynchronously */
     1.8 +
     1.9 +    object Consumer
    1.10 +    {
    1.11 +      private val errors = Synchronized[List[String]](Nil)
    1.12 +
    1.13 +      private val consumer =
    1.14 +        Consumer_Thread.fork(name = "dump")(
    1.15 +          consume = (args: (Document.Snapshot, Document_Status.Node_Status)) =>
    1.16 +            {
    1.17 +              val (snapshot, node_status) = args
    1.18 +              if (node_status.ok) {
    1.19 +                val aspect_args =
    1.20 +                  Aspect_Args(dump_options, progress, deps, output_dir,
    1.21 +                    snapshot.node_name, node_status, snapshot)
    1.22 +                aspects.foreach(_.operation(aspect_args))
    1.23 +              }
    1.24 +              for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) {
    1.25 +                val msg = XML.content(Pretty.formatted(List(tree)))
    1.26 +                errors.change(("Error" + Position.here(pos) + ":\n" + msg) :: _)
    1.27 +              }
    1.28 +              true
    1.29 +            })
    1.30 +
    1.31 +      def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit =
    1.32 +        consumer.send((snapshot, node_status))
    1.33 +
    1.34 +      def shutdown(): List[String] =
    1.35 +      {
    1.36 +        consumer.shutdown()
    1.37 +        errors.value.reverse
    1.38 +      }
    1.39 +    }
    1.40 +
    1.41 +
    1.42      /* session */
    1.43  
    1.44      val session =
    1.45        Thy_Resources.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs,
    1.46          include_sessions = include_sessions, progress = progress, log = log)
    1.47  
    1.48 -    val theories_result = session.use_theories(use_theories, progress = progress)
    1.49 +    val theories_result =
    1.50 +      session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
    1.51 +
    1.52      val session_result = session.stop()
    1.53  
    1.54 -
    1.55 -    /* dump aspects */
    1.56 -
    1.57 -    for ((node_name, node_status) <- theories_result.nodes) {
    1.58 -      val snapshot = theories_result.snapshot(node_name)
    1.59 -      val aspect_args =
    1.60 -        Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot)
    1.61 -      aspects.foreach(_.operation(aspect_args))
    1.62 -    }
    1.63 +    Consumer.shutdown().foreach(progress.echo_error_message(_))
    1.64  
    1.65      if (theories_result.ok) session_result
    1.66 -    else {
    1.67 -      for {
    1.68 -        (name, status) <- theories_result.nodes if !status.ok
    1.69 -        (tree, _) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
    1.70 -      } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
    1.71 -
    1.72 -      session_result.copy(rc = session_result.rc max 1)
    1.73 -    }
    1.74 +    else session_result.copy(rc = session_result.rc max 1)
    1.75    }
    1.76  
    1.77