# HG changeset patch # User wenzelm # Date 1536344062 -7200 # Node ID e609c3dec6f828c0bc7dc5ffb74564bd23c62139 # Parent 35ea237696cf6337d8ea4802d360ba5d305b5a3f# Parent fc5763d000e817a9813f1161bc97d6d941456241 merged diff -r 35ea237696cf -r e609c3dec6f8 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Sep 07 13:27:41 2018 +0200 +++ b/src/Pure/PIDE/command.ML Fri Sep 07 20:14:22 2018 +0200 @@ -452,7 +452,7 @@ fun run_process execution_id exec_id process = let val group = Future.worker_subgroup () in if Execution.running execution_id exec_id [group] then - ignore (task_context group Lazy.force_result {strict = true} process) + ignore (task_context group (fn () => Lazy.force_result {strict = true} process) ()) else () end; diff -r 35ea237696cf -r e609c3dec6f8 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Fri Sep 07 13:27:41 2018 +0200 +++ b/src/Pure/System/process_result.scala Fri Sep 07 20:14:22 2018 +0200 @@ -23,6 +23,8 @@ def ok: Boolean = rc == 0 def interrupted: Boolean = rc == Exn.Interrupt.return_code + def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1) + def check_rc(pred: Int => Boolean): Process_Result = if (pred(rc)) this else if (interrupted) throw Exn.Interrupt() diff -r 35ea237696cf -r e609c3dec6f8 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Fri Sep 07 13:27:41 2018 +0200 +++ b/src/Pure/Thy/export.scala Fri Sep 07 20:14:22 2018 +0200 @@ -167,7 +167,7 @@ class Consumer private[Export](db: SQL.Database, cache: XZ.Cache) { - private val export_errors = Synchronized[List[String]](Nil) + private val errors = Synchronized[List[String]](Nil) private val consumer = Consumer_Thread.fork(name = "export")(consume = (entry: Entry) => @@ -175,8 +175,8 @@ entry.body.join db.transaction { if (read_name(db, entry.session_name, entry.theory_name, entry.name)) { - val err = message("Duplicate export", entry.theory_name, entry.name) - export_errors.change(errs => err :: errs) + val msg = message("Duplicate export", entry.theory_name, entry.name) + errors.change(msg :: _) } else entry.write(db) } @@ -190,7 +190,7 @@ { consumer.shutdown() if (close) db.close() - export_errors.value.reverse + errors.value.reverse } } diff -r 35ea237696cf -r e609c3dec6f8 src/Pure/Thy/thy_resources.scala --- a/src/Pure/Thy/thy_resources.scala Fri Sep 07 13:27:41 2018 +0200 +++ b/src/Pure/Thy/thy_resources.scala Fri Sep 07 20:14:22 2018 +0200 @@ -66,11 +66,14 @@ class Theories_Result private[Thy_Resources]( val state: Document.State, val version: Document.Version, - val nodes: List[(Document.Node.Name, Document_Status.Node_Status)]) + val nodes: List[(Document.Node.Name, Document_Status.Node_Status)], + val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)]) { - def node_names: List[Document.Node.Name] = nodes.map(_._1) - def ok: Boolean = nodes.forall({ case (_, st) => st.ok }) - def snapshot(name: Document.Node.Name): Document.Snapshot = stable_snapshot(state, version, name) + def snapshot(name: Document.Node.Name): Document.Snapshot = + stable_snapshot(state, version, name) + + def ok: Boolean = + (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) } val default_check_delay: Double = 0.5 @@ -84,9 +87,15 @@ { session => + + /* temporary directory */ + val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session") val tmp_dir_name: String = File.path(tmp_dir).implode + def master_directory(master_dir: String): String = + proper_string(master_dir) getOrElse tmp_dir_name + override def toString: String = session_name override def stop(): Process_Result = @@ -102,7 +111,7 @@ last_update: Time = Time.now(), nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, already_initialized: Set[Document.Node.Name] = Set.empty, - already_committed: Set[Document.Node.Name] = Set.empty, + already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, result: Promise[Theories_Result] = Future.promise[Theories_Result]) { def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = @@ -131,7 +140,7 @@ def check_result( state: Document.State, version: Document.Version, - theories: List[Document.Node.Name], + dep_theories: List[Document.Node.Name], beyond_limit: Boolean, watchdog_timeout: Time, commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit]) @@ -141,29 +150,35 @@ if (commit.isDefined) { val committed = for { - name <- theories - if !already_committed(name) && state.node_consolidated(version, name) + name <- dep_theories + if !already_committed.isDefinedAt(name) && state.node_consolidated(version, name) } yield { val snapshot = stable_snapshot(state, version, name) val status = Document_Status.Node_Status.make(state, version, name) commit.get.apply(snapshot, status) - name + (name -> status) } copy(already_committed = already_committed ++ committed) } else this if (beyond_limit || watchdog(watchdog_timeout) || - theories.forall(name => - already_committed(name) || + dep_theories.forall(name => + already_committed.isDefinedAt(name) || state.node_consolidated(version, name) || nodes_status.quasi_consolidated(name))) { val nodes = - for (name <- theories) + for (name <- dep_theories) yield { (name -> Document_Status.Node_Status.make(state, version, name)) } - try { result.fulfill(new Theories_Result(state, version, nodes)) } + val nodes_committed = + for { + name <- dep_theories + status <- already_committed.get(name) + } yield (name -> status) + + try { result.fulfill(new Theories_Result(state, version, nodes, nodes_committed)) } catch { case _: IllegalStateException => } } @@ -186,9 +201,9 @@ { val dep_theories = { - val master = proper_string(master_dir) getOrElse tmp_dir_name val import_names = - theories.map(thy => resources.import_name(qualifier, master, thy) -> Position.none) + theories.map(thy => + resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) resources.dependencies(import_names, progress = progress).check_errors.theories } val dep_theories_set = dep_theories.toSet @@ -300,8 +315,9 @@ master_dir: String = "", all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) = { - val master = proper_string(master_dir) getOrElse tmp_dir_name - val nodes = if (all) None else Some(theories.map(resources.import_name(qualifier, master, _))) + val nodes = + if (all) None + else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _))) resources.purge_theories(session, nodes) } } @@ -309,6 +325,40 @@ /* internal state */ + final class Theory private[Thy_Resources]( + val node_name: Document.Node.Name, + val node_header: Document.Node.Header, + val text: String, + val node_required: Boolean) + { + override def toString: String = node_name.toString + + def node_perspective: Document.Node.Perspective_Text = + Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) + + def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = + List(node_name -> Document.Node.Deps(node_header), + node_name -> Document.Node.Edits(text_edits), + node_name -> node_perspective) + + def node_edits(old: Option[Theory]): List[Document.Edit_Text] = + { + val (text_edits, old_required) = + if (old.isEmpty) (Text.Edit.inserts(0, text), false) + else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) + + if (text_edits.isEmpty && node_required == old_required) Nil + else make_edits(text_edits) + } + + def purge_edits: List[Document.Edit_Text] = + make_edits(Text.Edit.removes(0, text)) + + def required(required: Boolean): Theory = + if (required == node_required) this + else new Theory(node_name, node_header, text, required) + } + sealed case class State( required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty, theories: Map[Document.Node.Name, Theory] = Map.empty) @@ -344,40 +394,6 @@ Graph.make(entries, symmetric = true)(Document.Node.Name.Ordering) } } - - final class Theory private[Thy_Resources]( - val node_name: Document.Node.Name, - val node_header: Document.Node.Header, - val text: String, - val node_required: Boolean) - { - override def toString: String = node_name.toString - - def node_perspective: Document.Node.Perspective_Text = - Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) - - def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = - List(node_name -> Document.Node.Deps(node_header), - node_name -> Document.Node.Edits(text_edits), - node_name -> node_perspective) - - def node_edits(old: Option[Theory]): List[Document.Edit_Text] = - { - val (text_edits, old_required) = - if (old.isEmpty) (Text.Edit.inserts(0, text), false) - else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) - - if (text_edits.isEmpty && node_required == old_required) Nil - else make_edits(text_edits) - } - - def purge_edits: List[Document.Edit_Text] = - make_edits(Text.Edit.removes(0, text)) - - def required(required: Boolean): Theory = - if (required == node_required) this - else new Theory(node_name, node_header, text, required) - } } class Thy_Resources(session_base: Sessions.Base, log: Logger = No_Logger) diff -r 35ea237696cf -r e609c3dec6f8 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Sep 07 13:27:41 2018 +0200 +++ b/src/Pure/Tools/build.scala Fri Sep 07 20:14:22 2018 +0200 @@ -332,8 +332,7 @@ val result1 = export_consumer.shutdown(close = true).map(Output.error_message_text(_)) match { case Nil => result0 - case errs if result0.ok => result0.copy(rc = 1).errors(errs) - case errs => result0.errors(errs) + case errs => result0.errors(errs).error_rc } Isabelle_System.rm_tree(export_tmp_dir) diff -r 35ea237696cf -r e609c3dec6f8 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Fri Sep 07 13:27:41 2018 +0200 +++ b/src/Pure/Tools/dump.scala Fri Sep 07 20:14:22 2018 +0200 @@ -16,13 +16,12 @@ progress: Progress, deps: Sessions.Deps, output_dir: Path, - node_name: Document.Node.Name, - node_status: Document_Status.Node_Status, - snapshot: Document.Snapshot) + snapshot: Document.Snapshot, + node_status: Document_Status.Node_Status) { def write(file_name: Path, bytes: Bytes) { - val path = output_dir + Path.basic(node_name.theory) + file_name + val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name Isabelle_System.mkdirs(path.dir) Bytes.write(path, bytes) } @@ -115,34 +114,58 @@ flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory)) + /* dump aspects asynchronously */ + + object Consumer + { + private val consumer_ok = Synchronized(true) + + private val consumer = + Consumer_Thread.fork(name = "dump")( + consume = (args: (Document.Snapshot, Document_Status.Node_Status)) => + { + val (snapshot, node_status) = args + if (node_status.ok) { + val aspect_args = + Aspect_Args(dump_options, progress, deps, output_dir, snapshot, node_status) + aspects.foreach(_.operation(aspect_args)) + } + else { + consumer_ok.change(_ => false) + for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) { + val msg = XML.content(Pretty.formatted(List(tree))) + progress.echo_error_message("Error" + Position.here(pos) + ":\n" + msg) + } + } + true + }) + + def apply(snapshot: Document.Snapshot, node_status: Document_Status.Node_Status): Unit = + consumer.send((snapshot, node_status)) + + def shutdown(): Boolean = + { + consumer.shutdown() + consumer_ok.value + } + } + + /* session */ val session = Thy_Resources.start_session(dump_options, logic, session_dirs = dirs ::: select_dirs, include_sessions = include_sessions, progress = progress, log = log) - val theories_result = session.use_theories(use_theories, progress = progress) + val theories_result = + session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _)) + val session_result = session.stop() - - /* dump aspects */ - - for ((node_name, node_status) <- theories_result.nodes) { - val snapshot = theories_result.snapshot(node_name) - val aspect_args = - Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot) - aspects.foreach(_.operation(aspect_args)) - } + val consumer_ok = Consumer.shutdown() - if (theories_result.ok) session_result - else { - for { - (name, status) <- theories_result.nodes if !status.ok - (tree, _) <- theories_result.snapshot(name).messages if Protocol.is_error(tree) - } progress.echo_error_message(XML.content(Pretty.formatted(List(tree)))) - - session_result.copy(rc = session_result.rc max 1) - } + if (theories_result.ok && consumer_ok) session_result + else session_result.error_rc }