# HG changeset patch
# User desharna
# Date 1739346495 -3600
# Node ID b97cea26d3a3805ba380561670848e0b2608a6a3
# Parent  5d57110da8eb787b2bbf4f1cc055ed4ee2dbe2e5# Parent  08475a3360a88bd7bbac25e599b8797ce9c356b7
merged

diff -r 08475a3360a8 -r b97cea26d3a3 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Wed Feb 12 08:47:44 2025 +0100
+++ b/src/Pure/General/http.scala	Wed Feb 12 08:48:15 2025 +0100
@@ -379,9 +379,10 @@
 
   object CSS_Service extends CSS()
 
-  class CSS(name: String = "css", fonts: String = Fonts_Service.name) extends Service(name) {
+  class CSS(name: String = "isabelle.css", fonts: String = Fonts_Service.name)
+    extends Service(name) {
     private lazy val css =
-      HTML.fonts_css("/" + fonts + "/" + _) + "\n\n" + File.read(HTML.isabelle_css)
+      HTML.fonts_css(fonts + "/" + _) + "\n\n" + File.read(HTML.isabelle_css)
 
     def apply(request: Request): Option[Response] =
       Some(Response(Bytes(css), Content.mime_type_css))
diff -r 08475a3360a8 -r b97cea26d3a3 src/Tools/Find_Facts/web/src/Main.elm
--- a/src/Tools/Find_Facts/web/src/Main.elm	Wed Feb 12 08:47:44 2025 +0100
+++ b/src/Tools/Find_Facts/web/src/Main.elm	Wed Feb 12 08:48:15 2025 +0100
@@ -82,6 +82,7 @@
 
 
 {- url encoding/decoding -}
+{- NB: routing only in URL fragment. -}
 
 aboutN = "about"
 searchN = "search"
@@ -128,7 +129,7 @@
 
 get_result: Query -> Cmd Msg
 get_result query =
-  Http.post {url="/api/query", expect = Http.expectJson (Query_Result query) Query.decode_result,
+  Http.post {url="api/query", expect = Http.expectJson (Query_Result query) Query.decode_result,
     body = query |> Query.encode_query |> Http.jsonBody}
 
 query_delay: Query -> Delay Msg
@@ -136,12 +137,12 @@
 
 get_blocks: Query -> String -> Cmd Msg
 get_blocks query cursor =
-  Http.post {url = "/api/blocks", expect = Http.expectJson (Query_Blocks query) Query.decode_blocks,
+  Http.post {url = "api/blocks", expect = Http.expectJson (Query_Blocks query) Query.decode_blocks,
     body = {query = query, cursor = cursor} |> Query.encode_query_blocks |> Http.jsonBody}
 
 get_block: String -> Cmd Msg
 get_block id =
-  Http.post {url = "/api/block", expect = Http.expectJson (Query_Block id) Query.decode_block,
+  Http.post {url = "api/block", expect = Http.expectJson (Query_Block id) Query.decode_block,
     body = id |> Query.encode_query_block |> Http.jsonBody}
 
 
@@ -164,7 +165,9 @@
   case msg of
     Link_Clicked urlRequest ->
       case urlRequest of
-        Browser.Internal url -> (model, push_url True model.nav_key url)
+        Browser.Internal url ->
+          if url.path == model.url.path then (model, push_url True model.nav_key url)
+          else (model, Navigation.load (Url.toString url))
         Browser.External href -> (model, Navigation.load href)
 
     Url_Changed url ->