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