added command "purge_theories";
authorwenzelm
Fri Mar 23 23:31:59 2018 +0100 (14 months ago)
changeset 6794149a34b2fa788
parent 67940 b4e80f062fbf
child 67942 a3e5f08e6b58
added command "purge_theories";
proper documentation: command "use_theories" is asynchronous;
src/Doc/System/Server.thy
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Doc/System/Server.thy	Fri Mar 23 22:53:32 2018 +0100
     1.2 +++ b/src/Doc/System/Server.thy	Fri Mar 23 23:31:59 2018 +0100
     1.3 @@ -873,7 +873,8 @@
     1.4  text \<open>
     1.5    \begin{tabular}{ll}
     1.6    argument: & \<open>use_theories_arguments\<close> \\
     1.7 -  regular result: & \<^verbatim>\<open>OK\<close> \<open>use_theories_results\<close> \\
     1.8 +  immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
     1.9 +  regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>use_theories_results\<close> \\
    1.10    \end{tabular}
    1.11  
    1.12    \begin{tabular}{ll}
    1.13 @@ -906,10 +907,11 @@
    1.14    (\secref{sec:json-types}): the outermost command structure has finished (or
    1.15    failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
    1.16  
    1.17 -  Already used theories persist in the session until purged explicitly. This
    1.18 -  also means that repeated invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it
    1.19 -  could make sense to do that with different values for \<open>pretty_margin\<close> or
    1.20 -  \<open>unicode_symbols\<close> to get different formatting for \<open>errors\<close> or \<open>messages\<close>.
    1.21 +  Already used theories persist in the session until purged explicitly
    1.22 +  (\secref{sec:command-purge-theories}). This also means that repeated
    1.23 +  invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it could make sense to do
    1.24 +  that with different values for \<open>pretty_margin\<close> or \<open>unicode_symbols\<close> to get
    1.25 +  different formatting for \<open>errors\<close> or \<open>messages\<close>.
    1.26  \<close>
    1.27  
    1.28  
    1.29 @@ -923,11 +925,12 @@
    1.30    The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
    1.31    ROOT \<^bold>\<open>theories\<close>.
    1.32  
    1.33 -  \<^medskip> The \<open>master_dir\<close> field specifies the master directory of imported
    1.34 -  theories: it acts like the ``current working directory'' for locating theory
    1.35 -  files. This may be omitted if all entries of \<open>theories\<close> use a
    1.36 -  session-qualified theory name (e.g.\ \<^verbatim>\<open>"HOL-Library.AList"\<close>) or absolute
    1.37 -  path name (e.g.\ \<^verbatim>\<open>"~~/src/HOL/ex/Seq"\<close>).
    1.38 +  \<^medskip>
    1.39 +  The \<open>master_dir\<close> field specifies the master directory of imported theories:
    1.40 +  it acts like the ``current working directory'' for locating theory files.
    1.41 +  This may be omitted if all entries of \<open>theories\<close> use a session-qualified
    1.42 +  theory name (e.g.\ \<^verbatim>\<open>"HOL-Library.AList"\<close>) or absolute path name (e.g.\
    1.43 +  \<^verbatim>\<open>"~~/src/HOL/ex/Seq"\<close>).
    1.44  
    1.45    \<^medskip>
    1.46    The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
    1.47 @@ -996,4 +999,61 @@
    1.48  session_stop {"session_id": ...}\<close>}
    1.49  \<close>
    1.50  
    1.51 +
    1.52 +subsection \<open>Command \<^verbatim>\<open>purge_theories\<close> \label{sec:command-purge-theories}\<close>
    1.53 +
    1.54 +text \<open>
    1.55 +  \begin{tabular}{ll}
    1.56 +  argument: & \<open>purge_theories_arguments\<close> \\
    1.57 +  regular result: & \<^verbatim>\<open>OK\<close> \<open>purge_theories_result\<close> \\
    1.58 +  \end{tabular}
    1.59 +
    1.60 +  \begin{tabular}{ll}
    1.61 +  \<^bold>\<open>type\<close> \<open>purge_theories_arguments =\<close> \\
    1.62 +  \quad\<open>{session_id: uuid,\<close> \\
    1.63 +  \quad~~\<open>theories: [string],\<close> \\
    1.64 +  \quad~~\<open>master_dir?: string,\<close> \\
    1.65 +  \quad~~\<open>all?: bool}\<close> \\[2ex]
    1.66 +  \end{tabular}
    1.67 +
    1.68 +  \begin{tabular}{ll}
    1.69 +  \<^bold>\<open>type\<close> \<open>purge_theories_result = {purged: [string]}\<close> \\
    1.70 +  \end{tabular}
    1.71 +
    1.72 +  \<^medskip>
    1.73 +  The \<^verbatim>\<open>purge_theories\<close> command updates the identified session by removing
    1.74 +  theories that are no longer required: theories that are used in pending
    1.75 +  \<^verbatim>\<open>use_theories\<close> tasks or imported by other theories are retained.
    1.76 +\<close>
    1.77 +
    1.78 +
    1.79 +subsubsection \<open>Arguments\<close>
    1.80 +
    1.81 +text \<open>
    1.82 +  The \<open>session_id\<close> is the identifier provided by the server, when the session
    1.83 +  was created (possibly on a different client connection).
    1.84 +
    1.85 +  \<^medskip>
    1.86 +  The \<open>theories\<close> field specifies theory names to be purged: imported
    1.87 +  dependencies are \<^emph>\<open>not\<close> completed. Instead it is possible to provide the
    1.88 +  already completed import graph returned by \<^verbatim>\<open>use_theories\<close> as \<open>nodes\<close> /
    1.89 +  \<open>node_name\<close>.
    1.90 +
    1.91 +  \<^medskip>
    1.92 +  The \<open>master_dir\<close> field specifies the master directory as in \<^verbatim>\<open>use_theories\<close>;
    1.93 +  by passing its \<open>nodes\<close> / \<open>node_name\<close> results, the \<open>master_dir\<close> is redundant.
    1.94 +
    1.95 +  \<^medskip>
    1.96 +  The \<open>all\<close> field set to \<^verbatim>\<open>true\<close> attempts to purge all presently loaded
    1.97 +  theories.
    1.98 +\<close>
    1.99 +
   1.100 +
   1.101 +subsubsection \<open>Results\<close>
   1.102 +
   1.103 +text \<open>
   1.104 +  The \<open>purged\<close> field reveals the \<open>node_name\<close> of each theory that was actually
   1.105 +  removed.
   1.106 +\<close>
   1.107 +
   1.108  end
     2.1 --- a/src/Pure/Tools/server.scala	Fri Mar 23 22:53:32 2018 +0100
     2.2 +++ b/src/Pure/Tools/server.scala	Fri Mar 23 23:31:59 2018 +0100
     2.3 @@ -102,7 +102,12 @@
     2.4                    val session = context.server.the_session(args.session_id)
     2.5                    Server_Commands.Use_Theories.command(
     2.6                      args, session, id = task.id, progress = task.progress)._1
     2.7 -                })
     2.8 +                }),
     2.9 +          },
    2.10 +        "purge_theories" ->
    2.11 +          { case (context, Server_Commands.Purge_Theories(args)) =>
    2.12 +              val session = context.server.the_session(args.session_id)
    2.13 +              Server_Commands.Purge_Theories.command(args, session)._1
    2.14            })
    2.15  
    2.16      def unapply(name: String): Option[T] = table.get(name)
     3.1 --- a/src/Pure/Tools/server_commands.scala	Fri Mar 23 22:53:32 2018 +0100
     3.2 +++ b/src/Pure/Tools/server_commands.scala	Fri Mar 23 23:31:59 2018 +0100
     3.3 @@ -219,4 +219,31 @@
     3.4        (result_json, result)
     3.5      }
     3.6    }
     3.7 +
     3.8 +  object Purge_Theories
     3.9 +  {
    3.10 +    sealed case class Args(
    3.11 +      session_id: UUID,
    3.12 +      theories: List[String] = Nil,
    3.13 +      master_dir: String = "",
    3.14 +      all: Boolean = false)
    3.15 +
    3.16 +    def unapply(json: JSON.T): Option[Args] =
    3.17 +      for {
    3.18 +        session_id <- JSON.uuid(json, "session_id")
    3.19 +        theories <- JSON.list_default(json, "theories", JSON.Value.String.unapply _)
    3.20 +        master_dir <- JSON.string_default(json, "master_dir")
    3.21 +        all <- JSON.bool_default(json, "all")
    3.22 +      }
    3.23 +      yield { Args(session_id, theories = theories, master_dir = master_dir, all = all) }
    3.24 +
    3.25 +    def command(args: Args, session: Thy_Resources.Session)
    3.26 +      : (JSON.Object.T, List[Document.Node.Name]) =
    3.27 +    {
    3.28 +      val purged =
    3.29 +        session.purge_theories(
    3.30 +          theories = args.theories, master_dir = args.master_dir, all = args.all)
    3.31 +      (JSON.Object("purged" -> purged.map(_.node)), purged)
    3.32 +    }
    3.33 +  }
    3.34  }