--- a/NEWS Tue Jan 21 17:13:06 2025 +0100
+++ b/NEWS Tue Jan 21 17:15:52 2025 +0100
@@ -361,7 +361,7 @@
isabelle find_facts_index HOL
isabelle find_facts_server
- open http://localhost:8080/app#search?q=Hilbert
+ open http://localhost:8080/find_facts#search?q=Hilbert
Persistent data is stored in $ISABELLE_HOME_USER/find_facts/.
--- a/src/Tools/Find_Facts/src/find_facts.scala Tue Jan 21 17:13:06 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala Tue Jan 21 17:15:52 2025 +0100
@@ -924,7 +924,7 @@
def apply(request: HTTP.Request): Option[HTTP.Response] =
Some(HTTP.Response(Bytes(isabelle_style), "text/css"))
},
- new HTTP.Service("app") {
+ new HTTP.Service("find_facts") {
def apply(request: HTTP.Request): Option[HTTP.Response] =
Some(HTTP.Response.html(
if (devel) project.build_html(progress = progress) else frontend))
@@ -951,7 +951,7 @@
}))
server.start()
- progress.echo("Server started " + server.toString + "/app")
+ progress.echo("Server started " + server.toString + "/find_facts")
@tailrec
def loop(): Unit = {