# HG changeset patch
# User wenzelm
# Date 1521844319 -3600
# Node ID 49a34b2fa788b6803878aaead7d152f0e6bc6021
# Parent  b4e80f062fbfbc6deef66d269ee67ac2f8d3ca1c
added command "purge_theories";
proper documentation: command "use_theories" is asynchronous;

diff -r b4e80f062fbf -r 49a34b2fa788 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Fri Mar 23 22:53:32 2018 +0100
+++ b/src/Doc/System/Server.thy	Fri Mar 23 23:31:59 2018 +0100
@@ -873,7 +873,8 @@
 text \<open>
   \begin{tabular}{ll}
   argument: & \<open>use_theories_arguments\<close> \\
-  regular result: & \<^verbatim>\<open>OK\<close> \<open>use_theories_results\<close> \\
+  immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
+  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>use_theories_results\<close> \\
   \end{tabular}
 
   \begin{tabular}{ll}
@@ -906,10 +907,11 @@
   (\secref{sec:json-types}): the outermost command structure has finished (or
   failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
 
-  Already used theories persist in the session until purged explicitly. This
-  also means that repeated invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it
-  could make sense to do that with different values for \<open>pretty_margin\<close> or
-  \<open>unicode_symbols\<close> to get different formatting for \<open>errors\<close> or \<open>messages\<close>.
+  Already used theories persist in the session until purged explicitly
+  (\secref{sec:command-purge-theories}). This also means that repeated
+  invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it could make sense to do
+  that with different values for \<open>pretty_margin\<close> or \<open>unicode_symbols\<close> to get
+  different formatting for \<open>errors\<close> or \<open>messages\<close>.
 \<close>
 
 
@@ -923,11 +925,12 @@
   The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
   ROOT \<^bold>\<open>theories\<close>.
 
-  \<^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>).
+  \<^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>).
 
   \<^medskip>
   The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
@@ -996,4 +999,61 @@
 session_stop {"session_id": ...}\<close>}
 \<close>
 
+
+subsection \<open>Command \<^verbatim>\<open>purge_theories\<close> \label{sec:command-purge-theories}\<close>
+
+text \<open>
+  \begin{tabular}{ll}
+  argument: & \<open>purge_theories_arguments\<close> \\
+  regular result: & \<^verbatim>\<open>OK\<close> \<open>purge_theories_result\<close> \\
+  \end{tabular}
+
+  \begin{tabular}{ll}
+  \<^bold>\<open>type\<close> \<open>purge_theories_arguments =\<close> \\
+  \quad\<open>{session_id: uuid,\<close> \\
+  \quad~~\<open>theories: [string],\<close> \\
+  \quad~~\<open>master_dir?: string,\<close> \\
+  \quad~~\<open>all?: bool}\<close> \\[2ex]
+  \end{tabular}
+
+  \begin{tabular}{ll}
+  \<^bold>\<open>type\<close> \<open>purge_theories_result = {purged: [string]}\<close> \\
+  \end{tabular}
+
+  \<^medskip>
+  The \<^verbatim>\<open>purge_theories\<close> command updates the identified session by removing
+  theories that are no longer required: theories that are used in pending
+  \<^verbatim>\<open>use_theories\<close> tasks or imported by other theories are retained.
+\<close>
+
+
+subsubsection \<open>Arguments\<close>
+
+text \<open>
+  The \<open>session_id\<close> is the identifier provided by the server, when the session
+  was created (possibly on a different client connection).
+
+  \<^medskip>
+  The \<open>theories\<close> field specifies theory names to be purged: imported
+  dependencies are \<^emph>\<open>not\<close> completed. Instead it is possible to provide the
+  already completed import graph returned by \<^verbatim>\<open>use_theories\<close> as \<open>nodes\<close> /
+  \<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.
+
+  \<^medskip>
+  The \<open>all\<close> field set to \<^verbatim>\<open>true\<close> attempts to purge all presently loaded
+  theories.
+\<close>
+
+
+subsubsection \<open>Results\<close>
+
+text \<open>
+  The \<open>purged\<close> field reveals the \<open>node_name\<close> of each theory that was actually
+  removed.
+\<close>
+
 end
diff -r b4e80f062fbf -r 49a34b2fa788 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Fri Mar 23 22:53:32 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 23 23:31:59 2018 +0100
@@ -102,7 +102,12 @@
                   val session = context.server.the_session(args.session_id)
                   Server_Commands.Use_Theories.command(
                     args, session, id = task.id, progress = task.progress)._1
-                })
+                }),
+          },
+        "purge_theories" ->
+          { case (context, Server_Commands.Purge_Theories(args)) =>
+              val session = context.server.the_session(args.session_id)
+              Server_Commands.Purge_Theories.command(args, session)._1
           })
 
     def unapply(name: String): Option[T] = table.get(name)
diff -r b4e80f062fbf -r 49a34b2fa788 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:53:32 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 23:31:59 2018 +0100
@@ -219,4 +219,31 @@
       (result_json, result)
     }
   }
+
+  object Purge_Theories
+  {
+    sealed case class Args(
+      session_id: UUID,
+      theories: List[String] = Nil,
+      master_dir: String = "",
+      all: Boolean = false)
+
+    def unapply(json: JSON.T): Option[Args] =
+      for {
+        session_id <- JSON.uuid(json, "session_id")
+        theories <- JSON.list_default(json, "theories", JSON.Value.String.unapply _)
+        master_dir <- JSON.string_default(json, "master_dir")
+        all <- JSON.bool_default(json, "all")
+      }
+      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]) =
+    {
+      val purged =
+        session.purge_theories(
+          theories = args.theories, master_dir = args.master_dir, all = args.all)
+      (JSON.Object("purged" -> purged.map(_.node)), purged)
+    }
+  }
 }