--- a/src/Doc/System/Server.thy Tue May 29 20:01:50 2018 +0200
+++ b/src/Doc/System/Server.thy Tue May 29 22:29:32 2018 +0200
@@ -516,13 +516,14 @@
session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
\<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
- int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
- represents a formal theory node status of the PIDE document model. Fields
- \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close> account
- for individual commands within a theory node; \<open>ok\<close> is an abstraction for
- \<open>failed = 0\<close>. The \<open>consolidated\<close> flag indicates whether the outermost theory
- command structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has
- been checked.
+ int, warned: int, failed: int, finished: int, initialized: bool,
+ consolidated: bool}\<close> represents a formal theory node status of the PIDE
+ document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>,
+ \<open>failed\<close>, \<open>finished\<close> account for individual commands within a theory node;
+ \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>initialized\<close> flag indicates
+ that the initial \<^theory_text>\<open>theory\<close> command has been processed. The \<open>consolidated\<close>
+ flag indicates whether the outermost theory command structure has finished
+ (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
\<close>
--- a/src/Doc/System/Sessions.thy Tue May 29 20:01:50 2018 +0200
+++ b/src/Doc/System/Sessions.thy Tue May 29 22:29:32 2018 +0200
@@ -557,7 +557,7 @@
\<open>Usage: isabelle export [OPTIONS] SESSION
Options are:
- -D DIR target directory for exported files (default: "export")
+ -O DIR output directory for exported files (default: "export")
-d DIR include session directory
-l list exports
-n no build of session
@@ -590,7 +590,7 @@
\<^emph>\<open>all\<close> theory exports. Multiple options \<^verbatim>\<open>-x\<close> refer to the union of all
specified patterns.
- Option \<^verbatim>\<open>-D\<close> specifies an alternative base directory for option \<^verbatim>\<open>-x\<close>: the
+ Option \<^verbatim>\<open>-O\<close> specifies an alternative output directory for option \<^verbatim>\<open>-x\<close>: the
default is \<^verbatim>\<open>export\<close> within the current directory. Each theory creates its
own sub-directory hierarchy, using the session-qualified theory name.
\<close>
--- a/src/Pure/General/exn.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/General/exn.scala Tue May 29 22:29:32 2018 +0200
@@ -81,6 +81,10 @@
found_interrupt
}
+ def interruptible_capture[A](e: => A): Result[A] =
+ try { Res(e) }
+ catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
+
object Interrupt
{
def apply(): Throwable = new InterruptedException
--- a/src/Pure/General/graph.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/General/graph.scala Tue May 29 22:29:32 2018 +0200
@@ -66,6 +66,7 @@
def is_empty: Boolean = rep.isEmpty
def defined(x: Key): Boolean = rep.isDefinedAt(x)
+ def domain: Set[Key] = rep.keySet
def iterator: Iterator[(Key, Entry)] = rep.iterator
--- a/src/Pure/PIDE/command.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/PIDE/command.scala Tue May 29 22:29:32 2018 +0200
@@ -260,6 +260,8 @@
exports: Exports = Exports.empty,
markups: Markups = Markups.empty)
{
+ def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED)
+
lazy val consolidated: Boolean =
status.exists(markup => markup.name == Markup.CONSOLIDATED)
@@ -565,6 +567,8 @@
val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
+ def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
+
/* blobs */
--- a/src/Pure/PIDE/document.ML Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/PIDE/document.ML Tue May 29 22:29:32 2018 +0200
@@ -633,7 +633,9 @@
val parents =
if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports;
val _ = Position.reports (map #2 parents_reports);
- in Resources.begin_theory master_dir header parents end;
+ val thy = Resources.begin_theory master_dir header parents;
+ val _ = Output.status (Markup.markup_only Markup.initialized);
+ in thy end;
fun check_root_theory node =
let
--- a/src/Pure/PIDE/document.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/PIDE/document.scala Tue May 29 22:29:32 2018 +0200
@@ -383,6 +383,8 @@
new Nodes(graph3.map_node(name, _ => node))
}
+ def domain: Set[Node.Name] = graph.domain
+
def iterator: Iterator[(Node.Name, Node)] =
graph.iterator.map({ case (name, (node, _)) => (name, node) })
@@ -529,7 +531,6 @@
def node_name: Node.Name
def node: Node
- def node_consolidated: Boolean
def commands_loading: List[Command]
def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
@@ -920,6 +921,13 @@
}
}
+ def node_initialized(version: Version, name: Node.Name): Boolean =
+ name.is_theory &&
+ (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
+ case None => false
+ case Some(command) => command_states(version, command).headOption.exists(_.initialized)
+ })
+
def node_consolidated(version: Version, name: Node.Name): Boolean =
!name.is_theory ||
version.nodes(name).commands.reverse.iterator.
@@ -969,8 +977,6 @@
val node_name: Node.Name = name
val node: Node = version.nodes(name)
- def node_consolidated: Boolean = state.node_consolidated(version, node_name)
-
val commands_loading: List[Command] =
if (node_name.is_theory) Nil
else version.nodes.commands_loading(node_name)
--- a/src/Pure/PIDE/markup.ML Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/PIDE/markup.ML Tue May 29 22:29:32 2018 +0200
@@ -167,6 +167,7 @@
val runningN: string val running: T
val finishedN: string val finished: T
val failedN: string val failed: T
+ val initializedN: string val initialized: T
val consolidatedN: string val consolidated: T
val exec_idN: string
val initN: string
@@ -580,6 +581,8 @@
val (runningN, running) = markup_elem "running";
val (finishedN, finished) = markup_elem "finished";
val (failedN, failed) = markup_elem "failed";
+
+val (initializedN, initialized) = markup_elem "initialized";
val (consolidatedN, consolidated) = markup_elem "consolidated";
--- a/src/Pure/PIDE/markup.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/PIDE/markup.scala Tue May 29 22:29:32 2018 +0200
@@ -426,6 +426,8 @@
val RUNNING = "running"
val FINISHED = "finished"
val FAILED = "failed"
+
+ val INITIALIZED = "initialized"
val CONSOLIDATED = "consolidated"
--- a/src/Pure/PIDE/protocol.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/PIDE/protocol.scala Tue May 29 22:29:32 2018 +0200
@@ -142,7 +142,8 @@
/* node status */
sealed case class Node_Status(
- unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
+ unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
+ initialized: Boolean, consolidated: Boolean)
{
def ok: Boolean = failed == 0
def total: Int = unprocessed + running + warned + failed + finished
@@ -150,15 +151,16 @@
def json: JSON.Object.T =
JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
"running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
- "consolidated" -> consolidated)
+ "initialized" -> initialized, "consolidated" -> consolidated)
}
def node_status(
state: Document.State,
version: Document.Version,
- name: Document.Node.Name,
- node: Document.Node): Node_Status =
+ name: Document.Node.Name): Node_Status =
{
+ val node = version.nodes(name)
+
var unprocessed = 0
var running = 0
var warned = 0
@@ -174,9 +176,10 @@
else if (status.is_finished) finished += 1
else unprocessed += 1
}
+ val initialized = state.node_initialized(version, name)
val consolidated = state.node_consolidated(version, name)
- Node_Status(unprocessed, running, warned, failed, finished, consolidated)
+ Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
}
--- a/src/Pure/PIDE/resources.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/PIDE/resources.scala Tue May 29 22:29:32 2018 +0200
@@ -300,7 +300,7 @@
private def require_thy(
progress: Progress,
initiators: List[Document.Node.Name],
- required: Dependencies,
+ dependencies: Dependencies,
thy: (Document.Node.Name, Position.T)): Dependencies =
{
val (name, pos) = thy
@@ -309,10 +309,10 @@
"The error(s) above occurred for theory " + quote(name.theory) +
required_by(initiators) + Position.here(pos)
- if (required.seen(name)) required
+ if (dependencies.seen(name)) dependencies
else {
- val required1 = required + name
- if (session_base.loaded_theory(name)) required1
+ val dependencies1 = dependencies + name
+ if (session_base.loaded_theory(name)) dependencies1
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
@@ -322,11 +322,11 @@
try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
catch { case ERROR(msg) => cat_error(msg, message) }
Document.Node.Entry(name, header) ::
- require_thys(progress, name :: initiators, required1, header.imports)
+ require_thys(progress, name :: initiators, dependencies1, header.imports)
}
catch {
case e: Throwable =>
- Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
+ Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: dependencies1
}
}
}
@@ -335,9 +335,9 @@
private def require_thys(
progress: Progress,
initiators: List[Document.Node.Name],
- required: Dependencies,
+ dependencies: Dependencies,
thys: List[(Document.Node.Name, Position.T)]): Dependencies =
- (required /: thys)(require_thy(progress, initiators, _, _))
+ (dependencies /: thys)(require_thy(progress, initiators, _, _))
def dependencies(
thys: List[(Document.Node.Name, Position.T)],
--- a/src/Pure/Thy/export.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/Thy/export.scala Tue May 29 22:29:32 2018 +0200
@@ -251,7 +251,7 @@
Usage: isabelle export [OPTIONS] SESSION
Options are:
- -D DIR target directory for exported files (default: """ + default_export_dir + """)
+ -O DIR output directory for exported files (default: """ + default_export_dir + """)
-d DIR include session directory
-l list exports
-n no build of session
@@ -266,7 +266,7 @@
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
and variants {pattern1,pattern2,pattern3}.
""",
- "D:" -> (arg => export_dir = Path.explode(arg)),
+ "O:" -> (arg => export_dir = Path.explode(arg)),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l" -> (_ => export_list = true),
"n" -> (_ => no_build = true),
--- a/src/Pure/Thy/sessions.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/Thy/sessions.scala Tue May 29 22:29:32 2018 +0200
@@ -146,6 +146,7 @@
doc_names: List[String] = Nil,
global_theories: Map[String, String] = Map.empty,
loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
+ used_theories: List[Document.Node.Name] = Nil,
known: Known = Known.empty,
overall_syntax: Outer_Syntax = Outer_Syntax.empty,
imported_sources: List[(Path, SHA1.Digest)] = Nil,
@@ -349,6 +350,7 @@
doc_names = doc_names,
global_theories = global_theories,
loaded_theories = dependencies.loaded_theories,
+ used_theories = dependencies.theories,
known = known,
overall_syntax = overall_syntax,
imported_sources = check_sources(imported_files),
--- a/src/Pure/Thy/thy_resources.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala Tue May 29 22:29:32 2018 +0200
@@ -60,6 +60,7 @@
val version: Document.Version,
val nodes: List[(Document.Node.Name, Protocol.Node_Status)])
{
+ 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)] =
@@ -73,6 +74,13 @@
} 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)
@@ -125,7 +133,7 @@
case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) =>
val nodes =
for (name <- dep_theories)
- yield (name -> Protocol.node_status(state, version, name, version.nodes(name)))
+ yield (name -> Protocol.node_status(state, version, name))
try { result.fulfill(Theories_Result(state, version, nodes)) }
catch { case _: IllegalStateException => }
case _ =>
--- a/src/Pure/Tools/dump.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Pure/Tools/dump.scala Tue May 29 22:29:32 2018 +0200
@@ -9,12 +9,67 @@
object Dump
{
+ /* aspects */
+
+ sealed case class Aspect_Args(
+ options: Options, progress: Progress, output_dir: Path, result: Thy_Resources.Theories_Result)
+ {
+ def write(node_name: Document.Node.Name, file_name: String, bytes: Bytes)
+ {
+ val path = output_dir + Path.basic(node_name.theory) + Path.basic(file_name)
+ Isabelle_System.mkdirs(path.dir)
+ Bytes.write(path, bytes)
+ }
+
+ def write(node_name: Document.Node.Name, file_name: String, text: String)
+ {
+ write(node_name, file_name, Bytes(text))
+ }
+ }
+
+ sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit)
+
+ private val known_aspects =
+ List(
+ Aspect("list", "list theory nodes",
+ { case args =>
+ for (node_name <- args.result.node_names) args.progress.echo(node_name.toString)
+ }),
+ Aspect("messages", "output messages (YXML format)",
+ { case args =>
+ for (node_name <- args.result.node_names) {
+ args.write(node_name, "messages.yxml",
+ YXML.string_of_body(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, "markup.yxml",
+ YXML.string_of_body(args.result.markup_to_XML(node_name)))
+ }
+ })
+ )
+
+ def show_aspects: String =
+ cat_lines(known_aspects.sortBy(_.name).map(aspect => aspect.name + " - " + aspect.description))
+
+ def the_aspect(name: String): Aspect =
+ known_aspects.find(aspect => aspect.name == name) getOrElse
+ error("Unknown aspect " + quote(name))
+
+
+ /* dump */
+
+ val default_output_dir = Path.explode("dump")
+
def dump(options: Options, logic: String,
- consume: Thy_Resources.Theories_Result => Unit = _ => (),
+ aspects: List[Aspect] = Nil,
progress: Progress = No_Progress,
log: Logger = No_Logger,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
+ output_dir: Path = default_output_dir,
verbose: Boolean = false,
system_mode: Boolean = false,
selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
@@ -24,22 +79,37 @@
val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false)
+
+ /* dependencies */
+
val deps =
Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
selection_deps(selection)
+ val include_sessions =
+ deps.sessions_structure.imports_topological_order
+
+ val use_theories =
+ deps.sessions_structure.build_topological_order.
+ flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory))
+
+
+ /* session */
+
val session =
Thy_Resources.start_session(dump_options, logic, session_dirs = dirs,
- include_sessions = deps.sessions_structure.imports_topological_order,
- progress = progress, log = log)
+ include_sessions = include_sessions, progress = progress, log = log)
+
+ val theories_result = session.use_theories(use_theories, progress = progress)
+ val session_result = session.stop()
+
- val theories = deps.all_known.theory_graph.topological_order.map(_.theory)
- val theories_result = session.use_theories(theories, progress = progress)
+ /* dump aspects */
- try { consume(theories_result) }
- catch { case exn: Throwable => session.stop (); throw exn }
+ val aspect_args = Aspect_Args(dump_options, progress, output_dir, theories_result)
+ aspects.foreach(_.operation(aspect_args))
- session.stop()
+ session_result
}
@@ -48,8 +118,10 @@
val isabelle_tool =
Isabelle_Tool("dump", "dump build database produced by PIDE session.", args =>
{
+ var aspects: List[Aspect] = Nil
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
+ var output_dir = default_output_dir
var requirements = false
var exclude_session_groups: List[String] = Nil
var all_sessions = false
@@ -65,8 +137,10 @@
Usage: isabelle dump [OPTIONS] [SESSIONS ...]
Options are:
+ -A NAMES dump named aspects (comma-separated list, see below)
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
+ -O DIR output directory for dumped files (default: """ + default_output_dir + """)
-R operate on requirements of selected sessions
-X NAME exclude sessions from group NAME and all descendants
-a select all sessions
@@ -78,9 +152,14 @@
-v verbose
-x NAME exclude session NAME and all descendants
- Dump build database (PIDE markup etc.) based on dynamic session.""",
+ Dump build database produced by PIDE session. The following dump aspects
+ are known (option -A):
+
+""" + Library.prefix_lines(" ", show_aspects) + "\n",
+ "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))),
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "O:" -> (arg => output_dir = Path.explode(arg)),
"R" -> (_ => requirements = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
"a" -> (_ => all_sessions = true),
@@ -96,18 +175,13 @@
val progress = new Console_Progress(verbose = verbose)
- def consume(theories_result: Thy_Resources.Theories_Result)
- {
- // FIXME
- for ((node, _) <- theories_result.nodes) progress.echo(node.toString)
- }
-
val result =
dump(options, logic,
- consume = consume _,
+ aspects = aspects,
progress = progress,
dirs = dirs,
select_dirs = select_dirs,
+ output_dir = output_dir,
verbose = verbose,
selection = Sessions.Selection(
requirements = requirements,
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue May 29 20:01:50 2018 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue May 29 22:29:32 2018 +0200
@@ -228,21 +228,17 @@
val snapshot = PIDE.session.snapshot()
val nodes = snapshot.version.nodes
- val iterator =
- restriction match {
- case Some(names) => names.iterator.map(name => (name, nodes(name)))
- case None => nodes.iterator
- }
val nodes_status1 =
- (nodes_status /: iterator)({ case (status, (name, node)) =>
- if (PIDE.resources.is_hidden(name) ||
- PIDE.resources.session_base.loaded_theory(name) ||
- node.is_empty) status
- else {
- val st = Protocol.node_status(snapshot.state, snapshot.version, name, node)
- status + (name -> st)
- }
- })
+ (nodes_status /: (restriction.getOrElse(nodes.domain).iterator))(
+ { case (status, name) =>
+ if (PIDE.resources.is_hidden(name) ||
+ PIDE.resources.session_base.loaded_theory(name) ||
+ nodes(name).is_empty) status
+ else {
+ val st = Protocol.node_status(snapshot.state, snapshot.version, name)
+ status + (name -> st)
+ }
+ })
val nodes_status2 =
nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_suppressed(_))