# HG changeset patch
# User wenzelm
# Date 1738446573 -3600
# Node ID cb121d499f11505847827ba34f1c83a3198da95e
# Parent  5be1b43546386a9385e4451efac91dbc57e792a9# Parent  17436dc0d3d4331b22c5af50f6576d83039e36f5
merged;

diff -r 5be1b4354638 -r cb121d499f11 NEWS
--- a/NEWS	Sat Feb 01 22:41:05 2025 +0100
+++ b/NEWS	Sat Feb 01 22:49:33 2025 +0100
@@ -398,7 +398,7 @@
 Apache Solr (see also https://solr.apache.org). Minimal example:
 
     isabelle find_facts_index HOL
-    isabelle find_facts_server
+    isabelle find_facts_server -p 8080
     open http://localhost:8080/find_facts#search?q=Hilbert
 
 Persistent data is stored in $ISABELLE_HOME_USER/find_facts/.
diff -r 5be1b4354638 -r cb121d499f11 src/Doc/System/Presentation.thy
--- a/src/Doc/System/Presentation.thy	Sat Feb 01 22:41:05 2025 +0100
+++ b/src/Doc/System/Presentation.thy	Sat Feb 01 22:49:33 2025 +0100
@@ -202,4 +202,59 @@
   @{verbatim [display] \<open>isabelle document -v -V -O. FOL\<close>}
 \<close>
 
+
+section \<open>Full-text search for formal theory content\<close>
+
+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>,
+  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
+  the search index can be specified via system option 
+  @{system_option find_facts_database_name}. A finished search index can be
+  packed for later use as a regular Isabelle component using the 
+  @{tool_def find_facts_index_build} tool: Initializing such a component
+  causes it to be added to the list of managed components in
+  @{setting FIND_FACTS_INDEXES}.
+
+  \<^medskip>
+  The user interface of the search is available as web application that 
+  can be started with the @{tool_def find_facts_server} tool. Its usage is:
+  @{verbatim [display]
+\<open>Usage: isabelle find_facts_server [OPTIONS]
+
+  Options are:
+    -d           devel mode
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -p PORT      explicit web server port
+    -v           verbose server
+
+  Run server for Find_Facts.
+\<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
+  endpoints for search queries with JSON data.
+
+  Options \<^verbatim>\<open>-o\<close>, \<open>-v\<close> have the same meaning as usual.
+
+  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. 
+\<close>
+
 end
diff -r 5be1b4354638 -r cb121d499f11 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Sat Feb 01 22:41:05 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Sat Feb 01 22:49:33 2025 +0100
@@ -888,11 +888,9 @@
   val web_sources: Path = Path.explode("$FIND_FACTS_HOME/web")
   val web_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/web")
 
-  val default_port = 8080
-
   def find_facts_server(
     options: Options,
-    port: Int = default_port,
+    port: Int = 0,
     devel: Boolean = false,
     progress: Progress = new Progress
   ): Unit = {
@@ -977,7 +975,7 @@
     Command_Line.tool {
       var devel = false
       var options = Options.init()
-      var port = default_port
+      var port = 0
       var verbose = false
 
       val getopts = Getopts("""
@@ -986,7 +984,7 @@
   Options are:
     -d           devel mode
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
-    -p PORT      explicit web server port (default: """ + default_port + """)
+    -p PORT      explicit server port
     -v           verbose server
 
   Run server for Find_Facts.