--- 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;
--- 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()
--- 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
}
}
--- 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)
--- 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)
--- 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
}