clarified theory node name;
purge_theories: return purged, retained;
tuned documentation;
--- a/src/Doc/System/Server.thy Sat Mar 24 15:07:13 2018 +0100
+++ b/src/Doc/System/Server.thy Sat Mar 24 20:45:30 2018 +0100
@@ -509,6 +509,12 @@
connections and may be shared by different clients, as long as the internal
session identifier is known.
+ \<^item> \<^bold>\<open>type\<close> \<open>node = {node_name: string, theory_name: string}\<close> represents the
+ internal node name of a theory. The \<open>node_name\<close> is derived from the
+ canonical theory file-name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close> after
+ normalization within the file-system). The \<open>theory_name\<close> is the
+ 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
@@ -888,15 +894,13 @@
\begin{tabular}{ll}
\<^bold>\<open>type\<close> \<open>node_result =\<close> \\
- \quad\<open>{node_name: string,\<close> \\
- \quad~~\<open>theory: string,\<close> \\
- \quad~~\<open>status: node_status,\<close> \\
+ \quad\<open>{status: node_status,\<close> \\
\quad~~\<open>messages: [message]}\<close> \\[2ex]
\<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
\quad\<open>{ok: bool,\<close> \\
\quad~~\<open>errors: [message],\<close> \\
- \quad~~\<open>nodes: [node_result]}\<close> \\[2ex]
+ \quad~~\<open>nodes: [node \<oplus> node_result]}\<close> \\[2ex]
\end{tabular}
\<^medskip>
@@ -928,9 +932,9 @@
\<^medskip>
The \<open>master_dir\<close> field specifies the master directory of imported theories:
it acts like the ``current working directory'' for locating theory files.
- This may be omitted if all entries of \<open>theories\<close> use a session-qualified
- theory name (e.g.\ \<^verbatim>\<open>"HOL-Library.AList"\<close>) or absolute path name (e.g.\
- \<^verbatim>\<open>"~~/src/HOL/ex/Seq"\<close>).
+ This may be omitted if all entries of \<open>theories\<close> use an absolute path name
+ (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq.thy"\<close>) or session-qualified theory name (e.g.\
+ \<^verbatim>\<open>"HOL-ex/Seq"\<close>).
\<^medskip>
The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
@@ -961,10 +965,10 @@
The \<open>nodes\<close> field provides detailed information about each imported theory
node. The individual fields are as follows:
- \<^item> \<open>node_name\<close>: the physical name for the theory node, based on its
+ \<^item> \<open>node_name\<close>: the canonical name for the theory node, based on its
file-system location;
- \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close>;
+ \<^item> \<open>theory_name\<close>: the logical theory name;
\<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
\<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
@@ -1040,8 +1044,9 @@
\<open>node_name\<close>.
\<^medskip>
- The \<open>master_dir\<close> field specifies the master directory as in \<^verbatim>\<open>use_theories\<close>;
- by passing its \<open>nodes\<close> / \<open>node_name\<close> results, the \<open>master_dir\<close> is redundant.
+ The \<open>master_dir\<close> field specifies the master directory as in \<^verbatim>\<open>use_theories\<close>.
+ It is redundant, when passing fully-qualified theory node names (e.g.\
+ \<open>node_name\<close> from \<open>nodes\<close> in \<open>use_theories_results\<close>).
\<^medskip>
The \<open>all\<close> field set to \<^verbatim>\<open>true\<close> attempts to purge all presently loaded
@@ -1052,8 +1057,11 @@
subsubsection \<open>Results\<close>
text \<open>
- The \<open>purged\<close> field reveals the \<open>node_name\<close> of each theory that was actually
- removed.
+ The \<open>purged\<close> field gives the theory nodes that were actually removed.
+
+ \<^medskip>
+ The \<open>retained\<close> field gives the remaining theory nodes, i.e.\ the complement
+ of \<open>purged\<close>.
\<close>
end
--- a/src/Pure/PIDE/document.scala Sat Mar 24 15:07:13 2018 +0100
+++ b/src/Pure/PIDE/document.scala Sat Mar 24 20:45:30 2018 +0100
@@ -130,6 +130,9 @@
def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
+
+ def json: JSON.Object.T =
+ JSON.Object("node_name" -> node, "theory_name" -> theory)
}
sealed case class Entry(name: Node.Name, header: Node.Header)
--- a/src/Pure/Thy/thy_resources.scala Sat Mar 24 15:07:13 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala Sat Mar 24 20:45:30 2018 +0100
@@ -142,7 +142,7 @@
theories: List[String],
qualifier: String = Sessions.DRAFT,
master_dir: String = "",
- all: Boolean = false): List[Document.Node.Name] =
+ all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
resources.purge_theories(session, theories = theories, qualifier = qualifier,
master_dir = master_dir, all = all)
}
@@ -294,7 +294,7 @@
theories: List[String],
qualifier: String = Sessions.DRAFT,
master_dir: String = "",
- all: Boolean = false): List[Document.Node.Name] =
+ all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
{
val nodes = theories.map(import_name(qualifier, master_dir, _))
@@ -306,12 +306,14 @@
val purge =
(if (all) all_nodes else nodes.filter(graph.defined(_))).
filterNot(st.is_required(_)).toSet
- val purged = all_nodes.filterNot(graph.all_preds(all_nodes.filterNot(purge)).toSet)
+
+ val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet
+ val (retained, purged) = all_nodes.partition(retain)
val purge_edits = purged.flatMap(name => st.theories(name).purge_edits)
session.update(Document.Blobs.empty, purge_edits)
- (purged, st.remove_theories(purged))
+ ((purged, retained), st.remove_theories(purged))
})
}
}
--- a/src/Pure/Tools/server_commands.scala Sat Mar 24 15:07:13 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Sat Mar 24 20:45:30 2018 +0100
@@ -208,11 +208,9 @@
} yield output_message(tree, pos)),
"nodes" ->
(for ((name, status) <- result.nodes) yield
- JSON.Object(
- "node_name" -> name.node,
- "theory" -> name.theory,
- "status" -> status.json,
- "messages" ->
+ name.json +
+ ("status" -> status.json) +
+ ("messages" ->
(for ((tree, pos) <- result.messages(name))
yield output_message(tree, pos)))))
@@ -238,12 +236,16 @@
yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
def command(args: Args, session: Thy_Resources.Session)
- : (JSON.Object.T, List[Document.Node.Name]) =
+ : (JSON.Object.T, (List[Document.Node.Name], List[Document.Node.Name])) =
{
- val purged =
+ val (purged, retained) =
session.purge_theories(
theories = args.theories, master_dir = args.master_dir, all = args.all)
- (JSON.Object("purged" -> purged.map(_.node)), purged)
+
+ val result_json =
+ JSON.Object("purged" -> purged.map(_.json), "retained" -> retained.map(_.json))
+
+ (result_json, (purged, retained))
}
}
}