# HG changeset patch
# User wenzelm
# Date 1521920730 -3600
# Node ID b45f0c0ea14f51ebcf3160b535164d844db24dd6
# Parent  a3e5f08e6b589d93560646e6620a5002dfa59657
clarified theory node name;
purge_theories: return purged, retained;
tuned documentation;

diff -r a3e5f08e6b58 -r b45f0c0ea14f src/Doc/System/Server.thy
--- 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
diff -r a3e5f08e6b58 -r b45f0c0ea14f src/Pure/PIDE/document.scala
--- 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)
diff -r a3e5f08e6b58 -r b45f0c0ea14f src/Pure/Thy/thy_resources.scala
--- 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))
       })
   }
 }
diff -r a3e5f08e6b58 -r b45f0c0ea14f src/Pure/Tools/server_commands.scala
--- 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))
     }
   }
 }