--- a/NEWS Thu Nov 26 15:51:20 2020 +0000
+++ b/NEWS Thu Nov 26 18:32:06 2020 +0100
@@ -242,6 +242,9 @@
ISABELLE_TOOL_JAVA_OPTIONS="$ISABELLE_TOOL_JAVA_OPTIONS -Xmx8g"
+This includes full PIDE markup, if option "build_pide_reports" is
+enabled.
+
* The command-line tool "isabelle build" provides option -P DIR to
produce PDF/HTML presentation in the specified directory; -P: refers to
the standard directory according to ISABELLE_BROWSER_INFO /
--- a/etc/options Thu Nov 26 15:51:20 2020 +0000
+++ b/etc/options Thu Nov 26 18:32:06 2020 +0100
@@ -150,6 +150,9 @@
option pide_reports : bool = true
-- "report PIDE markup"
+option build_pide_reports : bool = false
+ -- "report PIDE markup in batch build"
+
section "Editor Session"
--- a/src/Pure/PIDE/command.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/PIDE/command.scala Thu Nov 26 18:32:06 2020 +0100
@@ -418,7 +418,7 @@
span: Command_Span.Span): Command =
{
val (source, span1) = span.compact_source
- new Command(id, node_name, blobs_info, span1, source, Results.empty, Markup_Tree.empty)
+ new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty)
}
val empty: Command =
@@ -430,16 +430,17 @@
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 =
+ markups: Markups = Markups.empty): Command =
{
val (source1, span1) = Command_Span.unparsed(source, theory).compact_source
- new Command(id, node_name, no_blobs, span1, source1, results, markup)
+ new Command(id, node_name, no_blobs, span1, source1, results, markups)
}
def text(source: String): Command = unparsed(source)
def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
- unparsed(XML.content(body), id = id, results = results, markup = Markup_Tree.from_XML(body))
+ unparsed(XML.content(body), id = id, results = results,
+ markups = Markups.init(Markup_Tree.from_XML(body)))
/* perspective */
@@ -554,7 +555,7 @@
val span: Command_Span.Span,
val source: String,
val init_results: Command.Results,
- val init_markup: Markup_Tree)
+ val init_markups: Command.Markups)
{
override def toString: String = id + "/" + span.kind.toString
@@ -669,7 +670,7 @@
/* accumulated results */
val init_state: Command.State =
- Command.State(this, results = init_results, markups = Command.Markups.init(init_markup))
+ Command.State(this, results = init_results, markups = init_markups)
val empty_state: Command.State = Command.State(this)
}
--- a/src/Pure/PIDE/document.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/PIDE/document.scala Thu Nov 26 18:32:06 2020 +0100
@@ -552,7 +552,29 @@
def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
- def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
+ def command_snippet(command: Command): Snapshot =
+ {
+ val node_name = command.node_name
+
+ val nodes0 = version.nodes
+ val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
+ val version1 = Document.Version.make(nodes1)
+
+ val edits: List[Edit_Text] =
+ List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source))))
+
+ val state0 = state.define_command(command)
+ val state1 =
+ state0.continue_history(Future.value(version), edits, Future.value(version1))
+ .define_version(version1, state0.the_assignment(version))
+ .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
+
+ state1.snapshot(name = node_name)
+ }
+
+ def xml_markup(
+ range: Text.Range = Text.Range.full,
+ elements: Markup.Elements = Markup.Elements.full): XML.Body
def messages: List[(XML.Tree, Position.T)]
def exports: List[Export.Entry]
def exports_map: Map[String, Export.Entry]
@@ -712,7 +734,8 @@
def define_command(command: Command): State =
{
val id = command.id
- copy(commands = commands + (id -> command.init_state))
+ if (commands.isDefinedAt(id)) fail
+ else copy(commands = commands + (id -> command.init_state))
}
def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
@@ -793,10 +816,18 @@
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 {
+ def end_theory(theory: String): (Snapshot, State) =
+ theories.collectFirst({ case (_, st) if st.command.node_name.theory == theory => st }) match {
case None => fail
- case Some((id, st)) => (st, copy(theories = theories - id))
+ case Some(st) =>
+ val command = st.command
+ val node_name = command.node_name
+ val command1 =
+ Command.unparsed(command.source, theory = true, id = command.id, node_name = node_name,
+ results = st.results, markups = st.markups)
+ val state1 = copy(theories = theories - command1.id)
+ val snapshot = state1.snapshot(name = node_name).command_snippet(command1)
+ (snapshot, state1)
}
def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update)
@@ -973,11 +1004,11 @@
range: Text.Range, elements: Markup.Elements): Markup_Tree =
Command.State.merge_markup(command_states(version, command), index, range, elements)
- def markup_to_XML(
+ def xml_markup(
version: Version,
node_name: Node.Name,
- range: Text.Range,
- elements: Markup.Elements): XML.Body =
+ range: Text.Range = Text.Range.full,
+ elements: Markup.Elements = Markup.Elements.full): XML.Body =
{
val node = version.nodes(node_name)
if (node_name.is_theory) {
@@ -1097,8 +1128,10 @@
}
else version.nodes.commands_loading(other_node_name).headOption
- def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
- state.markup_to_XML(version, node_name, range, elements)
+ def xml_markup(
+ range: Text.Range = Text.Range.full,
+ elements: Markup.Elements = Markup.Elements.full): XML.Body =
+ state.xml_markup(version, node_name, range = range, elements = elements)
lazy val messages: List[(XML.Tree, Position.T)] =
(for {
--- a/src/Pure/PIDE/rendering.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/PIDE/rendering.scala Thu Nov 26 18:32:06 2020 +0100
@@ -97,8 +97,8 @@
def output_messages(results: Command.Results): List[XML.Tree] =
{
val (states, other) =
- results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
- .partition(Protocol.is_state(_))
+ results.iterator.map(_._2).filterNot(Protocol.is_result).toList
+ .partition(Protocol.is_state)
states ::: other
}
@@ -296,13 +296,13 @@
Some(Completion.Language_Context.inner)
}).headOption.map(_.info)
- def citation(range: Text.Range): Option[Text.Info[String]] =
+ def citations(range: Text.Range): List[Text.Info[String]] =
snapshot.select(range, Rendering.citation_elements, _ =>
{
case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
Some(Text.Info(snapshot.convert(info_range), name))
case _ => None
- }).headOption.map(_.info)
+ }).map(_.info)
/* file-system path completion */
--- a/src/Pure/PIDE/session.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/PIDE/session.scala Thu Nov 26 18:32:06 2020 +0100
@@ -181,7 +181,7 @@
/* outlets */
- val finished_theories = new Session.Outlet[Command.State](dispatcher)
+ val finished_theories = new Session.Outlet[Document.Snapshot](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)
@@ -511,8 +511,8 @@
case Markup.Finished_Theory(theory) =>
try {
- val st = global_state.change_result(_.end_theory(theory))
- finished_theories.post(st)
+ val snapshot = global_state.change_result(_.end_theory(theory))
+ finished_theories.post(snapshot)
}
catch { case _: Document.State.Fail => bad_output() }
--- a/src/Pure/System/process_result.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/System/process_result.scala Thu Nov 26 18:32:06 2020 +0100
@@ -53,6 +53,9 @@
def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1)
+ def errors_rc(errs: List[String]): Process_Result =
+ if (errs.isEmpty) this else errors(errs).error_rc
+
def check_rc(pred: Int => Boolean): Process_Result =
if (pred(rc)) this
else if (interrupted) throw Exn.Interrupt()
--- a/src/Pure/Thy/bibtex.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/Thy/bibtex.scala Thu Nov 26 18:32:06 2020 +0100
@@ -191,7 +191,7 @@
models: Map[A, B]): Option[Completion.Result] =
{
for {
- Text.Info(r, name) <- rendering.citation(rendering.before_caret_range(caret))
+ Text.Info(r, name) <- rendering.citations(rendering.before_caret_range(caret)).headOption
name1 <- Completion.clean_name(name)
original <- rendering.model.get_text(r)
--- a/src/Pure/Thy/export.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/Thy/export.scala Thu Nov 26 18:32:06 2020 +0100
@@ -18,6 +18,7 @@
val MARKUP = "PIDE/markup"
val MESSAGES = "PIDE/messages"
val DOCUMENT_PREFIX = "document/"
+ val CITATIONS = DOCUMENT_PREFIX + "citations"
val THEORY_PREFIX: String = "theory/"
val PROOFS_PREFIX: String = "proofs/"
--- a/src/Pure/Thy/presentation.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/Thy/presentation.scala Thu Nov 26 18:32:06 2020 +0100
@@ -266,7 +266,7 @@
val documents =
for {
doc <- info.document_variants
- document <- db_context.read_document(session, doc.name)
+ document <- db_context.input_database(session)(read_document(_, _, doc.name))
} yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc }
val links =
@@ -437,7 +437,7 @@
}
def pide_document(snapshot: Document.Snapshot): XML.Body =
- make_html(snapshot.markup_to_XML(Text.Range.full, document_elements))
+ make_html(snapshot.xml_markup(elements = document_elements))
@@ -533,7 +533,7 @@
val old_document =
for {
- old_doc <- db_context.read_document(session, doc.name)
+ old_doc <- db_context.input_database(session)(read_document(_, _, doc.name))
if old_doc.sources == sources
}
yield {
--- a/src/Pure/Thy/sessions.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/Thy/sessions.scala Thu Nov 26 18:32:06 2020 +0100
@@ -1190,6 +1190,22 @@
def close { database_server.foreach(_.close) }
+ def output_database[A](session: String)(f: SQL.Database => A): A =
+ database_server match {
+ case Some(db) => f(db)
+ case None => using(store.open_database(session, output = true))(f)
+ }
+
+ def input_database[A](session: String)(f: (SQL.Database, String) => Option[A]): Option[A] =
+ database_server match {
+ case Some(db) => f(db, session)
+ case None =>
+ store.try_open_database(session) match {
+ case Some(db) => using(db)(f(_, session))
+ case None => None
+ }
+ }
+
def read_export(session: String, theory_name: String, name: String): Option[Export.Entry] =
{
val hierarchy = sessions_structure.build_graph.all_preds(List(session)).view
@@ -1211,16 +1227,6 @@
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_Output] =
- database_server match {
- case Some(db) => Presentation.read_document(db, session_name, name)
- case None =>
- store.try_open_database(session_name) match {
- case Some(db) => using(db)(Presentation.read_document(_, session_name, name))
- case None => None
- }
- }
-
override def toString: String =
{
val s =
--- a/src/Pure/Tools/build.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/Tools/build.scala Thu Nov 26 18:32:06 2020 +0100
@@ -202,7 +202,7 @@
options +
"completion_limit=0" +
"editor_tracing_messages=0" +
- "pide_reports=false" // FIXME
+ ("pide_reports=" + options.bool("build_pide_reports"))
val store = Sessions.store(build_options)
--- a/src/Pure/Tools/build_job.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/Tools/build_job.scala Thu Nov 26 18:32:06 2020 +0100
@@ -51,6 +51,10 @@
override val xml_cache: XML.Cache = store.xml_cache
override val xz_cache: XZ.Cache = store.xz_cache
}
+ def make_rendering(snapshot: Document.Snapshot): Rendering =
+ new Rendering(snapshot, options, session) {
+ override def model: Document.Model = ???
+ }
object Build_Session_Errors
{
@@ -157,16 +161,26 @@
case Session.Runtime_Statistics(props) => runtime_statistics += props
}
- session.finished_theories += Session.Consumer[Command.State]("finished_theories")
+ session.finished_theories += Session.Consumer[Document.Snapshot]("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)))
+ case snapshot =>
+ val rendering = make_rendering(snapshot)
+
+ def export(name: String, xml: XML.Body)
+ {
+ val theory_name = snapshot.node_name.theory
+ val args = Protocol.Export.Args(theory_name = theory_name, name = name)
+ val bytes = Bytes(YXML.string_of_body(xml))
+ if (!bytes.is_empty) export_consumer(session_name, args, bytes)
+ }
+ def export_text(name: String, text: String): Unit =
+ export(name, List(XML.Text(text)))
+
+ export(Export.MARKUP, snapshot.xml_markup())
+ export(Export.MESSAGES, snapshot.messages.map(_._1))
+
+ val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info))
+ export_text(Export.CITATIONS, cat_lines(citations))
}
session.all_messages += Session.Consumer[Any]("build_session_output")
@@ -232,16 +246,18 @@
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty)
{
- 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 = progress,
- verbose = verbose))
- using(store.open_database(session_name, output = true))(db =>
- documents.foreach(_.write(db, session_name)))
- (documents.flatMap(_.log_lines), Nil)
+ using(store.open_database_context(deps.sessions_structure))(db_context =>
+ {
+ val documents =
+ Presentation.build_documents(session_name, deps, db_context,
+ output_sources = info.document_output,
+ output_pdf = info.document_output,
+ progress = progress,
+ verbose = verbose)
+ db_context.output_database(session_name)(db =>
+ documents.foreach(_.write(db, session_name)))
+ (documents.flatMap(_.log_lines), Nil)
+ })
}
(Nil, Nil)
}
@@ -260,10 +276,9 @@
task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
document_output
- val more_errors =
- Library.trim_line(stderr.toString) :: export_errors ::: document_errors
-
- process_result.output(more_output).errors(more_errors)
+ process_result.output(more_output)
+ .error(Library.trim_line(stderr.toString))
+ .errors_rc(export_errors ::: document_errors)
}
build_errors match {
--- a/src/Pure/Tools/dump.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/Tools/dump.scala Thu Nov 26 18:32:06 2020 +0100
@@ -48,29 +48,22 @@
val known_aspects: List[Aspect] =
List(
Aspect("markup", "PIDE markup (YXML format)",
- { case args =>
- args.write(Path.explode(Export.MARKUP),
- args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full))
- }),
+ args => args.write(Path.explode(Export.MARKUP), args.snapshot.xml_markup())),
Aspect("messages", "output messages (YXML format)",
- { case args =>
- args.write(Path.explode(Export.MESSAGES),
- args.snapshot.messages.iterator.map(_._1).toList)
- }),
+ args => args.write(Path.explode(Export.MESSAGES), args.snapshot.messages.map(_._1))),
Aspect("latex", "generated LaTeX source",
- { case args =>
- for {
- entry <- args.snapshot.exports
- if entry.name_has_prefix(Export.DOCUMENT_PREFIX)
- } args.write(Path.explode(entry.name), entry.uncompressed())
- }),
+ args =>
+ 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_has_prefix(Export.THEORY_PREFIX)
- } args.write(Path.explode(entry.name), entry.uncompressed())
- }, options = List("export_theory"))
+ args =>
+ for {
+ entry <- args.snapshot.exports
+ if entry.name_has_prefix(Export.THEORY_PREFIX)
+ } args.write(Path.explode(entry.name), entry.uncompressed()),
+ options = List("export_theory"))
).sortBy(_.name)
def show_aspects: String =
--- a/src/Pure/Tools/update.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Pure/Tools/update.scala Thu Nov 26 18:32:06 2020 +0100
@@ -45,8 +45,8 @@
val snapshot = args.snapshot
for ((node_name, node) <- snapshot.nodes) {
val xml =
- snapshot.state.markup_to_XML(snapshot.version, node_name,
- Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
+ snapshot.state.xml_markup(snapshot.version, node_name,
+ elements = Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
val source1 = Symbol.encode(XML.content(update_xml(xml)))
if (source1 != Symbol.encode(node.source)) {
--- a/src/Tools/jEdit/src/jedit_rendering.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Thu Nov 26 18:32:06 2020 +0100
@@ -21,9 +21,21 @@
object JEdit_Rendering
{
+ /* make rendering */
+
def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
new JEdit_Rendering(snapshot, model, options)
+ def text(snapshot: Document.Snapshot, formatted_body: XML.Body,
+ results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) =
+ {
+ val command = Command.rich_text(Document_ID.make(), results, formatted_body)
+ val snippet = snapshot.command_snippet(command)
+ val model = File_Model.empty(PIDE.session)
+ val rendering = apply(snippet, model, PIDE.options.value)
+ (command.source, rendering)
+ }
+
/* popup window bounds */
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 26 15:51:20 2020 +0000
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 26 18:32:06 2020 +0100
@@ -27,42 +27,6 @@
import org.gjt.sp.util.{SyntaxUtilities, Log}
-object Pretty_Text_Area
-{
- /* auxiliary */
-
- private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
- formatted_body: XML.Body): (String, Document.State) =
- {
- val command = Command.rich_text(Document_ID.make(), base_results, formatted_body)
- val node_name = command.node_name
- val edits: List[Document.Edit_Text] =
- List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
-
- val state0 = base_snapshot.state.define_command(command)
- val version0 = base_snapshot.version
- val nodes0 = version0.nodes
-
- val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
- val version1 = Document.Version.make(nodes1)
- val state1 =
- state0.continue_history(Future.value(version0), edits, Future.value(version1))
- .define_version(version1, state0.the_assignment(version0))
- .assign(version1.id, Nil, List(command.id -> List(Document_ID.make())))._2
-
- (command.source, state1)
- }
-
- private def text_rendering(base_snapshot: Document.Snapshot, base_results: Command.Results,
- formatted_body: XML.Body): (String, JEdit_Rendering) =
- {
- val (text, state) = document_state(base_snapshot, base_results, formatted_body)
- val model = File_Model.empty(PIDE.session)
- val rendering = JEdit_Rendering(state.snapshot(), model, PIDE.options.value)
- (text, rendering)
- }
-}
-
class Pretty_Text_Area(
view: View,
close_action: () => Unit = () => (),
@@ -77,7 +41,7 @@
private var current_base_snapshot = Document.Snapshot.init
private var current_base_results = Command.Results.empty
private var current_rendering: JEdit_Rendering =
- Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
+ JEdit_Rendering.text(current_base_snapshot, Nil)._2
private var future_refresh: Option[Future[Unit]] = None
private val rich_text_area =
@@ -112,7 +76,7 @@
getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
- get_background().map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
+ get_background().foreach(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
@@ -127,15 +91,15 @@
val metric = JEdit_Lib.pretty_metric(getPainter)
val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0
- val base_snapshot = current_base_snapshot
- val base_results = current_base_results
+ val snapshot = current_base_snapshot
+ val results = current_base_results
val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
- future_refresh.map(_.cancel)
+ future_refresh.foreach(_.cancel)
future_refresh =
Some(Future.fork {
val (text, rendering) =
- try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
+ try { JEdit_Rendering.text(snapshot, formatted_body, results = results) }
catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
Exn.Interrupt.expose()