clarified find_facts URL;
authorFabian Huch <huch@in.tum.de>
Tue, 21 Jan 2025 17:15:52 +0100
changeset 81892 f1d520cd7575
parent 81891 560c7ff87f74
child 81893 78b8b776fd1f
clarified find_facts URL;
NEWS
src/Tools/Find_Facts/src/find_facts.scala
--- 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 = {