--- a/src/Doc/System/Server.thy Thu Mar 22 13:53:15 2018 +0100
+++ b/src/Doc/System/Server.thy Thu Mar 22 17:06:15 2018 +0100
@@ -76,28 +76,29 @@
\<^medskip>
Option \<^verbatim>\<open>-c\<close> connects the console in/out channels after the initial check
- for a suitable server process. Note that the @{tool client} tool
- (\secref{sec:tool-client}) provides a more convenient way to do this
- interactively, together with command-line editor support.
-
- \<^medskip>
- Option \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
- details.
-
- \<^medskip>
- Option \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a \<^verbatim>\<open>shutdown\<close>
- command.
+ for a suitable server process. Also note that the @{tool client} tool
+ (\secref{sec:tool-client}) provides a command-line editor to interact with
+ the server.
\<^medskip>
Option \<^verbatim>\<open>-L\<close> specifies a log file for exceptional output of internal server
and session operations.
+
+ \<^medskip>
+ Operation \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
+ details.
+
+ \<^medskip>
+ Operation \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a
+ \<^verbatim>\<open>shutdown\<close> command.
\<close>
subsection \<open>Client \label{sec:tool-client}\<close>
text \<open>
- The @{tool_def client} provides console interaction for Isabelle servers:
+ The @{tool_def client} tool provides console interaction for Isabelle
+ servers:
@{verbatim [display]
\<open>Usage: isabelle client [OPTIONS]
@@ -107,8 +108,8 @@
Console interaction for Isabelle server (with line-editor).\<close>}
- This is a convenient wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
- experimentation, wrapped into @{setting ISABELLE_LINE_EDITOR} if available.
+ This is a wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
+ experimentation, which uses @{setting ISABELLE_LINE_EDITOR} if available.
The server name is sufficient for identification, as the client can
determine the connection details from the local database of active servers.
@@ -126,10 +127,9 @@
Ensure that a particular server instance is running in the background:
@{verbatim [display] \<open>isabelle server -n test &\<close>}
- Here the first line of output presents the connection details:\<^footnote>\<open>This
- information may be used in an independent TCP client, while the
- Isabelle/Scala tool merely needs the server name to access the database of
- servers.\<close>
+ The first line of output presents the connection details:\<^footnote>\<open>This information
+ may be used in other TCP clients, without access to Isabelle/Scala and the
+ underlying database of running servers.\<close>
@{verbatim [display] \<open>server "test" = 127.0.0.1:4711 (password "XYZ")\<close>}
\<^medskip>
@@ -152,7 +152,7 @@
possible to reconnect again, and have multiple connections at the same time.
\<^medskip>
- Finally, exit the named server on the command-line:
+ Exit the named server on the command-line:
@{verbatim [display] \<open>isabelle server -n test -x\<close>}
\<close>
@@ -161,12 +161,12 @@
text \<open>
The Isabelle server listens on a regular TCP socket, using a line-oriented
- protocol of structured messages: input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
+ protocol of structured messages. Input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
(via \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>) are strictly alternating on the toplevel, but
commands may also return a \<^emph>\<open>task\<close> identifier to indicate an ongoing
asynchronous process that is joined later (via \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>).
Asynchronous \<^verbatim>\<open>NOTE\<close> messages may occur at any time: they are independent of
- the main command-reply protocol.
+ the main command-result protocol.
For example, the synchronous \<^verbatim>\<open>echo\<close> command immediately returns its
argument as \<^verbatim>\<open>OK\<close> result. In contrast, the asynchronous \<^verbatim>\<open>session_build\<close>
@@ -176,7 +176,7 @@
may emit asynchronous messages of the form \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>
to inform about its progress. Due to the explicit task identifier, the
client can show these messages in the proper context, e.g.\ a GUI window for
- the session build job.
+ this particular session build job.
\medskip Subsequently, the protocol message formats are described in further
detail.
@@ -191,22 +191,22 @@
particular length. Messages are written as a single chunk that is flushed
immediately.
- The message boundary is determined as follows:
+ Message boundaries are determined as follows:
\<^item> A \<^emph>\<open>short message\<close> consists of a single line: it is a sequence of
arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or
just LF.
- \<^item> A \<^emph>\<open>long message\<close> starts with a single line as above, which consists
- only of decimal digits: that is interpreted as length of the subsequent
- block of arbitrary bytes. A final line-terminator may be included here,
+ \<^item> A \<^emph>\<open>long message\<close> starts with a single that consists only of decimal
+ digits: these are interpreted as length of the subsequent block of
+ arbitrary bytes. A final line-terminator (as above) may be included here,
but is not required.
Messages in JSON format (see below) always fit on a single line, due to
escaping of newline characters within string literals. This is convenient
for interactive experimentation, but it can impact performance for very long
messages. If the message byte-length is given on the preceding line, the
- server can read the message efficiently as a single block.
+ server can read the message more efficiently as a single block.
\<close>
@@ -224,7 +224,7 @@
\<close>
-subsection \<open>Input and output messages\<close>
+subsection \<open>Input and output messages \label{sec:input-output-messages}\<close>
text \<open>
Server input and output messages have a uniform format as follows:
@@ -232,13 +232,13 @@
\<^item> \<open>name argument\<close> such that:
\<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
- ``\<^verbatim>\<open>_\<close>'' (underscore), or ``\<^verbatim>\<open>.\<close>'' (dot),
+ ``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
\<^item> the separator between \<open>name\<close> and \<open>argument\<close> is the longest possible
sequence of ASCII blanks (it could be empty, e.g.\ when the argument
starts with a quote or bracket),
- \<^item> \<open>argument\<close> is the rest of the message without the line terminator.
+ \<^item> \<open>argument\<close> is the rest of the message without line terminator.
\<^medskip>
Input messages are sent from the client to the server. Here the \<open>name\<close>
@@ -283,7 +283,8 @@
Whenever a new client opens the server socket, the initial message needs to
be its unique password. The server replies either with \<^verbatim>\<open>OK\<close> (and some
information about the Isabelle version) or by silent disconnection of what
- is considered an illegal connection attempt.
+ is considered an illegal connection attempt. Note that @{tool client}
+ already presents the correct password internally.
Server passwords are created as Universally Unique Identifier (UUID) in
Isabelle/Scala and stored in a per-user database, with restricted
@@ -301,7 +302,7 @@
Isabelle/Scala, with single argument and result (regular or error). Both the
argument and the result may consist of type \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close>.
An error result typically consists of a JSON object with error message and
- potentially further fields (this resembles exceptions in Scala).
+ potentially further result fields (this resembles exceptions in Scala).
These are the protocol exchanges for both cases of command execution:
\begin{center}
@@ -318,11 +319,11 @@
text \<open>
An \<^emph>\<open>asynchronous command\<close> corresponds to an ongoing process that finishes
- or fails eventually, while emitting arbitrary notifications intermediately.
- Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close> and
- the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad command
- syntax. For a running task, the termination is indicated later by
- \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result.
+ or fails eventually, while emitting arbitrary notifications in between.
+ Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close>
+ giving the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad
+ command syntax. For a running task, the termination is indicated later by
+ \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result value.
These are the protocol exchanges for various cases of command task
execution:
@@ -332,7 +333,6 @@
\<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> \\
intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
- intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
(a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
(b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\[3ex]
\<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
@@ -341,14 +341,673 @@
\end{center}
All asynchronous messages are decorated with the task identifier that was
- revealed in the immediate (synchronous) result. Thus it is possible to emit
- further asynchronous commands and dispatch the mingled stream of
+ revealed in the immediate (synchronous) result. Thus the client can
+ invoke further asynchronous commands and still dispatch the resulting stream of
asynchronous messages properly.
- The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
- prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result with error message
- \<^verbatim>\<open>Interrupt\<close>, but this is not guaranteed: the cancel event may come too
- late or the task may just ignore it.
+ The synchronous command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> tells the specified task
+ to terminate prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is
+ not guaranteed: the cancel event may come too late or the running process
+ may just ignore it.
+\<close>
+
+
+section \<open>Types for JSON values \label{sec:json-types}\<close>
+
+text \<open>
+ In order to specify concrete JSON types for command arguments and result
+ messages, the following type definition language shall be used:
+
+ \<^rail>\<open>
+ @{syntax type_def}: @'type' @{syntax name} '=' @{syntax type}
+ ;
+ @{syntax type}: @{syntax name} | @{syntax value} | 'any' | 'null' |
+ 'bool' | 'int' | 'long' | 'double' | 'string' | '[' @{syntax type} ']' |
+ '{' (@{syntax field_type} ',' *) '}' |
+ @{syntax type} '\<oplus>' @{syntax type} |
+ @{syntax type} '|' @{syntax type} |
+ '(' @{syntax type} ')'
+ ;
+ @{syntax field_type}: @{syntax name} ('?'?) ':' @{syntax type}
+ \<close>
+
+ This is a simplified variation of TypeScript
+ interfaces.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
+ The meaning of these types is specified wrt. the Isabelle/Scala
+ implementation as follows.
+
+ \<^item> A \<open>name\<close> refers to a type defined elsewhere. The environment of type
+ definitions is given informally: put into proper foundational order, it
+ needs to specify a strongly normalizing system of syntactic abbreviations;
+ type definitions may not be recursive.
+
+ \<^item> A \<open>value\<close> in JSON notation represents the singleton type of the given
+ item. For example, the string \<^verbatim>\<open>"error"\<close> can be used as type for a slot that
+ is guaranteed to contain that constant.
+
+ \<^item> Type \<open>any\<close> is the super type of all other types: it is an untyped slot in
+ the specification and corresponds to \<^verbatim>\<open>Any\<close> or \<^verbatim>\<open>JSON.T\<close> in Isabelle/Scala.
+
+ \<^item> Type \<open>null\<close> is the type of the improper value \<open>null\<close>; it corresponds to
+ type \<^verbatim>\<open>Null\<close> in Scala and is normally not used in Isabelle/Scala.\<^footnote>\<open>See also
+ ``Null References: The Billion Dollar Mistake'' by Tony Hoare
+ \<^url>\<open>https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\<close>.\<close>
+
+ \<^item> Type \<open>bool\<close> is the type of the truth values \<^verbatim>\<open>true\<close> and \<^verbatim>\<open>false\<close>; it
+ corresponds to \<^verbatim>\<open>Boolean\<close> in Scala.
+
+ \<^item> Types \<open>int\<close>, \<open>long\<close>, \<open>double\<close> are specific versions of the generic
+ \<open>number\<close> type, corresponding to \<^verbatim>\<open>Int\<close>, \<^verbatim>\<open>Long\<close>, \<^verbatim>\<open>Double\<close> in Scala, but
+ \<^verbatim>\<open>Long\<close> is limited to 53 bit precision.\<^footnote>\<open>Implementations of JSON typically
+ standardize \<open>number\<close> to \<^verbatim>\<open>Double\<close>, which can absorb \<^verbatim>\<open>Int\<close> faithfully, but
+ not all of \<^verbatim>\<open>Long\<close>.\<close>
+
+ \<^item> Type \<open>string\<close> represents Unicode text; it corresponds to type \<^verbatim>\<open>String\<close> in
+ Scala.
+
+ \<^item> Type \<open>[t]\<close> is the array (or list) type over \<open>t\<close>; it corresponds to
+ \<^verbatim>\<open>List[t]\<close> in Scala. The list type is co-variant as usual (i.e.\ monotonic
+ wrt. the subtype relation).
+
+ \<^item> Object types describe the possible content of JSON records, with field
+ names and types. A question mark after a field name means that it is
+ optional. In Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>, e.g.\
+ \<open>{a: int, b?: string}\<close> corresponding to a Scala case class with arguments
+ \<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
+
+ Alternatively, optional fields can have a default value. If nothing else is
+ specified, a standard ``empty value'' is used for each type, i.e.\ \<^verbatim>\<open>0\<close> for
+ the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string, array, object
+ etc.
+
+ Object types are \<^emph>\<open>permissive\<close> in the sense that only the specified field
+ names need to conform to the given types, but unspecified fields may be
+ present as well.
+
+ \<^item> The type expression \<open>t\<^sub>1 \<oplus> t\<^sub>2\<close> only works for two object types with
+ disjoint field names: it is the concatenation of the respective @{syntax
+ field_type} specifications taken together. For example: \<open>{task: string} \<oplus>
+ {ok: bool}\<close> is the equivalent to \<open>{task: string, ok: bool}\<close>.
+
+ \<^item> The type expression \<open>t\<^sub>1 | t\<^sub>2\<close> is the disjoint union of two types, either
+ one of the two cases may occur.
+
+ \<^item> Parentheses \<open>(t)\<close> merely group type expressions syntactically.
+
+
+ These types correspond to JSON values in an obvious manner, which is not
+ further described here. For example, the JSON array \<^verbatim>\<open>[1, 2, 3]\<close> conforms to
+ types \<open>[int]\<close>, \<open>[long]\<close>, \<open>[double]\<close>, \<open>[any]\<close>, \<open>any\<close>.
+
+ Note that JSON objects require field names to be quoted, but the type
+ language omits quotes for clarity. Thus the object \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close>
+ conforms to the type \<open>{a: int, b: string}\<close>, for example.
+
+ \<^medskip>
+ The absence of an argument or result is represented by the Scala type
+ \<^verbatim>\<open>Unit\<close>: it is written as empty text in the message \<open>argument\<close>
+ (\secref{sec:input-output-messages}). This is not part of the JSON language.
+
+ Server replies have name tags like \<^verbatim>\<open>OK\<close>, \<^verbatim>\<open>ERROR\<close>: these are used literally
+ together with type specifications to indicate the particular name with the
+ type of its argument, e.g.\ \<^verbatim>\<open>OK\<close>~\<open>[string]\<close> for a regular result that is a
+ list (JSON array) of strings.
+
+ \<^bigskip>
+ Here are some common type definitions, for use in particular specifications
+ of command arguments and results.
+
+ \<^item> \<^bold>\<open>type\<close>~\<open>position = {line?: int, offset?: int, end_offset?: int, file?:
+ string, id?: long}\<close> describes a source position within Isabelle text. Only
+ the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
+ Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
+ Isabelle symbols, see @{ML_type Symbol.symbol} in Isabelle/ML @{cite
+ "isabelle-implementation"}. The position \<open>id\<close> belongs to the representation
+ of command transactions in the Isabelle/PIDE protocol: it normally does not
+ occur in externalized positions.
+
+ \<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
+ the \<open>kind\<close> provides some hint about the role and importance of the message.
+ The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>,
+ \<^verbatim>\<open>error\<close>. Messages without explicit kind can be treated like \<^verbatim>\<open>writeln\<close>.
+
+ \<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
+ error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
+ \<^verbatim>\<open>FAILED\<close> replies, but also as initial command syntax errors (which are
+ omitted in the command specifications below).
+
+ \<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
+ string, session: string}\<close> reports formal progress in loading theories (e.g.\
+ when building a session image). Apart from a regular output message, it also
+ reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
+ \<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
+ e.g. theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
+
+ \<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
+ common Isabelle timing information in seconds, usually with a precision of
+ three digits after the point (whole milliseconds).
+
+ \<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
+ as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
+ \<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/UUID.html\<close>.\<close> Such
+ identifiers are created as private random numbers of the server and only
+ revealed to the client that creates a certain resource (e.g.\ task or
+ session). A client may disclose this information for use in a different
+ client connection: this allows to share sessions between multiple
+ connections.
+
+ Client commands need to provide syntactically wellformed UUIDs: this is
+ trivial to achieve by using only identifiers that have been produced by the
+ server beforehand.
+
+ \<^item> \<^bold>\<open>type\<close>~\<open>task = {task: uuid}\<close> identifies a newly created asynchronous task
+ and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
+ task identification is included in all messages produced by this task.
+
+ \<^item> \<^bold>\<open>type\<close> \<open>session_id = {session_id: uuid}\<close> identifies a newly created PIDE
+ session managed by the server. Sessions are independent of client
+ connections and may be shared by different clients, as long as the internal
+ session identifier is known.
+
+ \<^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.
+\<close>
+
+
+section \<open>Server commands and results\<close>
+
+text \<open>
+ Here follows an overview of particular Isabelle server commands with their
+ results, which are usually represented as JSON values with types according
+ to \secref{sec:json-types}. The general format of input and output messages
+ is described in \secref{sec:input-output-messages}. The relevant
+ Isabelle/Scala source files are:
+
+ \<^medskip>
+ \begin{tabular}{l}
+ \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
+ \<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close> \\
+ \<^file>\<open>$ISABELLE_HOME/src/Pure/General/json.scala\<close> \\
+ \end{tabular}
+\<close>
+
+
+subsection \<open>Command \<^verbatim>\<open>help\<close>\<close>
+
+text \<open>
+ \begin{tabular}{ll}
+ regular result: & \<^verbatim>\<open>OK\<close> \<open>[string]\<close> \\
+ \end{tabular}
+ \<^medskip>
+
+ The \<^verbatim>\<open>help\<close> command has no argument and returns the list of server command
+ names. This is occasionally useful for interactive experimentation (see also
+ @{tool client} in \secref{sec:tool-client}).
+\<close>
+
+
+subsection \<open>Command \<^verbatim>\<open>echo\<close>\<close>
+
+text \<open>
+ \begin{tabular}{ll}
+ argument: & \<open>any\<close> \\
+ regular result: & \<^verbatim>\<open>OK\<close> \<open>any\<close> \\
+ \end{tabular}
+ \<^medskip>
+
+ The \<^verbatim>\<open>echo\<close> command is the identity function: it returns its argument as
+ regular result. This is occasionally useful for testing and interactive
+ experimentation (see also @{tool client} in \secref{sec:tool-client}).
+
+ The Scala type of \<^verbatim>\<open>echo\<close> is actually more general than given above:
+ \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> work uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
+ be difficult to type on the console in its YXML syntax
+ (\secref{sec:yxml-vs-xml}).
+\<close>
+
+
+subsection \<open>Command \<^verbatim>\<open>shutdown\<close>\<close>
+
+text \<open>
+ \begin{tabular}{ll}
+ regular result: & \<^verbatim>\<open>OK\<close> \\
+ \end{tabular}
+ \<^medskip>
+
+ The \<^verbatim>\<open>shutdown\<close> command has no argument and result value. It forces a
+ shutdown of the connected server process, stopping all open sessions and
+ closing the server socket. This may disrupt pending commands on other
+ connections!
+
+ \<^medskip>
+ The command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server connection
+ and issues a \<^verbatim>\<open>shutdown\<close> command (see also \secref{sec:tool-server}).
+\<close>
+
+
+subsection \<open>Command \<^verbatim>\<open>cancel\<close>\<close>
+
+text \<open>
+ \begin{tabular}{ll}
+ argument: & \<open>task\<close> \\
+ regular result: & \<^verbatim>\<open>OK\<close> \\
+ \end{tabular}
+ \<^medskip>
+
+ The command \<^verbatim>\<open>cancel {"task":\<close>~\<open>id\<close>\<^verbatim>\<open>}\<close> attempts to cancel the specified
+ task.
+
+ Cancellation is merely a hint that the client prefers an ongoing process to
+ be stopped. The command always succeeds formally, but it may get ignored by
+ a task that is still running; it might also refer to a non-existing or
+ no-longer existing task (without producing an error).
+
+ Successful cancellation typically leads to an asynchronous failure of type
+ \<^verbatim>\<open>FAILED {\<close>\<open>task: uuid, message:\<close>~\<^verbatim>\<open>"Interrupt"}\<close>. A different message is
+ also possible, depending how the task handles the event.
+\<close>
+
+
+subsection \<open>Command \<^verbatim>\<open>session_build\<close> \label{sec:command-session-build}\<close>
+
+text \<open>
+ \begin{tabular}{lll}
+ argument: & \<open>session_build_args\<close> \\
+ immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
+ notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
+ regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_build_results\<close> \\
+ error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_build_results\<close> \\[2ex]
+ \end{tabular}
+
+ \begin{tabular}{lll}
+ \<^bold>\<open>type\<close> \<open>session_build_args =\<close> \\
+ \quad\<open>{session: string,\<close> \\
+ \quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
+ \quad~~\<open>options?: [string],\<close> \\
+ \quad~~\<open>dirs?: [string],\<close> \\
+ \quad~~\<open>include_sessions: [string],\<close> \\
+ \quad~~\<open>system_mode?: bool,\<close> \\
+ \quad~~\<open>verbose?: bool}\<close> \\[2ex]
+ \end{tabular}
+
+ \begin{tabular}{ll}
+ \<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
+ \quad\<open>{session: string,\<close> \\
+ \quad~~\<open>ok: bool,\<close> \\
+ \quad~~\<open>return_code: int,\<close> \\
+ \quad~~\<open>timeout: bool,\<close> \\
+ \quad~~\<open>timing: timing}\<close> \\[2ex]
+
+ \<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
+ \quad\<open>{ok: bool,\<close> \\
+ \quad~~\<open>return_code: int,\<close> \\
+ \quad~~\<open>sessions: [session_build_result]}\<close> \\
+ \end{tabular}
+\<close>
+
+text \<open>
+ The \<^verbatim>\<open>session_build\<close> command prepares a session image for interactive use of
+ theories. This is a limited version of command-line tool @{tool build}
+ (\secref{sec:tool-build}), with specific options to request a formal context
+ for an interactive PIDE session.
+
+ The build process is asynchronous, with notifications that inform about the
+ progress of loaded theories. Some further informative messages are output as
+ well.
+
+ Coordination of independent build processes is at the discretion of the
+ client (or end-user), just as for @{tool build} and @{tool jedit}. There is
+ no built-in coordination of conflicting builds with overlapping hierarchies
+ of session images. In the worst case, a session image produced by one task
+ may get overwritten by another task!
+\<close>
+
+
+subsubsection \<open>Arguments\<close>
+
+text \<open>
+ The \<open>session\<close> field specifies the target session name. The build process
+ will produce all required ancestor images according to the overall session
+ graph.
+
+ \<^medskip>
+ The environment of Isabelle system options is determined from \<open>preferences\<close>
+ that are augmented by \<open>options\<close>, which is a list individual updates of the
+ form the \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> (the latter abbreviates
+ \<open>name\<close>\<^verbatim>\<open>=true\<close>); see also command-line option \<^verbatim>\<open>-o\<close> for @{tool build}. The
+ preferences are loaded from the file
+ \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> by default, but the client may
+ provide alternative contents for it (as text, not a file-name). This could
+ be relevant in situations where client and server run in different
+ operating-system contexts.
+
+ \<^medskip>
+ The \<open>dirs\<close> field specifies additional directories for session ROOT and ROOTS
+ files (\secref{sec:session-root}). This augments the name space of available
+ sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
+
+ \<^medskip>
+ The \<open>include_sessions\<close> field specifies sessions whose theories should be
+ included in the overall name space of session-qualified theory names. This
+ corresponds to a \<^bold>\<open>sessions\<close> specification in ROOT files
+ (\secref{sec:session-root}). It enables the \<^verbatim>\<open>use_theories\<close> command
+ (\secref{sec:command-use-theories}) to refer to sources from other sessions
+ in a robust manner, instead of relying on directory locations.
+
+ \<^medskip>
+ The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
+ log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
+ @{setting ISABELLE_OUTPUT} (which is normally in @{setting
+ ISABELLE_HOME_USER}). See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
+
+ \<^medskip>
+ The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
+ similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
+\<close>
+
+
+subsubsection \<open>Intermediate output\<close>
+
+text \<open>
+ The asynchronous notifications of command \<^verbatim>\<open>session_build\<close> mainly serve as
+ progress indicator: the output resembles that of the session build window of
+ Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
+
+ For the client it is usually sufficient to print the messages in plain text,
+ but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
+ \<open>session\<close> names directly.
+\<close>
+
+
+subsubsection \<open>Results\<close>
+
+text \<open>
+ The overall \<open>session_build_results\<close> contain both a summary and an entry
+ \<open>session_build_result\<close> for each session in the build hierarchy. The result
+ is always provided, independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or
+ failure (\<^verbatim>\<open>FAILED\<close> task).
+
+ The \<open>ok\<close> field tells abstractly, whether all required session builds came
+ out as \<open>ok\<close>, i.e.\ with zero \<open>return_code\<close>. A non-zero \<open>return_code\<close>
+ indicates an error according to usual POSIX conventions for process exit.
+
+ The individual \<open>session_build_result\<close> entries provide extra fields:
+
+ \<^item> \<open>timeout\<close> tells if the build process was aborted after running too long,
+
+ \<^item> \<open>timing\<close> gives the overall process timing in the usual Isabelle format
+ with elapsed, CPU, GC time.
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Build of a session image from the Isabelle distribution:
+ @{verbatim [display] \<open>session_build {"session": "HOL-Word"}\<close>}
+
+ Build a session image from the Archive of Formal Proofs:
+ @{verbatim [display] \<open>session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
+\<close>
+
+
+subsection \<open>Command \<^verbatim>\<open>session_start\<close> \label{sec:command-session-start}\<close>
+
+text \<open>
+ \begin{tabular}{lll}
+ argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
+ immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
+ notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
+ regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id \<oplus> {tmp_dir: string}\<close> \\
+ error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
+ \end{tabular}
+
+ \<^medskip>
+ The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
+ underlying Isabelle/ML process, based on a session image that it produces on
+ demand using \<^verbatim>\<open>session_build\<close>. Thus it accepts all \<open>session_build_args\<close> and
+ produces similar notifications, but the detailed \<open>session_build_results\<close> are
+ omitted.
+
+ The session build and startup process is asynchronous: when the task is
+ finished, the session remains active for commands, until a \<^verbatim>\<open>session_stop\<close>
+ or \<^verbatim>\<open>shutdown\<close> command is sent to the server.
+
+ Sessions are independent of client connections: it is possible to start a
+ session and later apply \<^verbatim>\<open>use_theories\<close> on different connections, as long as
+ the internal session identifier is known: shared theory imports will be used
+ only once (and persist until purged explicitly).
+\<close>
+
+
+subsubsection \<open>Arguments\<close>
+
+text \<open>
+ Most arguments are shared with \<^verbatim>\<open>session_build\<close>
+ (\secref{sec:command-session-build}).
+
+ \<^medskip>
+ The \<open>print_mode\<close> field adds identifiers of print modes to be made active for
+ this session. For example, \<^verbatim>\<open>"print_mode": ["ASCII"]\<close> prefers ASCII
+ replacement syntax over mathematical Isabelle symbols. See also option \<^verbatim>\<open>-m\<close>
+ in @{tool process} (\secref{sec:tool-process}).
+\<close>
+
+
+subsubsection \<open>Results\<close>
+
+text \<open>
+ The \<open>session_id\<close> provides the internal identification of the session object
+ within the sever process. It can remain active as long as the server is
+ running, independently of the current client connection.
+
+ \<^medskip>
+ The \<open>tmp_dir\<close> fields reveals a temporary directory that is specifically
+ created for this session and deleted after it has been stopped. This may
+ serve as auxiliary file-space for the \<^verbatim>\<open>use_theories\<close> command, but
+ concurrent use requires some care in naming temporary files, e.g.\ by
+ using sub-directories with globally unique names.
+\<close>
+
+
+subsection \<open>Examples\<close>
+
+text \<open>
+ Start a default Isabelle/HOL session:
+ @{verbatim [display] \<open>session_start {"session": "HOL"}\<close>}
+
+ Start a session from the Archive of Formal Proofs:
+ @{verbatim [display] \<open>session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
+\<close>
+
+
+subsection \<open>Command \<^verbatim>\<open>session_stop\<close>\<close>
+
+text \<open>
+ \begin{tabular}{ll}
+ argument: & \<open>session_id\<close> \\
+ immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
+ regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
+ error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
+ \end{tabular}
+
+ \begin{tabular}{l}
+ \<^bold>\<open>type\<close> \<open>session_stop_result = {ok: bool, return_code: int}\<close>
+ \end{tabular}
+
+ \<^medskip>
+ The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified PIDE
+ session. This asynchronous tasks usually finishes quickly. Failure only
+ happens in unusual situations, according to the return code of the
+ underlying Isabelle/ML process.
+\<close>
+
+
+subsubsection \<open>Arguments\<close>
+
+text \<open>
+ The \<open>session_id\<close> provides the UUID originally created by the server for this
+ session.
+\<close>
+
+
+subsubsection \<open>Results\<close>
+
+text \<open>
+ The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process has
+ terminated properly.
+
+ The \<open>return_code\<close> field expresses this information according to usual POSIX
+ conventions for process exit.
+\<close>
+
+
+subsection \<open>Command \<^verbatim>\<open>use_theories\<close> \label{sec:command-use-theories}\<close>
+
+text \<open>
+ \begin{tabular}{ll}
+ argument: & \<open>use_theories_arguments\<close> \\
+ regular result: & \<^verbatim>\<open>OK\<close> \<open>use_theories_results\<close> \\
+ \end{tabular}
+
+ \begin{tabular}{ll}
+ \<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
+ \end{tabular}
+
+ \begin{tabular}{ll}
+ \<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
+ \quad\<open>{session_id: uuid,\<close> \\
+ \quad~~\<open>theories: [theory_name],\<close> \\
+ \quad~~\<open>qualifier?: string,\<close> \\
+ \quad~~\<open>master_dir?: string,\<close> \\
+ \quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
+ \quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
+ \end{tabular}
+
+ \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>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]
+ \end{tabular}
+
+ \<^medskip>
+ The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
+ current version of theory files to it, while dependencies are resolved
+ implicitly. The command succeeds eventually, when all theories have been
+ \<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
+ (\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>.
+\<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 as in theory \<^theory_text>\<open>imports\<close> or in
+ ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
+ specifications may be given, which is occasionally useful for precise error
+ locations.
+
+ \<^medskip>
+ The \<open>qualifier\<close> field provides an alternative session qualifier for theories
+ that are not formally recognized as a member of a particular session. The
+ default is \<^verbatim>\<open>Draft\<close> as in Isabelle/jEdit. There is rarely a need to change
+ that, as theory nodes are already uniquely identified by their physical
+ file-system location. This already allows reuse of theory base names with
+ the same session qualifier --- as long as these theories are not used
+ together (e.g.\ in \<^theory_text>\<open>imports\<close>).
+
+ \<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
+ the imported theory. Normally this is determined implicitly from the parent
+ directory of the theory file.
+
+ \<^medskip>
+ The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
+ default is suitable for classic console output. Formatting happens at the
+ end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.
+
+ \<^medskip>
+ The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> renders message output for direct
+ output on a Unicode capable channel, ideally with the Isabelle fonts as in
+ Isabelle/jEdit. The default is to keep the symbolic representation of
+ Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead of its rendering as \<open>\<forall>\<close>. This means the
+ client needs to perform its own rendering before presenting it to the
+ end-user.
+\<close>
+
+
+subsubsection \<open>Results\<close>
+
+text \<open>
+ The \<open>ok\<close> field indicates overall success of processing the specified
+ theories with all their dependencies.
+
+ When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively
+ (including imported theories). The messages contain position information for
+ the original theory nodes.
+
+ \<^medskip>
+ 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
+ file-system location;
+
+ \<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close>;
+
+ \<^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"};
+
+ \<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
+ (\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
+\<close>
+
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+ Process some example theory from the Isabelle distribution, within the
+ context of an already started session for Isabelle/HOL (see also
+ \secref{sec:command-session-start}):
+ @{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Isar_Examples/Drinker"]}\<close>}
+
+ \<^medskip>
+ Process some example theories in the context of their (single) parent
+ session:
+
+ @{verbatim [display] \<open>session_start {"session": "HOL-Library"}
+use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
+session_stop {"session_id": ...}\<close>}
+
+ \<^medskip>
+ Process some example theories that import other theories via
+ session-qualified theory names:
+
+ @{verbatim [display] \<open>session_start {"session": "HOL", "include_sessions": ["HOL-Unix"]}
+use_theories {"session_id": ..., "theories": ["HOL-Unix.Unix"]}
+session_stop {"session_id": ...}\<close>}
\<close>
end
--- a/src/Pure/PIDE/protocol.scala Thu Mar 22 13:53:15 2018 +0100
+++ b/src/Pure/PIDE/protocol.scala Thu Mar 22 17:06:15 2018 +0100
@@ -144,13 +144,13 @@
sealed case class Node_Status(
unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
{
+ def ok: Boolean = failed == 0
def total: Int = unprocessed + running + warned + failed + finished
- def ok: Boolean = failed == 0
def json: JSON.Object.T =
- JSON.Object("unprocessed" -> unprocessed, "running" -> running, "warned" -> warned,
- "failed" -> failed, "finished" -> finished, "consolidated" -> consolidated,
- "total" -> total, "ok" -> ok)
+ JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
+ "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
+ "consolidated" -> consolidated)
}
def node_status(
@@ -239,6 +239,13 @@
case _ => false
}
+ def is_writeln(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WRITELN, _), _) => true
+ case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _), _) => true
+ case _ => false
+ }
+
def is_warning(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.WARNING, _), _) => true
@@ -263,6 +270,9 @@
def is_inlined(msg: XML.Tree): Boolean =
!(is_result(msg) || is_tracing(msg) || is_state(msg))
+ def is_exported(msg: XML.Tree): Boolean =
+ is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
+
/* breakpoints */
--- a/src/Pure/System/isabelle_system.scala Thu Mar 22 13:53:15 2018 +0100
+++ b/src/Pure/System/isabelle_system.scala Thu Mar 22 17:06:15 2018 +0100
@@ -173,10 +173,10 @@
File.platform_file(path)
}
- def tmp_file(name: String, ext: String = ""): JFile =
+ def tmp_file(name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
val suffix = if (ext == "") "" else "." + ext
- val file = Files.createTempFile(isabelle_tmp_prefix().toPath, name, suffix).toFile
+ val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile
file.deleteOnExit
file
}
@@ -217,9 +217,9 @@
}
}
- def tmp_dir(name: String): JFile =
+ def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile =
{
- val dir = Files.createTempDirectory(isabelle_tmp_prefix().toPath, name).toFile
+ val dir = Files.createTempDirectory(base_dir.toPath, name).toFile
dir.deleteOnExit
dir
}
--- a/src/Pure/Thy/sessions.scala Thu Mar 22 13:53:15 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Thu Mar 22 17:06:15 2018 +0100
@@ -373,6 +373,7 @@
session: String,
progress: Progress = No_Progress,
dirs: List[Path] = Nil,
+ include_sessions: List[String] = Nil,
ancestor_session: Option[String] = None,
all_known: Boolean = false,
focus_session: Boolean = false,
@@ -435,15 +436,17 @@
if (infos1.isEmpty) full_sessions
else load_structure(options, dirs = dirs, infos = infos1)
- val select_sessions1 =
- if (focus_session) full_sessions1.imports_descendants(List(session1))
- else List(session1)
val selected_sessions1 =
+ {
+ val sel_sessions1 = session1 :: include_sessions
+ val select_sessions1 =
+ if (focus_session) full_sessions1.imports_descendants(sel_sessions1) else sel_sessions1
full_sessions1.selection(Selection(sessions = select_sessions1))
+ }
val sessions1 = if (all_known) full_sessions1 else selected_sessions1
val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
- val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
+ val base1 = deps1(session1).copy(known = deps1.all_known)
Base_Info(options, dirs, session1, sessions1, deps1.errors, base1, infos1)
}
--- a/src/Pure/Thy/thy_resources.scala Thu Mar 22 13:53:15 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala Thu Mar 22 17:06:15 2018 +0100
@@ -7,6 +7,9 @@
package isabelle
+import java.io.{File => JFile}
+
+
object Thy_Resources
{
/* PIDE session */
@@ -65,7 +68,6 @@
Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
pos = command.span.keyword_pos(start).position(command.span.name)
(_, tree) <- state.command_results(version, command).iterator
- if Protocol.is_inlined(tree)
} yield (tree, pos)).toList
}
}
@@ -76,6 +78,14 @@
{
session =>
+ val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session")
+
+ override def stop(): Process_Result =
+ {
+ try { super.stop() }
+ finally { Isabelle_System.rm_tree(tmp_dir) }
+ }
+
def use_theories(
theories: List[(String, Position.T)],
qualifier: String = Sessions.DRAFT,
--- a/src/Pure/Tools/server.scala Thu Mar 22 13:53:15 2018 +0100
+++ b/src/Pure/Tools/server.scala Thu Mar 22 17:06:15 2018 +0100
@@ -69,7 +69,8 @@
"help" -> { case (_, ()) => table.keySet.toList.sorted },
"echo" -> { case (_, t) => t },
"shutdown" -> { case (context, ()) => context.server.shutdown() },
- "cancel" -> { case (context, JSON.Value.UUID(id)) => context.cancel_task(id) },
+ "cancel" ->
+ { case (context, Server_Commands.Cancel(args)) => context.cancel_task(args.task) },
"session_build" ->
{ case (context, Server_Commands.Session_Build(args)) =>
context.make_task(task =>
@@ -115,8 +116,8 @@
def json_error(exn: Throwable): JSON.Object.T =
exn match {
+ case e: Error => Reply.error_message(e.message) ++ e.json
case ERROR(msg) => Reply.error_message(msg)
- case e: Error => Reply.error_message(e.message) ++ e.json
case _ if Exn.is_interrupt(exn) => Reply.error_message(Exn.message(exn))
case _ => JSON.Object.empty
}
@@ -130,7 +131,7 @@
else JSON.Object(Markup.KIND -> kind, "message" -> msg)
def error_message(msg: String): JSON.Object.T =
- message(msg, kind = Markup.ERROR_MESSAGE)
+ message(msg, kind = Markup.ERROR)
def unapply(msg: String): Option[(Reply.Value, Any)] =
{
@@ -225,7 +226,7 @@
def writeln(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WRITELN, msg, more:_*)
def warning(msg: String, more: JSON.Object.Entry*): Unit = message(Markup.WARNING, msg, more:_*)
def error_message(msg: String, more: JSON.Object.Entry*): Unit =
- message(Markup.ERROR_MESSAGE, msg, more:_*)
+ message(Markup.ERROR, msg, more:_*)
def progress(more: JSON.Object.Entry*): Connection_Progress =
new Connection_Progress(context, more:_*)
--- a/src/Pure/Tools/server_commands.scala Thu Mar 22 13:53:15 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Thu Mar 22 17:06:15 2018 +0100
@@ -23,6 +23,16 @@
case _ => None
}
+ object Cancel
+ {
+ sealed case class Args(task: UUID)
+
+ def unapply(json: JSON.T): Option[Args] =
+ for { task <- JSON.uuid(json, "task") }
+ yield Args(task)
+ }
+
+
object Session_Build
{
sealed case class Args(
@@ -30,10 +40,7 @@
preferences: String = default_preferences,
options: List[String] = Nil,
dirs: List[String] = Nil,
- ancestor_session: String = "",
- all_known: Boolean = false,
- focus_session: Boolean = false,
- required_session: Boolean = false,
+ include_sessions: List[String] = Nil,
system_mode: Boolean = false,
verbose: Boolean = false)
@@ -43,17 +50,13 @@
preferences <- JSON.string_default(json, "preferences", default_preferences)
options <- JSON.list_default(json, "options", JSON.Value.String.unapply _)
dirs <- JSON.list_default(json, "dirs", JSON.Value.String.unapply _)
- ancestor_session <- JSON.string_default(json, "ancestor_session")
- all_known <- JSON.bool_default(json, "all_known")
- focus_session <- JSON.bool_default(json, "focus_session")
- required_session <- JSON.bool_default(json, "required_session")
+ include_sessions <- JSON.list_default(json, "include_sessions", JSON.Value.String.unapply _)
system_mode <- JSON.bool_default(json, "system_mode")
verbose <- JSON.bool_default(json, "verbose")
}
yield {
Args(session, preferences = preferences, options = options, dirs = dirs,
- ancestor_session = ancestor_session, all_known = all_known, focus_session = focus_session,
- required_session = required_session, system_mode = system_mode, verbose = verbose)
+ include_sessions = include_sessions, system_mode = system_mode, verbose = verbose)
}
def command(args: Args, progress: Progress = No_Progress)
@@ -63,14 +66,8 @@
val dirs = args.dirs.map(Path.explode(_))
val base_info =
- Sessions.base_info(options,
- args.session,
- progress = progress,
- dirs = dirs,
- ancestor_session = proper_string(args.ancestor_session),
- all_known = args.all_known,
- focus_session = args.focus_session,
- required_session = args.required_session)
+ Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
+ include_sessions = args.include_sessions)
val base = base_info.check_base
val results =
@@ -89,14 +86,19 @@
val results_json =
JSON.Object(
+ "ok" -> results.ok,
"return_code" -> results.rc,
"sessions" ->
results.sessions.toList.sortBy(sessions_order).map(session =>
- JSON.Object(
- "session" -> session,
- "return_code" -> results(session).rc,
- "timeout" -> results(session).timeout,
- "timing" -> results(session).timing.json)))
+ {
+ val result = results(session)
+ JSON.Object(
+ "session" -> session,
+ "ok" -> result.ok,
+ "return_code" -> result.rc,
+ "timeout" -> result.timeout,
+ "timing" -> result.timing.json)
+ }))
if (results.ok) (results_json, results, base_info)
else throw new Server.Error("Session build failed: return code " + results.rc, results_json)
@@ -119,7 +121,9 @@
def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
: (JSON.Object.T, (UUID, Thy_Resources.Session)) =
{
- val base_info = Session_Build.command(args.build, progress = progress)._3
+ val base_info =
+ try { Session_Build.command(args.build, progress = progress)._3 }
+ catch { case exn: Server.Error => error(exn.message) }
val session =
Thy_Resources.start_session(
@@ -132,7 +136,11 @@
log = log)
val id = UUID()
- val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id.toString)
+
+ val res =
+ JSON.Object(
+ "session_id" -> id.toString,
+ "tmp_dir" -> File.path(session.tmp_dir).implode)
(res, id -> session)
}
@@ -146,7 +154,7 @@
def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
{
val result = session.stop()
- val result_json = JSON.Object("return_code" -> result.rc)
+ val result_json = JSON.Object("ok" -> result.ok, "return_code" -> result.rc)
if (result.ok) (result_json, result)
else throw new Server.Error("Session shutdown failed: return code " + result.rc, result_json)
@@ -196,7 +204,9 @@
case XML.Text(msg) => Server.Reply.message(output_text(msg)) + position
case elem: XML.Elem =>
val msg = XML.content(Pretty.formatted(List(elem), margin = args.pretty_margin))
- val kind = Markup.messages.collectFirst({ case (a, b) if b == elem.name => a })
+ val kind =
+ Markup.messages.collectFirst({ case (a, b) if b == elem.name =>
+ if (Protocol.is_legacy(elem)) Markup.WARNING else a })
Server.Reply.message(output_text(msg), kind = kind getOrElse "") + position
}
}
@@ -208,6 +218,7 @@
(for {
(name, status) <- result.nodes if !status.ok
(tree, pos) <- result.messages(name) if Protocol.is_error(tree)
+ if Protocol.is_exported(tree)
} yield output_message(tree, pos)),
"nodes" ->
(for ((name, status) <- result.nodes) yield