# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1739560338 -3600
# Node ID 4a10892b6a005c624f9f62e78bbe24c6189c10c3
# Parent  812d9ed6925e633586a3f1205a2b9c0079146525
clarified;

diff -r 812d9ed6925e -r 4a10892b6a00 src/Tools/Find_Facts/web/src/Searcher.elm
--- a/src/Tools/Find_Facts/web/src/Searcher.elm	Fri Feb 14 20:10:57 2025 +0100
+++ b/src/Tools/Find_Facts/web/src/Searcher.elm	Fri Feb 14 20:12:18 2025 +0100
@@ -271,16 +271,13 @@
 isabelle_icon_button s =
   IconButton.customIcon
     Html.i
-    [class "material-icons", style "vertical-align" "top",
-      style "font-family" "\"Isabelle DejaVu Sans Mono\", monospace", style "font-size" "math"]
+    [class "material-icons", style "vertical-align" "top", Utils.isabelle_font,
+     style "font-size" "math"]
     [Html.text s]
 
 isabelle_icon_textfield s =
   TextFieldIcon.customIcon
-    Html.i
-    [class "material-icons", style "font-family" "\"Isabelle DejaVu Sans Mono\", monospace",
-      style "font-size" "larger"]
-    [Html.text s]
+    Html.i [class "material-icons", Utils.isabelle_font, style "font-size" "larger"] [Html.text s]
 
 view_filter: Maybe String -> Dict String Int -> (Int, Filter) -> Html Msg
 view_filter search0 counts (i, filter) =
diff -r 812d9ed6925e -r 4a10892b6a00 src/Tools/Find_Facts/web/src/Utils.elm
--- a/src/Tools/Find_Facts/web/src/Utils.elm	Fri Feb 14 20:10:57 2025 +0100
+++ b/src/Tools/Find_Facts/web/src/Utils.elm	Fri Feb 14 20:12:18 2025 +0100
@@ -80,4 +80,7 @@
     Decode.oneOf [
       Decode.field "name" Decode.string |> Decode.andThen decode_name,
       Decode.lazy (\_ -> outside_elem name |> Decode.field "parentNode"),
-      Decode.succeed True]
\ No newline at end of file
+      Decode.succeed True]
+
+isabelle_font : Attribute msg
+isabelle_font = style "font-family" "\"Isabelle DejaVu Sans Mono\", monospace"
\ No newline at end of file