# HG changeset patch # User wenzelm # Date 1606140898 -3600 # Node ID 22aeec526ffda2e49137cd2ed6236d696c5f5b34 # Parent 2126cf9460866686d19f15dfb2224af5d755ad3d support for PIDE markup in batch build (inactive due to pide_reports=false); diff -r 2126cf946086 -r 22aeec526ffd src/Pure/General/position.scala --- 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)) diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/command.scala --- 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 = diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/command_span.scala --- 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 "" case Ignored_Span => "" case Malformed_Span => "" + case Theory_Span => "" } } 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 */ diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/document.scala --- 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) = { diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/markup.ML --- 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")]; diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/markup.scala --- 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") diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/protocol.scala --- 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) } diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/protocol_message.scala --- 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 - } } diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/rendering.scala --- 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) diff -r 2126cf946086 -r 22aeec526ffd src/Pure/PIDE/session.scala --- 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) => diff -r 2126cf946086 -r 22aeec526ffd src/Pure/Thy/thy_info.ML --- 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); diff -r 2126cf946086 -r 22aeec526ffd src/Pure/Tools/build.scala --- 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) diff -r 2126cf946086 -r 22aeec526ffd src/Pure/Tools/build_job.scala --- 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 =>