--- a/src/Pure/General/position.scala Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/General/position.scala Mon Nov 23 15:14:58 2020 +0100
@@ -112,21 +112,6 @@
}
}
- 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))
--- a/src/Pure/PIDE/command.scala Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/command.scala Mon Nov 23 15:14:58 2020 +0100
@@ -331,16 +331,19 @@
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) =>
(this /: msgs)((state, msg) =>
@@ -348,38 +351,42 @@
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, atts), args) =>
+ 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 = 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
+ }
+ case _ =>
+ // silently ignore excessive reports
+ state
}
- case _ =>
- // silently ignore excessive reports
- 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 None
+ 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 _ => bad(); state
}
})
+
case XML.Elem(Markup(name, props), body) =>
props match {
case Markup.Serial(i) =>
@@ -392,8 +399,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 +431,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 +617,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 Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/command_span.scala Mon Nov 23 15:14:58 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 Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/document.scala Mon Nov 23 15:14:58 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 Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Nov 23 15:14:58 2020 +0100
@@ -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
@@ -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 Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Nov 23 15:14:58 2020 +0100
@@ -596,7 +596,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 Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Nov 23 15:14:58 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 Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/protocol_message.scala Mon Nov 23 15:14:58 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 Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/rendering.scala Mon Nov 23 15:14:58 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 Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/PIDE/session.scala Mon Nov 23 15:14:58 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/Thy/thy_info.ML Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Nov 23 15:14:58 2020 +0100
@@ -62,6 +62,7 @@
val _ =
Theory.setup (add_presentation (fn {options, file_pos, segments, ...} => fn thy =>
+ (Output.try_protocol_message (Markup.finished_theory (Context.theory_long_name thy)) [];
if exists (Toplevel.is_skipped_proof o #state) segments then ()
else
let
@@ -76,7 +77,7 @@
val latex = Latex.isabelle_body thy_name body;
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
in Export.export thy document_tex_name (XML.blob output) end
- end));
+ end)));
@@ -326,26 +327,28 @@
fun load_thy options initiators update_time 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
(if name = Context.PureN then [Context.the_global_context ()] else parents);
--- a/src/Pure/Tools/build.scala Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/Tools/build.scala Mon Nov 23 15:14:58 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)
--- a/src/Pure/Tools/build_job.scala Mon Nov 23 13:52:14 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Nov 23 15:14:58 2020 +0100
@@ -120,9 +120,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
}
@@ -158,6 +158,18 @@
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 =>