equal
deleted
inserted
replaced
762 text \<open> |
762 text \<open> |
763 \begin{tabular}{lll} |
763 \begin{tabular}{lll} |
764 argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\ |
764 argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\ |
765 immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\ |
765 immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\ |
766 notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\ |
766 notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\ |
767 regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id\<close> \\ |
767 regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_id \<oplus> {tmp_dir: string}\<close> \\ |
768 error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex] |
768 error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex] |
769 \end{tabular} |
769 \end{tabular} |
770 |
770 |
771 \<^medskip> |
771 \<^medskip> |
772 The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with |
772 The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with |
804 |
804 |
805 text \<open> |
805 text \<open> |
806 The \<open>session_id\<close> provides the internal identification of the session object |
806 The \<open>session_id\<close> provides the internal identification of the session object |
807 within the sever process. It can remain active as long as the server is |
807 within the sever process. It can remain active as long as the server is |
808 running, independently of the current client connection. |
808 running, independently of the current client connection. |
|
809 |
|
810 \<^medskip> |
|
811 The \<open>tmp_dir\<close> fields reveals a temporary directory that is specifically |
|
812 created for this session and deleted after it has been stopped. This may |
|
813 serve as auxiliary file-space for the \<^verbatim>\<open>use_theories\<close> command, but |
|
814 concurrent use requires some care in naming temporary files, e.g.\ by |
|
815 using sub-directories with globally unique names. |
809 \<close> |
816 \<close> |
810 |
817 |
811 |
818 |
812 subsection \<open>Examples\<close> |
819 subsection \<open>Examples\<close> |
813 |
820 |