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