# HG changeset patch # User wenzelm # Date 1694465974 -7200 # Node ID 5930c89d3bf29301ec13143fb5c5df099fee71e3 # Parent 0d2ea608d2234bb3a2b061bdf9faaa78682c54e1# Parent 4da1e18a963302532de351d01a92ced4f98c47d7 merged diff -r 4da1e18a9633 -r 5930c89d3bf2 .hgtags --- a/.hgtags Sat Sep 09 19:26:08 2023 +0100 +++ b/.hgtags Mon Sep 11 22:59:34 2023 +0200 @@ -46,3 +46,4 @@ f5fb5bb2533fdf96b136a2aa508e30d4608fd888 Isabelle2023-RC3 12aac1489f3bfcddfd21d3598dc2ed7512999682 Isabelle2023-RC4 ffa417b5c9137255818c24137df05f49a3af1b8d Isabelle2023-RC5 +b5f3d1051b131a80b1e4560cc05e5a3d223bc64f Isabelle2023 diff -r 4da1e18a9633 -r 5930c89d3bf2 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sat Sep 09 19:26:08 2023 +0100 +++ b/src/Doc/JEdit/JEdit.thy Mon Sep 11 22:59:34 2023 +0200 @@ -1846,7 +1846,7 @@ The ultimate purpose of Isabelle is to produce nicely rendered documents with the Isabelle document preparation system, which is based on {\LaTeX}; see also \<^cite>\"isabelle-system" and "isabelle-isar-ref"\. Isabelle/jEdit - provides some additional support for document editing. + provides some additional support to edit, build, and view documents. \ @@ -1961,6 +1961,101 @@ \ +section \Build and view documents interactively\ + +text \ + The \<^emph>\Document\ panel (\figref{fig:document}) allows to manage the build + process of formal documents. Theory sources are taken from the running PIDE + editor session, as specified in the \<^emph>\session selector\ and the \<^emph>\Input\ + tab. {\LaTeX} tools are run in various stages, as shown in the \<^emph>\Output\ + tab. The resulting PDF document may be viewed by an external browser. + + \begin{figure}[!htb] + \begin{center} + \includegraphics[scale=0.333]{document-panel} + \end{center} + \caption{Document panel with separate instances for \<^emph>\Input\ and \<^emph>\Output\} + \label{fig:document} + \end{figure} + + The traditional batch-build works on the command-line, e.g.\ via + \<^verbatim>\isabelle build -o document\~\SESSION\, see also \<^cite>\\\S3\ in + "isabelle-system"\. The corresponding session \<^verbatim>\ROOT\ entry determines + \isakeyword{theories} and \isakeyword{document\_files} for the overall + {\LaTeX} job. The latter is run as a monolithic process, using all theories + and taking contents from the file-system. + + In contrast, an interactive build within Isabelle/jEdit allows to select a + subset of theory sources, and contents are taken from the PIDE document + model. Beware that \isakeyword{document\_files} and the overall session + specification are still taken from the \<^verbatim>\ROOT\ entry: that information is + only processed on startup of Isabelle/jEdit, so changes to \<^verbatim>\ROOT\ require a + restart. + + \<^medskip> The GUI elements of the \<^emph>\Document\ panel (\figref{fig:document}), and its + sub-panels for \<^emph>\Input\ and \<^emph>\Output\ are described below (from left to + right). The screenshot has two instances of the panel to illustrate both + \<^emph>\Input\ and \<^emph>\Output\ simultaneously. + + \<^item> The \<^emph>\session selector\ tells, which session should be the basis of the + document build job. This determines, which theories may be selected in the + \<^emph>\Input\ tab (dynamically) and which \isakeyword{document\_files} should + be used (statically). + + \<^item> The \<^emph>\progress indicator\ provides some visual feedback on the document + build process. The ``spinning wheel'' is either active while processing + selected document theories in the Prover IDE, or while {\LaTeX} tools are + running. + + \<^item> The \<^emph>\Auto\ checkbox may be selected to say that the {\LaTeX} job should + be started automatically (after a timeout). This happens whenever the + selected theories have been fully processed in the Prover IDE (see also + the \<^emph>\Build\ button). If successful, the resulting PDF will be shown by an + external browser (see also the \<^emph>\View\ button). + + \<^item> The \<^emph>\Build\ button invokes the {\LaTeX} job manually, when \<^emph>\Input\ + theories have been fully processed. The \<^emph>\Output\ tab follows the stages + of the build job, with information about sources, log output, error + messages. + + \<^item> The \<^emph>\View\ button invokes an external browser application on the + resulting PDF file: its location is always the same, given within the + \<^verbatim>\$ISABELLE_HOME_USER\ directory. Multiple invocations should normally + refresh the viewer application, with the same document position as last + time. Beware that window focus handling depends on the application (and + the desktop environment): there may be conflicts with the editor + window focus. + + \<^item> The \<^emph>\Input\ sub-panel is similar to the regular \<^emph>\Theories\ panel + (\secref{sec:theories}). The selection is limited to the theories of the + underlying document session (see also the \<^emph>\session selector\). Each + theory may be selected or de-selected separately, using the checkbox next + to its name. Alternatively, there are buttons \<^emph>\All\ and \<^emph>\None\ to change + this state for the whole session. The document selection state is also + displayed in the regular \<^emph>\Theories\ panel as a ``document'' icon attached + to the theory name: that is only shown when at least one \<^emph>\Document\ panel + is active. The \<^emph>\Purge\ button is a clone of the same button on a regular + \<^emph>\Theories\ panel: it allows to remove unused theories from the PIDE + document model (that affects everything, not just document theories). + + Non-selected theories are turned into an (almost) empty {\LaTeX} source + file: formal \\<^cite>\ antiquotations \<^cite>\"isabelle-isar-ref"\ are + included, everything else is left blank. Thus the {\LaTeX} and Bib{\TeX} + document setup should normally work, independently of the selected subset + of theories. References to sections or pages might be missing, though. + + \<^item> The \<^emph>\Output\ sub-panel provides a structured view of the running build + process. Its progress output consists of a two-level hierarchy of + messages. The outer level displays program names with timing information. + Hovering over some name reveals the inner level with program log + information or error messages. + + The initial stage of ``\<^verbatim>\Creating directory\'' shows a directory listing + of the {\LaTeX} job that has been generated from all document sources. + This may help to explore structural failures of the {\LaTeX} job. +\ + + chapter \ML debugging within the Prover IDE\ text \ diff -r 4da1e18a9633 -r 5930c89d3bf2 src/Doc/JEdit/document/document-panel.png Binary file src/Doc/JEdit/document/document-panel.png has changed diff -r 4da1e18a9633 -r 5930c89d3bf2 src/Doc/ROOT --- a/src/Doc/ROOT Sat Sep 09 19:26:08 2023 +0100 +++ b/src/Doc/ROOT Mon Sep 11 22:59:34 2023 +0200 @@ -217,6 +217,7 @@ "auto-tools.png" "bibtex-mode.png" "cite-completion.png" + "document-panel.png" "isabelle-jedit.png" "markdown-document.png" "ml-debugger.png"