--- a/src/Pure/Admin/build_log.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Admin/build_log.scala Wed Nov 25 21:13:45 2020 +0100
@@ -485,12 +485,10 @@
val Session_Finished1 =
new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
val Session_Finished2 =
- new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
+ new Regex("""^Finished ([^\s/]+) \((\d+):(\d+):(\d+) elapsed time.*$""")
val Session_Timing =
new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
- val Session_Failed = new Regex("""^(\S+) FAILED""")
- val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
@@ -514,8 +512,6 @@
var timing = Map.empty[String, Timing]
var ml_timing = Map.empty[String, Timing]
var started = Set.empty[String]
- var failed = Set.empty[String]
- var cancelled = Set.empty[String]
var sources = Map.empty[String, String]
var heap_sizes = Map.empty[String, Long]
var theory_timings = Map.empty[String, Map[String, Timing]]
@@ -524,7 +520,7 @@
def all_sessions: Set[String] =
chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
- failed ++ cancelled ++ started ++ sources.keySet ++ heap_sizes.keySet ++
+ started ++ sources.keySet ++ heap_sizes.keySet ++
theory_timings.keySet ++ ml_statistics.keySet
@@ -596,9 +592,7 @@
Map(
(for (name <- all_sessions.toList) yield {
val status =
- if (failed(name)) Session_Status.failed
- else if (cancelled(name)) Session_Status.cancelled
- else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
+ if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
Session_Status.finished
else if (started(name)) Session_Status.failed
else Session_Status.existing
--- a/src/Pure/General/file.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/General/file.scala Wed Nov 25 21:13:45 2020 +0100
@@ -222,7 +222,7 @@
val line =
try { reader.readLine}
catch { case _: IOException => null }
- Option(line)
+ Option(line).map(Library.trim_line)
}
def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
--- a/src/Pure/General/position.ML Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/General/position.ML Wed Nov 25 21:13:45 2020 +0100
@@ -40,7 +40,6 @@
val def_properties_of: T -> Properties.T
val entity_markup: string -> string * T -> Markup.T
val entity_properties_of: bool -> serial -> T -> Properties.T
- val default_properties: T -> Properties.T -> Properties.T
val markup: T -> Markup.T -> Markup.T
val is_reported: T -> bool
val is_reported_range: T -> bool
@@ -91,7 +90,7 @@
fun norm_props (props: Properties.T) =
maps (fn a => the_list (find_first (fn (b, _) => a = b) props))
- Markup.position_properties';
+ [Markup.fileN, Markup.idN];
fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
@@ -211,10 +210,6 @@
if def then (Markup.defN, Value.print_int serial) :: properties_of pos
else (Markup.refN, Value.print_int serial) :: def_properties_of pos;
-fun default_properties default props =
- if exists (member (op =) Markup.position_properties o #1) props then props
- else properties_of default @ props;
-
val markup = Markup.properties o properties_of;
--- a/src/Pure/General/position.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/General/position.scala Wed Nov 25 21:13:45 2020 +0100
@@ -112,29 +112,12 @@
}
}
- object Identified
- {
- def unapply(pos: T): Option[(Long, Symbol.Text_Chunk.Name)] =
- pos match {
- case Id(id) =>
- val chunk_name =
- pos match {
- case File(name) => Symbol.Text_Chunk.File(name)
- case _ => Symbol.Text_Chunk.Default
- }
- Some((id, chunk_name))
- case _ => None
- }
- }
-
- def purge(props: T): T = props.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
-
/* here: user output */
def here(props: T, delimited: Boolean = true): String =
{
- val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1))
+ val pos = props.filter(Markup.position_property)
if (pos.isEmpty) ""
else {
val s0 =
--- a/src/Pure/PIDE/command.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/command.scala Wed Nov 25 21:13:45 2020 +0100
@@ -142,7 +142,7 @@
Markup_Index(status, chunk_name)
}
- (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
+ (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML))(body))(_ + _)
}
}
@@ -331,55 +331,56 @@
xml_cache: XML.Cache): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
- (this /: msgs)((state, msg) =>
- msg match {
- case elem @ XML.Elem(markup, Nil) =>
- state.
- add_status(markup).
- add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
- case _ =>
- Output.warning("Ignored status message: " + msg)
- state
- })
+ if (command.span.is_theory) this
+ else {
+ (this /: msgs)((state, msg) =>
+ msg match {
+ case elem @ XML.Elem(markup, Nil) =>
+ state.
+ add_status(markup).
+ add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem))
+ case _ =>
+ Output.warning("Ignored status message: " + msg)
+ state
+ })
+ }
- case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
+ case XML.Elem(Markup(Markup.REPORT, atts0), msgs) =>
(this /: msgs)((state, msg) =>
{
def bad(): Unit = Output.warning("Ignored report message: " + msg)
msg match {
- case XML.Elem(Markup(name, atts @ Position.Identified(id, chunk_name)), args) =>
-
- val target =
- if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
- Some((chunk_name, command.chunks(chunk_name)))
- else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
- else None
+ case XML.Elem(Markup(name, atts1), args) =>
+ val atts = atts1 ::: atts0
+ command.reported_position(atts) match {
+ case Some((id, chunk_name)) =>
+ val target =
+ if (self_id(id) && command.chunks.isDefinedAt(chunk_name))
+ Some((chunk_name, command.chunks(chunk_name)))
+ else if (chunk_name == Symbol.Text_Chunk.Default) other_id(id)
+ else None
- (target, atts) match {
- case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
- target_chunk.incorporate(symbol_range) match {
- case Some(range) =>
- val props = Position.purge(atts)
- val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
- state.add_markup(false, target_name, Text.Info(range, elem))
- case None => bad(); state
+ (target, atts) match {
+ case (Some((target_name, target_chunk)), Position.Range(symbol_range)) =>
+ target_chunk.incorporate(symbol_range) match {
+ case Some(range) =>
+ val props = atts.filterNot(Markup.position_property)
+ val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
+ state.add_markup(false, target_name, Text.Info(range, elem))
+ case None => bad(); state
+ }
+ case _ =>
+ // silently ignore excessive reports
+ state
}
- case _ =>
- // silently ignore excessive reports
- state
+
+ case _ => bad(); state
}
-
- case XML.Elem(Markup(name, atts), args)
- if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
- val range = command.core_range
- val props = Position.purge(atts)
- val elem = xml_cache.elem(XML.Elem(Markup(name, props), args))
- state.add_markup(false, Symbol.Text_Chunk.Default, Text.Info(range, elem))
-
case _ => bad(); state
}
})
+
case XML.Elem(Markup(name, props), body) =>
props match {
case Markup.Serial(i) =>
@@ -392,8 +393,7 @@
if (Protocol.is_inlined(message)) {
for {
(chunk_name, chunk) <- command.chunks.iterator
- range <- Protocol_Message.positions(
- self_id, command.span.position, chunk_name, chunk, message)
+ range <- command.message_positions(self_id, chunk_name, chunk, message)
} st = st.add_markup(false, chunk_name, Text.Info(range, message_markup))
}
st
@@ -425,24 +425,21 @@
Command(Document_ID.none, Document.Node.Name.empty, no_blobs, Command_Span.empty)
def unparsed(
- id: Document_ID.Command,
source: String,
- results: Results,
- markup: Markup_Tree): Command =
+ theory: Boolean = false,
+ id: Document_ID.Command = Document_ID.none,
+ node_name: Document.Node.Name = Document.Node.Name.empty,
+ results: Results = Results.empty,
+ markup: Markup_Tree = Markup_Tree.empty): Command =
{
- val (source1, span1) = Command_Span.unparsed(source).compact_source
- new Command(id, Document.Node.Name.empty, no_blobs, span1, source1, results, markup)
+ val (source1, span1) = Command_Span.unparsed(source, theory).compact_source
+ new Command(id, node_name, no_blobs, span1, source1, results, markup)
}
- def text(source: String): Command =
- unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
+ def text(source: String): Command = unparsed(source)
def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
- {
- val text = XML.content(body)
- val markup = Markup_Tree.from_XML(body)
- unparsed(id, text, results, markup)
- }
+ unparsed(XML.content(body), id = id, results = results, markup = Markup_Tree.from_XML(body))
/* perspective */
@@ -614,6 +611,61 @@
def source(range: Text.Range): String = range.substring(source)
+ /* reported positions */
+
+ def reported_position(pos: Position.T): Option[(Document_ID.Generic, Symbol.Text_Chunk.Name)] =
+ pos match {
+ case Position.Id(id) =>
+ val chunk_name =
+ pos match {
+ case Position.File(name) if name != node_name.node =>
+ Symbol.Text_Chunk.File(name)
+ case _ => Symbol.Text_Chunk.Default
+ }
+ Some((id, chunk_name))
+ case _ => None
+ }
+
+ def message_positions(
+ self_id: Document_ID.Generic => Boolean,
+ chunk_name: Symbol.Text_Chunk.Name,
+ chunk: Symbol.Text_Chunk,
+ message: XML.Elem): Set[Text.Range] =
+ {
+ def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
+ reported_position(props) match {
+ case Some((id, name)) if self_id(id) && name == chunk_name =>
+ val opt_range =
+ Position.Range.unapply(props) orElse {
+ if (name == Symbol.Text_Chunk.Default)
+ Position.Range.unapply(span.position)
+ else None
+ }
+ opt_range match {
+ case Some(symbol_range) =>
+ chunk.incorporate(symbol_range) match {
+ case Some(range) => set + range
+ case _ => set
+ }
+ case None => set
+ }
+ case _ => set
+ }
+ def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
+ t match {
+ case XML.Wrapped_Elem(Markup(name, props), _, body) =>
+ body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree)
+ case XML.Elem(Markup(name, props), body) =>
+ body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree)
+ case XML.Text(_) => set
+ }
+
+ val set = tree(Set.empty, message)
+ if (set.isEmpty) elem(message.markup.properties, set)
+ else set
+ }
+
+
/* accumulated results */
val init_state: Command.State =
--- a/src/Pure/PIDE/command_span.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala Wed Nov 25 21:13:45 2020 +0100
@@ -18,14 +18,18 @@
case Command_Span(name, _) => proper_string(name) getOrElse "<command>"
case Ignored_Span => "<ignored>"
case Malformed_Span => "<malformed>"
+ case Theory_Span => "<theory>"
}
}
case class Command_Span(name: String, pos: Position.T) extends Kind
case object Ignored_Span extends Kind
case object Malformed_Span extends Kind
+ case object Theory_Span extends Kind
sealed case class Span(kind: Kind, content: List[Token])
{
+ def is_theory: Boolean = kind == Theory_Span
+
def name: String =
kind match { case Command_Span(name, _) => name case _ => "" }
@@ -67,8 +71,11 @@
val empty: Span = Span(Ignored_Span, Nil)
- def unparsed(source: String): Span =
- Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
+ def unparsed(source: String, theory: Boolean): Span =
+ {
+ val kind = if (theory) Theory_Span else Malformed_Span
+ Span(kind, List(Token(Token.Kind.UNPARSED, source)))
+ }
/* XML data representation */
--- a/src/Pure/PIDE/document.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/document.scala Wed Nov 25 21:13:45 2020 +0100
@@ -672,6 +672,8 @@
versions: Map[Document_ID.Version, Version] = Map.empty,
/*inlined auxiliary files*/
blobs: Set[SHA1.Digest] = Set.empty,
+ /*loaded theories in batch builds*/
+ theories: Map[Document_ID.Exec, Command.State] = Map.empty,
/*static markup from define_command*/
commands: Map[Document_ID.Command, Command.State] = Map.empty,
/*dynamic markup from execution*/
@@ -721,7 +723,7 @@
def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail)
def lookup_id(id: Document_ID.Generic): Option[Command.State] =
- commands.get(id) orElse execs.get(id)
+ theories.get(id) orElse commands.get(id) orElse execs.get(id)
private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean =
id == st.command.id ||
@@ -738,18 +740,21 @@
def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache)
: (Command.State, State) =
{
- execs.get(id) match {
- case Some(st) =>
- val new_st = st.accumulate(self_id(st), other_id, message, xml_cache)
- val execs1 = execs + (id -> new_st)
- (new_st, copy(execs = execs1, commands_redirection = redirection(new_st)))
+ def update(st: Command.State): (Command.State, State) =
+ {
+ val st1 = st.accumulate(self_id(st), other_id, message, xml_cache)
+ (st1, copy(commands_redirection = redirection(st1)))
+ }
+ execs.get(id).map(update) match {
+ case Some((st1, state1)) => (st1, state1.copy(execs = execs + (id -> st1)))
case None =>
- commands.get(id) match {
- case Some(st) =>
- val new_st = st.accumulate(self_id(st), other_id, message, xml_cache)
- val commands1 = commands + (id -> new_st)
- (new_st, copy(commands = commands1, commands_redirection = redirection(new_st)))
- case None => fail
+ commands.get(id).map(update) match {
+ case Some((st1, state1)) => (st1, state1.copy(commands = commands + (id -> st1)))
+ case None =>
+ theories.get(id).map(update) match {
+ case Some((st1, state1)) => (st1, state1.copy(theories = theories + (id -> st1)))
+ case None => fail
+ }
}
}
}
@@ -781,6 +786,19 @@
st <- command_states(version, command).iterator
} yield st.exports)
+ def begin_theory(node_name: Node.Name, id: Document_ID.Exec, source: String): State =
+ if (theories.isDefinedAt(id)) fail
+ else {
+ val command = Command.unparsed(source, theory = true, id = id, node_name = node_name)
+ copy(theories = theories + (id -> command.empty_state))
+ }
+
+ def end_theory(theory: String): (Command.State, State) =
+ theories.find({ case (_, st) => st.command.node_name.theory == theory }) match {
+ case None => fail
+ case Some((id, st)) => (st, copy(theories = theories - id))
+ }
+
def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
: ((List[Node.Name], List[Command]), State) =
{
--- a/src/Pure/PIDE/markup.ML Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Nov 25 21:13:45 2020 +0100
@@ -59,8 +59,8 @@
val end_offsetN: string
val fileN: string
val idN: string
- val position_properties': string list
val position_properties: string list
+ val position_property: Properties.entry -> bool
val positionN: string val position: T
val expressionN: string val expression: string -> T
val citationN: string val citation: string -> T
@@ -220,6 +220,7 @@
val theory_timing: Properties.entry
val session_timing: Properties.entry
val loading_theory: string -> Properties.T
+ val finished_theory: string -> Properties.T
val build_session_finished: Properties.T
val print_operationsN: string
val print_operations: Properties.T
@@ -379,8 +380,8 @@
val fileN = "file";
val idN = "id";
-val position_properties' = [fileN, idN];
-val position_properties = [lineN, offsetN, end_offsetN] @ position_properties';
+val position_properties = [lineN, offsetN, end_offsetN, fileN, idN];
+fun position_property (entry: Properties.entry) = member (op =) position_properties (#1 entry);
val (positionN, position) = markup_elem "position";
@@ -692,7 +693,8 @@
val session_timing = (functionN, "session_timing");
-fun loading_theory name = [("function", "loading_theory"), ("name", name)];
+fun loading_theory name = [("function", "loading_theory"), (nameN, name)];
+fun finished_theory name = [("function", "finished_theory"), (nameN, name)];
val build_session_finished = [("function", "build_session_finished")];
--- a/src/Pure/PIDE/markup.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/markup.scala Wed Nov 25 21:13:45 2020 +0100
@@ -144,6 +144,8 @@
val DEF_ID = "def_id"
val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
+ def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1)
+
val POSITION = "position"
@@ -587,6 +589,7 @@
}
val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
+ def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
object Command_Timing extends Properties_Function("command_timing")
object Theory_Timing extends Properties_Function("theory_timing")
@@ -596,7 +599,8 @@
}
object Task_Statistics extends Properties_Function("task_statistics")
- object Loading_Theory extends Name_Function("loading_theory")
+ object Loading_Theory extends Properties_Function("loading_theory")
+ object Finished_Theory extends Name_Function("finished_theory")
object Build_Session_Finished extends Function("build_session_finished")
object Commands_Accepted extends Function("commands_accepted")
--- a/src/Pure/PIDE/protocol.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Nov 25 21:13:45 2020 +0100
@@ -21,6 +21,21 @@
val Error_Message_Marker = Protocol_Message.Marker("error_message")
+ /* batch build */
+
+ object Loading_Theory
+ {
+ def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] =
+ (props, props, props) match {
+ case (Markup.Name(name), Position.File(file), Position.Id(id))
+ if Path.is_wellformed(file) =>
+ val master_dir = Path.explode(file).dir.implode
+ Some((Document.Node.Name(file, master_dir, name), id))
+ case _ => None
+ }
+ }
+
+
/* document editing */
object Commands_Accepted
@@ -188,13 +203,13 @@
object Export
{
sealed case class Args(
- id: Option[String],
- serial: Long,
+ id: Option[String] = None,
+ serial: Long = 0L,
theory_name: String,
name: String,
- executable: Boolean,
- compress: Boolean,
- strict: Boolean)
+ executable: Boolean = false,
+ compress: Boolean = true,
+ strict: Boolean = true)
{
def compound_name: String = isabelle.Export.compound_name(theory_name, name)
}
--- a/src/Pure/PIDE/protocol_message.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/protocol_message.scala Wed Nov 25 21:13:45 2020 +0100
@@ -71,50 +71,4 @@
case XML.Elem(_, ts) => reports(props, ts)
case XML.Text(_) => Nil
}
-
-
- /* reported positions */
-
- private val position_elements =
- Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
-
- def positions(
- self_id: Document_ID.Generic => Boolean,
- command_position: Position.T,
- chunk_name: Symbol.Text_Chunk.Name,
- chunk: Symbol.Text_Chunk,
- message: XML.Elem): Set[Text.Range] =
- {
- def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] =
- props match {
- case Position.Identified(id, name) if self_id(id) && name == chunk_name =>
- val opt_range =
- Position.Range.unapply(props) orElse {
- if (name == Symbol.Text_Chunk.Default)
- Position.Range.unapply(command_position)
- else None
- }
- opt_range match {
- case Some(symbol_range) =>
- chunk.incorporate(symbol_range) match {
- case Some(range) => set + range
- case _ => set
- }
- case None => set
- }
- case _ => set
- }
- def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] =
- t match {
- case XML.Wrapped_Elem(Markup(name, props), _, body) =>
- body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
- case XML.Elem(Markup(name, props), body) =>
- body.foldLeft(if (position_elements(name)) elem(props, set) else set)(tree)
- case XML.Text(_) => set
- }
-
- val set = tree(Set.empty, message)
- if (set.isEmpty) elem(message.markup.properties, set)
- else set
- }
}
--- a/src/Pure/PIDE/rendering.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala Wed Nov 25 21:13:45 2020 +0100
@@ -169,6 +169,9 @@
/* markup elements */
+ val position_elements =
+ Markup.Elements(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
+
val semantic_completion_elements =
Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
--- a/src/Pure/PIDE/session.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/PIDE/session.scala Wed Nov 25 21:13:45 2020 +0100
@@ -181,6 +181,7 @@
/* outlets */
+ val finished_theories = new Session.Outlet[Command.State](dispatcher)
val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher)
val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher)
val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher)
@@ -475,7 +476,9 @@
{
try {
val st = global_state.change_result(f)
- change_buffer.invoke(false, Nil, List(st.command))
+ if (!st.command.span.is_theory) {
+ change_buffer.invoke(false, Nil, List(st.command))
+ }
}
catch { case _: Document.State.Fail => bad_output() }
}
@@ -502,6 +505,17 @@
val export = Export.make_entry("", args, msg.bytes, cache = xz_cache)
change_command(_.add_export(id, (args.serial, export)))
+ case Protocol.Loading_Theory(node_name, id) =>
+ try { global_state.change(_.begin_theory(node_name, id, msg.text)) }
+ catch { case _: Document.State.Fail => bad_output() }
+
+ case Markup.Finished_Theory(theory) =>
+ try {
+ val st = global_state.change_result(_.end_theory(theory))
+ finished_theories.post(st)
+ }
+ catch { case _: Document.State.Fail => bad_output() }
+
case List(Markup.Commands_Accepted.PROPERTY) =>
msg.text match {
case Protocol.Commands_Accepted(ids) =>
--- a/src/Pure/ROOT.ML Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/ROOT.ML Wed Nov 25 21:13:45 2020 +0100
@@ -352,3 +352,4 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML"
+
--- a/src/Pure/System/isabelle_process.ML Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/System/isabelle_process.ML Wed Nov 25 21:13:45 2020 +0100
@@ -148,11 +148,10 @@
if forall (fn s => s = "") ss then ()
else
let
- val props' =
- (case (Properties.defined props Markup.idN, Position.get_id (Position.thread_data ())) of
- (false, SOME id') => props @ [(Markup.idN, id')]
- | _ => props);
- in message name props' (XML.blob ss) end;
+ val pos_props =
+ if exists Markup.position_property props then props
+ else props @ Position.properties_of (Position.thread_data ());
+ in message name pos_props (XML.blob ss) end;
fun report_message ss =
if Context_Position.pide_reports ()
--- a/src/Pure/System/progress.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/System/progress.scala Wed Nov 25 21:13:45 2020 +0100
@@ -32,7 +32,6 @@
def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
- def echo_document(msg: String) { echo(msg) }
def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
Timing.timeit(message, enabled, echo)(e)
--- a/src/Pure/Thy/export.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/export.scala Wed Nov 25 21:13:45 2020 +0100
@@ -13,7 +13,13 @@
object Export
{
- /* name structure */
+ /* artefact names */
+
+ val MARKUP = "PIDE/markup"
+ val MESSAGES = "PIDE/messages"
+ val DOCUMENT_PREFIX = "document/"
+ val THEORY_PREFIX: String = "theory/"
+ val PROOFS_PREFIX: String = "proofs/"
def explode_name(s: String): List[String] = space_explode('/', s)
def implode_name(elems: Iterable[String]): String = elems.mkString("/")
@@ -89,6 +95,7 @@
def compound_name: String = Export.compound_name(theory_name, name)
+ def name_has_prefix(s: String): Boolean = name.startsWith(s)
val name_elems: List[String] = explode_name(name)
def name_extends(elems: List[String]): Boolean =
--- a/src/Pure/Thy/export_theory.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala Wed Nov 25 21:13:45 2020 +0100
@@ -62,9 +62,6 @@
/** theory content **/
- val export_prefix: String = "theory/"
- val export_prefix_proofs: String = "proofs/"
-
sealed case class Theory(name: String, parents: List[String],
types: List[Type],
consts: List[Const],
@@ -115,7 +112,7 @@
val parents =
if (theory_name == Thy_Header.PURE) Nil
else {
- provider(export_prefix + "parents") match {
+ provider(Export.THEORY_PREFIX + "parents") match {
case Some(entry) => split_lines(entry.uncompressed().text)
case None =>
error("Missing theory export in session " + quote(session_name) + ": " +
@@ -195,7 +192,7 @@
case XML.Elem(Markup(Markup.ENTITY, props), body) =>
val name = Markup.Name.unapply(props) getOrElse err()
val xname = Markup.XName.unapply(props) getOrElse err()
- val pos = props.filter({ case (a, _) => Markup.POSITION_PROPERTIES(a) && a != Markup.ID })
+ val pos = props.filter(p => Markup.position_property(p) && p._1 != Markup.ID)
val id = Position.Id.unapply(props)
val serial = Markup.Serial.unapply(props) getOrElse err()
(Entity(kind, name, xname, pos, id, serial), body)
@@ -239,7 +236,7 @@
}
def read_types(provider: Export.Provider): List[Type] =
- provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
+ provider.uncompressed_yxml(Export.THEORY_PREFIX + "types").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.TYPE, tree)
val (syntax, args, abbrev) =
@@ -271,7 +268,7 @@
}
def read_consts(provider: Export.Provider): List[Const] =
- provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
+ provider.uncompressed_yxml(Export.THEORY_PREFIX + "consts").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.CONST, tree)
val (syntax, (typargs, (typ, (abbrev, propositional)))) =
@@ -318,7 +315,7 @@
}
def read_axioms(provider: Export.Provider): List[Axiom] =
- provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
+ provider.uncompressed_yxml(Export.THEORY_PREFIX + "axioms").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.AXIOM, tree)
val prop = decode_prop(body)
@@ -348,7 +345,7 @@
}
def read_thms(provider: Export.Provider): List[Thm] =
- provider.uncompressed_yxml(export_prefix + "thms").map((tree: XML.Tree) =>
+ provider.uncompressed_yxml(Export.THEORY_PREFIX + "thms").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.THM, tree)
val (prop, deps, prf) =
@@ -379,7 +376,7 @@
def read_proof(
provider: Export.Provider, id: Thm_Id, cache: Option[Term.Cache] = None): Option[Proof] =
{
- for { entry <- provider.focus(id.theory_name)(export_prefix_proofs + id.serial) }
+ for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) }
yield {
val body = entry.uncompressed_yxml()
val (typargs, (args, (prop_body, proof_body))) =
@@ -454,7 +451,7 @@
}
def read_classes(provider: Export.Provider): List[Class] =
- provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
+ provider.uncompressed_yxml(Export.THEORY_PREFIX + "classes").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.CLASS, tree)
val (params, axioms) =
@@ -483,7 +480,7 @@
}
def read_locales(provider: Export.Provider): List[Locale] =
- provider.uncompressed_yxml(export_prefix + "locales").map((tree: XML.Tree) =>
+ provider.uncompressed_yxml(Export.THEORY_PREFIX + "locales").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.LOCALE, tree)
val (typargs, args, axioms) =
@@ -520,7 +517,7 @@
}
def read_locale_dependencies(provider: Export.Provider): List[Locale_Dependency] =
- provider.uncompressed_yxml(export_prefix + "locale_dependencies").map((tree: XML.Tree) =>
+ provider.uncompressed_yxml(Export.THEORY_PREFIX + "locale_dependencies").map((tree: XML.Tree) =>
{
val (entity, body) = decode_entity(Kind.LOCALE_DEPENDENCY, tree)
val (source, (target, (prefix, (subst_types, subst_terms)))) =
@@ -544,7 +541,7 @@
def read_classrel(provider: Export.Provider): List[Classrel] =
{
- val body = provider.uncompressed_yxml(export_prefix + "classrel")
+ val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "classrel")
val classrel =
{
import XML.Decode._
@@ -562,7 +559,7 @@
def read_arities(provider: Export.Provider): List[Arity] =
{
- val body = provider.uncompressed_yxml(export_prefix + "arities")
+ val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "arities")
val arities =
{
import XML.Decode._
@@ -583,7 +580,7 @@
def read_constdefs(provider: Export.Provider): List[Constdef] =
{
- val body = provider.uncompressed_yxml(export_prefix + "constdefs")
+ val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "constdefs")
val constdefs =
{
import XML.Decode._
@@ -609,7 +606,7 @@
def read_typedefs(provider: Export.Provider): List[Typedef] =
{
- val body = provider.uncompressed_yxml(export_prefix + "typedefs")
+ val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "typedefs")
val typedefs =
{
import XML.Decode._
@@ -645,7 +642,7 @@
def read_datatypes(provider: Export.Provider): List[Datatype] =
{
- val body = provider.uncompressed_yxml(export_prefix + "datatypes")
+ val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "datatypes")
val datatypes =
{
import XML.Decode._
@@ -741,7 +738,7 @@
def read_spec_rules(provider: Export.Provider): List[Spec_Rule] =
{
- val body = provider.uncompressed_yxml(export_prefix + "spec_rules")
+ val body = provider.uncompressed_yxml(Export.THEORY_PREFIX + "spec_rules")
val spec_rules =
{
import XML.Decode._
--- a/src/Pure/Thy/presentation.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Wed Nov 25 21:13:45 2020 +0100
@@ -12,9 +12,15 @@
object Presentation
{
- /* document variants */
+ /* document info */
- type Document_PDF = (Document_Variant, Bytes)
+ abstract class Document_Name
+ {
+ def name: String
+ def path: Path = Path.basic(name)
+
+ override def toString: String = name
+ }
object Document_Variant
{
@@ -29,13 +35,11 @@
}
}
- sealed case class Document_Variant(name: String, tags: List[String], sources: String = "")
+ sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name
{
def print_tags: String = tags.mkString(",")
def print: String = if (tags.isEmpty) name else name + "=" + print_tags
- def path: Path = Path.basic(name)
-
def latex_sty: String =
Library.terminate_lines(
tags.map(tag =>
@@ -45,8 +49,19 @@
case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
case cs => "\\isakeeptag{" + cs.mkString + "}"
}))
+ }
- def set_sources(s: String): Document_Variant = copy(sources = s)
+ sealed case class Document_Input(name: String, sources: SHA1.Digest)
+ extends Document_Name
+
+ sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
+ extends Document_Name
+ {
+ def log: String = log_xz.uncompress().text
+ def log_lines: List[String] = split_lines(log)
+
+ def write(db: SQL.Database, session_name: String) =
+ write_document(db, session_name, this)
}
@@ -56,32 +71,30 @@
{
val session_name = SQL.Column.string("session_name").make_primary_key
val name = SQL.Column.string("name").make_primary_key
- val tags = SQL.Column.string("tags")
val sources = SQL.Column.string("sources")
+ val log_xz = SQL.Column.bytes("log_xz")
val pdf = SQL.Column.bytes("pdf")
- val table = SQL.Table("isabelle_documents", List(session_name, name, tags, sources, pdf))
+ val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf))
def where_equal(session_name: String, name: String = ""): SQL.Source =
"WHERE " + Data.session_name.equal(session_name) +
(if (name == "") "" else " AND " + Data.name.equal(name))
}
- def read_document_variants(db: SQL.Database, session_name: String): List[Document_Variant] =
+ def read_documents(db: SQL.Database, session_name: String): List[Document_Input] =
{
- val select =
- Data.table.select(List(Data.name, Data.tags, Data.sources), Data.where_equal(session_name))
+ val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name))
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(res =>
{
val name = res.string(Data.name)
- val tags = res.string(Data.tags)
val sources = res.string(Data.sources)
- Document_Variant.parse(name, tags).set_sources(sources)
+ Document_Input(name, SHA1.fake(sources))
}).toList)
}
- def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_PDF] =
+ def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] =
{
val select = Data.table.select(sql = Data.where_equal(session_name, name))
db.using_statement(select)(stmt =>
@@ -89,24 +102,24 @@
val res = stmt.execute_query()
if (res.next()) {
val name = res.string(Data.name)
- val tags = res.string(Data.tags)
val sources = res.string(Data.sources)
+ val log_xz = res.bytes(Data.log_xz)
val pdf = res.bytes(Data.pdf)
- Some(Document_Variant.parse(name, tags).set_sources(sources) -> pdf)
+ Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf))
}
else None
})
}
- def write_document(db: SQL.Database, session_name: String, doc: Document_Variant, pdf: Bytes)
+ def write_document(db: SQL.Database, session_name: String, doc: Document_Output)
{
db.using_statement(Data.table.insert())(stmt =>
{
stmt.string(1) = session_name
stmt.string(2) = doc.name
- stmt.string(3) = doc.print_tags
- stmt.string(4) = doc.sources
- stmt.bytes(5) = pdf
+ stmt.string(3) = doc.sources.toString
+ stmt.bytes(4) = doc.log_xz
+ stmt.bytes(5) = doc.pdf
stmt.execute()
})
}
@@ -253,8 +266,8 @@
val documents =
for {
doc <- info.document_variants
- (_, pdf) <- db_context.read_document(session, doc.name)
- } yield { Bytes.write(session_dir + doc.path.pdf, pdf); doc }
+ document <- db_context.read_document(session, doc.name)
+ } yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc }
val links =
{
@@ -443,7 +456,7 @@
output_sources: Option[Path] = None,
output_pdf: Option[Path] = None,
verbose: Boolean = false,
- verbose_latex: Boolean = false): List[Document_PDF] =
+ verbose_latex: Boolean = false): List[Document_Output] =
{
/* session info */
@@ -499,7 +512,7 @@
yield {
Isabelle_System.with_tmp_dir("document")(tmp_dir =>
{
- progress.echo_document("Building document " + session + "/" + doc.name + " ...")
+ progress.echo("Preparing " + session + "/" + doc.name + " ...")
val start = Time.now()
@@ -507,7 +520,7 @@
val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
- val sources = SHA1.digest_set(digests).toString
+ val sources = SHA1.digest_set(digests)
prepare_dir2(tmp_dir, doc)
for (dir <- output_sources) {
@@ -520,12 +533,12 @@
val old_document =
for {
- document@(doc, pdf) <- db_context.read_document(session, doc.name)
- if doc.sources == sources
+ old_doc <- db_context.read_document(session, doc.name)
+ if old_doc.sources == sources
}
yield {
- Bytes.write(doc_dir + doc.path.pdf, pdf)
- document
+ Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf)
+ old_doc
}
old_document getOrElse {
@@ -574,20 +587,22 @@
else {
val stop = Time.now()
val timing = stop - start
- progress.echo_document("Finished document " + session + "/" + doc.name +
+ progress.echo("Finished " + session + "/" + doc.name +
" (" + timing.message_hms + " elapsed time)")
- doc.set_sources(sources) -> Bytes.read(result_path)
+ val log_xz = Bytes(cat_lines(result.out_lines ::: result.err_lines)).compress()
+ val pdf = Bytes.read(result_path)
+ Document_Output(doc.name, sources, log_xz, pdf)
}
}
})
}
- for (dir <- output_pdf; (doc, pdf) <- documents) {
+ for (dir <- output_pdf; doc <- documents) {
Isabelle_System.make_directory(dir)
val path = dir + doc.path.pdf
- Bytes.write(path, pdf)
- progress.echo_document("Document at " + path.absolute)
+ Bytes.write(path, doc.pdf)
+ progress.echo("Document at " + path.absolute)
}
documents
--- a/src/Pure/Thy/sessions.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Nov 25 21:13:45 2020 +0100
@@ -1211,7 +1211,7 @@
read_export(session, theory_name, name) getOrElse
Export.empty_entry(session, theory_name, name)
- def read_document(session_name: String, name: String): Option[Presentation.Document_PDF] =
+ def read_document(session_name: String, name: String): Option[Presentation.Document_Output] =
database_server match {
case Some(db) => Presentation.read_document(db, session_name, name)
case None =>
--- a/src/Pure/Thy/thy_info.ML Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML Wed Nov 25 21:13:45 2020 +0100
@@ -56,7 +56,8 @@
);
fun apply_presentation (context: presentation_context) thy =
- ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
+ (ignore (Presentation.get thy |> Par_List.map (fn (f, _) => f context thy));
+ Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) []);
fun add_presentation f = Presentation.map (cons (f, stamp ()));
@@ -292,7 +293,7 @@
val thy = Toplevel.end_theory end_pos end_state;
in (results, thy) end;
-fun eval_thy options update_time master_dir header text_pos text parents =
+fun eval_thy options master_dir header text_pos text parents =
let
val (name, _) = #name header;
val keywords =
@@ -324,30 +325,32 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy options initiators update_time deps text (name, pos) keywords parents =
+fun load_thy options initiators deps text (name, pos) keywords parents =
let
- val _ = remove_thy name;
- val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
- val _ = Output.try_protocol_message (Markup.loading_theory name) [];
+ val exec_id = Document_ID.make ();
+ val id = Document_ID.print exec_id;
+ val _ =
+ Execution.running Document_ID.none exec_id [] orelse
+ raise Fail ("Failed to register execution: " ^ id);
val {master = (thy_path, _), imports} = deps;
val dir = Path.dir thy_path;
val header = Thy_Header.make (name, pos) imports keywords;
-
val _ =
(imports ~~ parents) |> List.app (fn ((_, pos), thy) =>
Context_Position.reports_global thy [(pos, Theory.get_markup thy)]);
- val exec_id = Document_ID.make ();
- val _ =
- Execution.running Document_ID.none exec_id [] orelse
- raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
+ val text_pos = Position.put_id id (Path.position thy_path);
+ val text_props = Position.properties_of text_pos;
+
+ val _ = remove_thy name;
+ val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
+ val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) (XML.blob [text]);
val timing_start = Timing.start ();
- val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
val (theory, present, weight) =
- eval_thy options update_time dir header text_pos text
+ eval_thy options dir header text_pos text
(if name = Context.PureN then [Context.the_global_context ()] else parents);
val timing_result = Timing.result timing_start;
@@ -411,12 +414,8 @@
(case deps of
NONE => raise Fail "Malformed deps"
| SOME (dep, text) =>
- let
- val update_time = serial ();
- val load =
- load_thy options initiators update_time
- dep text (theory_name, theory_pos) keywords;
- in Task (parents, load) end);
+ Task (parents,
+ load_thy options initiators dep text (theory_name, theory_pos) keywords));
val tasks'' = new_entry theory_name parents task tasks';
in (all_current, tasks'') end)
--- a/src/Pure/Tools/build.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Tools/build.scala Wed Nov 25 21:13:45 2020 +0100
@@ -202,7 +202,7 @@
options +
"completion_limit=0" +
"editor_tracing_messages=0" +
- "pide_reports=false"
+ "pide_reports=false" // FIXME
val store = Sessions.store(build_options)
@@ -429,7 +429,7 @@
val numa_node = numa_nodes.next(used_node)
val job =
- new Build_Job(progress, session_name, info, deps, store, do_store, presentation,
+ new Build_Job(progress, session_name, info, deps, store, do_store,
verbose, numa_node, queue.command_timings(session_name))
loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
}
--- a/src/Pure/Tools/build_job.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Wed Nov 25 21:13:45 2020 +0100
@@ -16,7 +16,6 @@
deps: Sessions.Deps,
store: Sessions.Store,
do_store: Boolean,
- presentation: Presentation.Context,
verbose: Boolean,
val numa_node: Option[Int],
command_timings0: List[Properties.T])
@@ -77,7 +76,6 @@
val session_timings = new mutable.ListBuffer[Properties.T]
val runtime_statistics = new mutable.ListBuffer[Properties.T]
val task_statistics = new mutable.ListBuffer[Properties.T]
- val document_output = new mutable.ListBuffer[String]
def fun(
name: String,
@@ -120,9 +118,9 @@
private def loading_theory(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
- case Markup.Loading_Theory(name) =>
+ case Markup.Loading_Theory(Markup.Name(name)) =>
progress.theory(Progress.Theory(name, session = session_name))
- true
+ false
case _ => false
}
@@ -134,30 +132,43 @@
case _ => false
}
- private def command_timing(props: Properties.T): Option[Properties.T] =
- for {
- props1 <- Markup.Command_Timing.unapply(props)
- elapsed <- Markup.Elapsed.unapply(props1)
- elapsed_time = Time.seconds(elapsed)
- if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
- } yield props1.filter(p => Markup.command_timing_properties(p._1))
-
override val functions =
List(
Markup.Build_Session_Finished.name -> build_session_finished,
Markup.Loading_Theory.name -> loading_theory,
Markup.EXPORT -> export,
- fun(Markup.Command_Timing.name, command_timings, command_timing),
fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
})
+ session.command_timings += Session.Consumer("command_timings")
+ {
+ case Session.Command_Timing(props) =>
+ for {
+ elapsed <- Markup.Elapsed.unapply(props)
+ elapsed_time = Time.seconds(elapsed)
+ if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold")
+ } command_timings += props.filter(Markup.command_timing_property)
+ }
+
session.runtime_statistics += Session.Consumer("ML_statistics")
{
case Session.Runtime_Statistics(props) => runtime_statistics += props
}
+ session.finished_theories += Session.Consumer[Command.State]("finished_theories")
+ {
+ case st =>
+ val command = st.command
+ val theory_name = command.node_name.theory
+ val args = Protocol.Export.Args(theory_name = theory_name, name = Export.MARKUP)
+ val xml =
+ st.markups(Command.Markup_Index.markup)
+ .to_XML(command.range, command.source, Markup.Elements.full)
+ export_consumer(session_name, args, Bytes(YXML.string_of_body(xml)))
+ }
+
session.all_messages += Session.Consumer[Any]("build_session_output")
{
case msg: Prover.Output =>
@@ -212,38 +223,29 @@
val process_result =
Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown }
+ session.stop()
+
val export_errors =
export_consumer.shutdown(close = true).map(Output.error_message_text)
- val document_errors =
+ val (document_output, document_errors) =
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
{
- val document_progress =
- new Progress {
- override def echo(msg: String): Unit =
- document_output.synchronized { document_output += msg }
- override def echo_document(msg: String): Unit =
- progress.echo_document(msg)
- }
val documents =
using(store.open_database_context(deps.sessions_structure))(db_context =>
Presentation.build_documents(session_name, deps, db_context,
output_sources = info.document_output,
output_pdf = info.document_output,
- progress = document_progress,
- verbose = verbose,
- verbose_latex = true))
+ progress = progress,
+ verbose = verbose))
using(store.open_database(session_name, output = true))(db =>
- for ((doc, pdf) <- documents) {
- db.transaction {
- Presentation.write_document(db, session_name, doc, pdf)
- }
- })
+ documents.foreach(_.write(db, session_name)))
+ (documents.flatMap(_.log_lines), Nil)
}
- Nil
+ (Nil, Nil)
}
- catch { case Exn.Interrupt.ERROR(msg) => List(msg) }
+ catch { case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) }
val result =
{
@@ -256,7 +258,7 @@
session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
- document_output.toList
+ document_output
val more_errors =
Library.trim_line(stderr.toString) :: export_errors ::: document_errors
--- a/src/Pure/Tools/dump.scala Tue Nov 24 19:49:59 2020 +0100
+++ b/src/Pure/Tools/dump.scala Wed Nov 25 21:13:45 2020 +0100
@@ -49,24 +49,26 @@
List(
Aspect("markup", "PIDE markup (YXML format)",
{ case args =>
- args.write(Path.explode("markup.yxml"),
+ args.write(Path.explode(Export.MARKUP),
args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
}),
Aspect("messages", "output messages (YXML format)",
{ case args =>
- args.write(Path.explode("messages.yxml"),
+ args.write(Path.explode(Export.MESSAGES),
args.snapshot.messages.iterator.map(_._1).toList)
}),
Aspect("latex", "generated LaTeX source",
{ case args =>
- for (entry <- args.snapshot.exports if entry.name == "document.tex")
- args.write(Path.explode(entry.name), entry.uncompressed())
+ for {
+ entry <- args.snapshot.exports
+ if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
+ } args.write(Path.explode(entry.name), entry.uncompressed())
}),
Aspect("theory", "foundational theory content",
{ case args =>
for {
entry <- args.snapshot.exports
- if entry.name.startsWith(Export_Theory.export_prefix)
+ if entry.name_has_prefix(Export.THEORY_PREFIX)
} args.write(Path.explode(entry.name), entry.uncompressed())
}, options = List("export_theory"))
).sortBy(_.name)