clarified;
authorFabian Huch <huch@in.tum.de>
Fri, 14 Feb 2025 20:12:18 +0100
changeset 82174 4a10892b6a00
parent 82173 812d9ed6925e
child 82175 2213186e5928
clarified;
src/Tools/Find_Facts/web/src/Searcher.elm
src/Tools/Find_Facts/web/src/Utils.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) =
--- 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