--- 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 */
--- 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 _ =>
}
--- 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
}
--- 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)
}