--- 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