# HG changeset patch
# User wenzelm
# Date 1738508649 -3600
# Node ID 1be62b17bed921c0f5ab8769dfae18c536b79026
# Parent  0f22f7b370b243ef40d6c93206e76d964bbdd975
tuned documentation;

diff -r 0f22f7b370b2 -r 1be62b17bed9 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Sun Feb 02 14:16:26 2025 +0100
+++ b/src/Doc/System/Presentation.thy	Sun Feb 02 16:04:09 2025 +0100
@@ -208,14 +208,13 @@
 text \<open>
   The session information of a regular @{tool_ref build} can also be used to
   generate a search index for full-text search over formal theory content. To
-  that end, the \<^verbatim>\<open>Find_Facts\<close> module integrates Apache Solr\<^footnote>\<open>\<^url>\<open>https://solr.apache.org/\<close>\<close>,
+  that end, the \<^verbatim>\<open>Find_Facts\<close> module integrates Apache Solr\<^footnote>\<open>\<^url>\<open>https://solr.apache.org\<close>\<close>,
   a full-text search engine, that can run embedded in a JVM process. Solr is
   bundled as a separate Isabelle component, and its run-time dependencies 
   (as specified in  @{setting SOLR_JARS}) need to be added separately to the
   classpath of a regular Isabelle/Scala process.
 
   \<^medskip>
-  
   A search index can be created using the @{tool_def find_facts_index} tool,
   which has options similar to the regular @{tool_ref build}. User data such
   as search indexes is stored in @{setting FIND_FACTS_HOME_USER}. The name of
@@ -242,19 +241,19 @@
 \<close>}
 
   This Isabelle/Scala HTTP server provides the both the front-end
-  (implemented in the Elm\<^footnote>\<open>\<^url>\<open>https://elm-lang.org/\<close>\<close> language) and REST
+  (implemented in the Elm\<^footnote>\<open>\<^url>\<open>https://elm-lang.org\<close>\<close> language) and REST
   endpoints for search queries with JSON data.
 
-  Options \<^verbatim>\<open>-o\<close>, \<open>-v\<close> have the same meaning as usual.
+  Options \<^verbatim>\<open>-o\<close> and \<^verbatim>\<open>-v\<close> have the same meaning as in @{tool build}.
 
   Option \<^verbatim>\<open>-d\<close> re-compiles the front-end in \<^path>\<open>$FIND_FACTS_HOME_USER/web\<close>
   on page reload (when sources are changed).
 
-  Option \<^verbatim>\<open>-p\<close> specifies an explicit TCP port for the server socket 
-  (assigned by the operating system per default). For public-facing servers,
-  a common scheme is \<^verbatim>\<open>-p 8080\<close> that is access-restricted via firewall rules,
-  with a reverse proxy in system space (that also handles SSL) on ports 80 and
-  443. 
+  Option \<^verbatim>\<open>-p\<close> specifies an explicit TCP port for the server socket (assigned
+  by the operating system per default). For public-facing servers, a common
+  scheme is \<^verbatim>\<open>-p 8080\<close> that is access-restricted via firewall rules, with a
+  reverse proxy\<^footnote>\<open>E.g. via Caddy \<^url>\<open>https://caddyserver.com/docs\<close>\<close> in system
+  space (that also handles SSL) on ports 80 and 443.
 \<close>
 
 end
diff -r 0f22f7b370b2 -r 1be62b17bed9 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sun Feb 02 14:16:26 2025 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Feb 02 16:04:09 2025 +0100
@@ -203,7 +203,7 @@
   although it uses relatively complex quasi-hierarchic naming conventions like
   \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
   names that are relatively long and descriptive, as in the Archive of Formal
-  Proofs (\<^url>\<open>https://isa-afp.org\<close>), for example.
+  Proofs (AFP, \<^url>\<open>https://isa-afp.org\<close>), for example.
 \<close>
 
 
@@ -1104,6 +1104,7 @@
   service. The system option @{system_option build_manager_ci_jobs} controls
   which jobs are executed by the \<^verbatim>\<open>Build_Manager\<close>.
 
+  \<^medskip>
   The command-line usage to start the server is:
   @{verbatim [display]
 \<open>Usage: isabelle build_manager [OPTIONS]
@@ -1119,9 +1120,11 @@
   Run Isabelle build manager.
 \<close>}
 
-  \<^medskip> Options \<^verbatim>\<open>-o\<close> and \<^verbatim>\<open>-p\<close> are the same as in other server applications.
+  \<^medskip> Option \<^verbatim>\<open>-o\<close> has the same meaning as for @{tool build}.
 
-  \<^medskip> Option \<^verbatim>\<open>-A\<close> refers to the AFP (must be a Mercurial clone)
+  \<^medskip> Option \<^verbatim>\<open>-p\<close> has the same meaning as for @{tool server}.
+
+  \<^medskip> Option \<^verbatim>\<open>-A\<close> refers to the AFP (must be a Mercurial clone).
 
   \<^medskip> Option \<^verbatim>\<open>-D\<close> extra Isabelle components in a Mercurial repository clone to
   be considered by the poller and CI jobs.
diff -r 0f22f7b370b2 -r 1be62b17bed9 src/Doc/System/document/root.tex
--- a/src/Doc/System/document/root.tex	Sun Feb 02 14:16:26 2025 +0100
+++ b/src/Doc/System/document/root.tex	Sun Feb 02 16:04:09 2025 +0100
@@ -19,7 +19,9 @@
 
 \title{\includegraphics[scale=0.5]{isabelle_logo} \\[4ex] The Isabelle System Manual}
 
-\author{\emph{Makarius Wenzel}}
+\author{\emph{Makarius Wenzel} \\[3ex]
+  With Contributions by
+  Fabian Huch}
 
 \makeindex