# HG changeset patch # User wenzelm # Date 1528051036 -7200 # Node ID f9379279f98c0753822d9e85c43a237853aeb759 # Parent 5c579bb9adb11cf7ad098f09bf26cfa71aacbead clarified signature: prefer Document.Snapshot; diff -r 5c579bb9adb1 -r f9379279f98c src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sun Jun 03 19:06:56 2018 +0200 +++ b/src/Pure/PIDE/document.scala Sun Jun 03 20:37:16 2018 +0200 @@ -537,6 +537,8 @@ 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 messages: List[(XML.Tree, Position.T)] + def exports: List[Export.Entry] def find_command(id: Document_ID.Generic): Option[(Node, Command)] def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset) @@ -1006,6 +1008,22 @@ def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body = state.markup_to_XML(version, node_name, range, elements) + def messages: List[(XML.Tree, Position.T)] = + (for { + (command, start) <- + Document.Node.Commands.starts_pos( + node.commands.iterator, Token.Pos.file(node_name.node)) + pos = command.span.keyword_pos(start).position(command.span.name) + (_, tree) <- state.command_results(version, command).iterator + } yield (tree, pos)).toList + + def exports: List[Export.Entry] = + Command.Exports.merge( + for { + command <- node.commands.iterator + st <- state.command_states(version, command).iterator + } yield st.exports).iterator.map(_._2).toList + /* find command */ diff -r 5c579bb9adb1 -r f9379279f98c src/Pure/Thy/thy_resources.scala --- a/src/Pure/Thy/thy_resources.scala Sun Jun 03 19:06:56 2018 +0200 +++ b/src/Pure/Thy/thy_resources.scala Sun Jun 03 20:37:16 2018 +0200 @@ -55,7 +55,7 @@ } } - sealed case class Theories_Result( + class Theories_Result private[Thy_Resources]( val state: Document.State, val version: Document.Version, val nodes: List[(Document.Node.Name, Protocol.Node_Status)]) @@ -63,32 +63,11 @@ def node_names: List[Document.Node.Name] = nodes.map(_._1) def ok: Boolean = nodes.forall({ case (_, st) => st.ok }) - def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] = + def snapshot(node_name: Document.Node.Name): Document.Snapshot = { - val node = version.nodes(node_name) - (for { - (command, start) <- - Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node)) - pos = command.span.keyword_pos(start).position(command.span.name) - (_, tree) <- state.command_results(version, command).iterator - } yield (tree, pos)).toList - } - - def markup_to_XML(node_name: Document.Node.Name, - range: Text.Range = Text.Range.full, - elements: Markup.Elements = Markup.Elements.full): XML.Body = - { - state.markup_to_XML(version, node_name, range, elements) - } - - def exports(node_name: Document.Node.Name): List[Export.Entry] = - { - val node = version.nodes(node_name) - Command.Exports.merge( - for { - command <- node.commands.iterator - st <- state.command_states(version, command).iterator - } yield st.exports).iterator.map(_._2).toList + val snapshot = state.snapshot(node_name) + assert(version.id == snapshot.version.id) + snapshot } } @@ -134,7 +113,7 @@ val nodes = for (name <- dep_theories) yield (name -> Protocol.node_status(state, version, name)) - try { result.fulfill(Theories_Result(state, version, nodes)) } + try { result.fulfill(new Theories_Result(state, version, nodes)) } catch { case _: IllegalStateException => } case _ => } diff -r 5c579bb9adb1 -r f9379279f98c src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Sun Jun 03 19:06:56 2018 +0200 +++ b/src/Pure/Tools/dump.scala Sun Jun 03 20:37:16 2018 +0200 @@ -14,22 +14,24 @@ sealed case class Aspect_Args( options: Options, progress: Progress, + deps: Sessions.Deps, output_dir: Path, - deps: Sessions.Deps, - result: Thy_Resources.Theories_Result) + node_name: Document.Node.Name, + node_status: Protocol.Node_Status, + snapshot: Document.Snapshot) { - def write(node_name: Document.Node.Name, file_name: Path, bytes: Bytes) + def write(file_name: Path, bytes: Bytes) { val path = output_dir + Path.basic(node_name.theory) + file_name Isabelle_System.mkdirs(path.dir) Bytes.write(path, bytes) } - def write(node_name: Document.Node.Name, file_name: Path, text: String): Unit = - write(node_name, file_name, Bytes(text)) + def write(file_name: Path, text: String): Unit = + write(file_name, Bytes(text)) - def write(node_name: Document.Node.Name, file_name: Path, body: XML.Body): Unit = - write(node_name, file_name, Symbol.encode(YXML.string_of_body(body))) + def write(file_name: Path, body: XML.Body): Unit = + write(file_name, Symbol.encode(YXML.string_of_body(body))) } sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit, @@ -40,35 +42,27 @@ val known_aspects = List( + Aspect("markup", "PIDE markup (YXML format)", + { case args => + args.write(Path.explode("markup.yxml"), + args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full)) + }), Aspect("messages", "output messages (YXML format)", { case args => - for (node_name <- args.result.node_names) { - args.write(node_name, Path.explode("messages.yxml"), - args.result.messages(node_name).iterator.map(_._1).toList) - } - }), - Aspect("markup", "PIDE markup (YXML format)", - { case args => - for (node_name <- args.result.node_names) { - args.write(node_name, Path.explode("markup.yxml"), - args.result.markup_to_XML(node_name)) - } + args.write(Path.explode("messages.yxml"), + args.snapshot.messages.iterator.map(_._1).toList) }), Aspect("latex", "generated LaTeX source", { case args => - for { - node_name <- args.result.node_names - entry <- args.result.exports(node_name) - if entry.name == "document.tex" - } args.write(node_name, Path.explode(entry.name), entry.uncompressed()) + for (entry <- args.snapshot.exports if entry.name == "document.tex") + args.write(Path.explode(entry.name), entry.uncompressed()) }, options = List("editor_presentation")), Aspect("theory", "foundational theory content", { case args => for { - node_name <- args.result.node_names - entry <- args.result.exports(node_name) + entry <- args.snapshot.exports if entry.name.startsWith(Export_Theory.export_prefix) - } args.write(node_name, Path.explode(entry.name), entry.uncompressed()) + } args.write(Path.explode(entry.name), entry.uncompressed()) }, options = List("editor_presentation", "export_theory")) ).sortBy(_.name) @@ -129,8 +123,12 @@ /* dump aspects */ - val aspect_args = Aspect_Args(dump_options, progress, output_dir, deps, theories_result) - aspects.foreach(_.operation(aspect_args)) + for ((node_name, node_status) <- theories_result.nodes) { + val snapshot = theories_result.snapshot(node_name) + val aspect_args = + Aspect_Args(dump_options, progress, deps, output_dir, node_name, node_status, snapshot) + aspects.foreach(_.operation(aspect_args)) + } session_result } diff -r 5c579bb9adb1 -r f9379279f98c src/Pure/Tools/server_commands.scala --- a/src/Pure/Tools/server_commands.scala Sun Jun 03 19:06:56 2018 +0200 +++ b/src/Pure/Tools/server_commands.scala Sun Jun 03 20:37:16 2018 +0200 @@ -205,25 +205,27 @@ "errors" -> (for { (name, status) <- result.nodes if !status.ok - (tree, pos) <- result.messages(name) if Protocol.is_error(tree) + (tree, pos) <- result.snapshot(name).messages if Protocol.is_error(tree) } yield output_message(tree, pos)), "nodes" -> - (for ((name, status) <- result.nodes) yield + (for ((name, status) <- result.nodes) yield { + val snapshot = result.snapshot(name) name.json + ("status" -> status.json) + ("messages" -> (for { - (tree, pos) <- result.messages(name) if Protocol.is_exported(tree) + (tree, pos) <- snapshot.messages if Protocol.is_exported(tree) } yield output_message(tree, pos))) + ("exports" -> (if (args.export_pattern == "") Nil else { val matcher = Export.make_matcher(args.export_pattern) - for { entry <- result.exports(name) if matcher(entry.theory_name, entry.name) } + for { entry <- snapshot.exports if matcher(entry.theory_name, entry.name) } yield { val (base64, body) = entry.uncompressed().maybe_base64 JSON.Object("name" -> entry.name, "base64" -> base64, "body" -> body) } - })))) + })) + })) (result_json, result) }