merged

--- 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

--- 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>\<open>"isabelle-system" and "isabelle-isar-ref"\<close>. Isabelle/jEdit
-  provides some additional support for document editing.
+  provides some additional support to edit, build, and view documents.
 \<close>
 
 
@@ -1961,6 +1961,101 @@
 \<close>
 
 
+section \<open>Build and view documents interactively\<close>
+
+text \<open>
+  The \<^emph>\<open>Document\<close> 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>\<open>session selector\<close> and the \<^emph>\<open>Input\<close>
+  tab. {\LaTeX} tools are run in various stages, as shown in the \<^emph>\<open>Output\<close>
+  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>\<open>Input\<close> and \<^emph>\<open>Output\<close>}
+  \label{fig:document}
+  \end{figure}
+
+  The traditional batch-build works on the command-line, e.g.\ via
+  \<^verbatim>\<open>isabelle build -o document\<close>~\<open>SESSION\<close>, see also \<^cite>\<open>\<open>\S3\<close> in
+  "isabelle-system"\<close>. The corresponding session \<^verbatim>\<open>ROOT\<close> 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>\<open>ROOT\<close> entry: that information is
+  only processed on startup of Isabelle/jEdit, so changes to \<^verbatim>\<open>ROOT\<close> require a
+  restart.
+
+  \<^medskip> The GUI elements of the \<^emph>\<open>Document\<close> panel (\figref{fig:document}), and its
+  sub-panels for \<^emph>\<open>Input\<close> and \<^emph>\<open>Output\<close> are described below (from left to
+  right). The screenshot has two instances of the panel to illustrate both
+  \<^emph>\<open>Input\<close> and \<^emph>\<open>Output\<close> simultaneously.
+
+    \<^item> The \<^emph>\<open>session selector\<close> tells, which session should be the basis of the
+    document build job. This determines, which theories may be selected in the
+    \<^emph>\<open>Input\<close> tab (dynamically) and which \isakeyword{document\_files} should
+    be used (statically).
+
+    \<^item> The \<^emph>\<open>progress indicator\<close> 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>\<open>Auto\<close> 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>\<open>Build\<close> button). If successful, the resulting PDF will be shown by an
+    external browser (see also the \<^emph>\<open>View\<close> button).
+
+    \<^item> The \<^emph>\<open>Build\<close> button invokes the {\LaTeX} job manually, when \<^emph>\<open>Input\<close>
+    theories have been fully processed. The \<^emph>\<open>Output\<close> tab follows the stages
+    of the build job, with information about sources, log output, error
+    messages.
+
+    \<^item> The \<^emph>\<open>View\<close> button invokes an external browser application on the
+    resulting PDF file: its location is always the same, given within the
+    \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> 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>\<open>Input\<close> sub-panel is similar to the regular \<^emph>\<open>Theories\<close> panel
+    (\secref{sec:theories}). The selection is limited to the theories of the
+    underlying document session (see also the \<^emph>\<open>session selector\<close>). Each
+    theory may be selected or de-selected separately, using the checkbox next
+    to its name. Alternatively, there are buttons \<^emph>\<open>All\<close> and \<^emph>\<open>None\<close> to change
+    this state for the whole session. The document selection state is also
+    displayed in the regular \<^emph>\<open>Theories\<close> panel as a ``document'' icon attached
+    to the theory name: that is only shown when at least one \<^emph>\<open>Document\<close> panel
+    is active. The \<^emph>\<open>Purge\<close> button is a clone of the same button on a regular
+    \<^emph>\<open>Theories\<close> 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 \<open>\<^cite>\<close> antiquotations \<^cite>\<open>"isabelle-isar-ref"\<close> 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>\<open>Output\<close> 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>\<open>Creating directory\<close>'' 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.
+\<close>
+
+
 chapter \<open>ML debugging within the Prover IDE\<close>
 
 text \<open>

Binary file src/Doc/JEdit/document/document-panel.png has changed

--- 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"