# HG changeset patch # User wenzelm # Date 1606403319 -3600 # Node ID 3b804e0ffae9b65eec8e2bd2901ccf4c8da3dae0 # Parent ade53fbc6f037e1cbe2a0a62e3fb904be3d843ca clarified signature; diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Nov 26 15:59:09 2020 +0100 +++ b/src/Pure/PIDE/document.scala Thu Nov 26 16:08:39 2020 +0100 @@ -572,7 +572,9 @@ state1.snapshot(name = node_name) } - def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body + 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] @@ -1002,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) { @@ -1126,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 { diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Thu Nov 26 15:59:09 2020 +0100 +++ b/src/Pure/Thy/presentation.scala Thu Nov 26 16:08:39 2020 +0100 @@ -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)) diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Nov 26 15:59:09 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Thu Nov 26 16:08:39 2020 +0100 @@ -166,7 +166,7 @@ val args = Protocol.Export.Args(theory_name = theory_name, name = name) export_consumer(session_name, args, Bytes(YXML.string_of_body(xml))) } - export(Export.MARKUP, snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full)) + export(Export.MARKUP, snapshot.xml_markup()) } session.all_messages += Session.Consumer[Any]("build_session_output") diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Thu Nov 26 15:59:09 2020 +0100 +++ b/src/Pure/Tools/dump.scala Thu Nov 26 16:08:39 2020 +0100 @@ -50,7 +50,7 @@ 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.snapshot.xml_markup()) }), Aspect("messages", "output messages (YXML format)", { case args => diff -r ade53fbc6f03 -r 3b804e0ffae9 src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Thu Nov 26 15:59:09 2020 +0100 +++ b/src/Pure/Tools/update.scala Thu Nov 26 16:08:39 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)) {