--- a/src/Tools/Find_Facts/web/src/Details.elm Fri Feb 14 19:34:27 2025 +0100
+++ b/src/Tools/Find_Facts/web/src/Details.elm Fri Feb 14 20:10:57 2025 +0100
@@ -55,4 +55,4 @@
h2 [Typography.headline4] [text "Details"],
h3 [Typography.headline6]
[text "In ", a [href url] [text theory], text (" (" ++ block.file ++ ")")],
- Utils.view_code code start_before]
+ Utils.view_code code start_before Nothing]
--- a/src/Tools/Find_Facts/web/src/Results.elm Fri Feb 14 19:34:27 2025 +0100
+++ b/src/Tools/Find_Facts/web/src/Results.elm Fri Feb 14 20:10:57 2025 +0100
@@ -78,7 +78,7 @@
(LayoutGrid.layoutGrid [LayoutGrid.alignLeft, style "width" "100%"] [
div [Typography.caption, style "margin-bottom" "8px"]
[text (block.session ++ "/" ++ block.file_name)],
- Utils.view_code block.html block.start_line]),
+ Utils.view_code block.html block.start_line (Just 34)]),
[])}
view_results blocks is_loading =
--- a/src/Tools/Find_Facts/web/src/Utils.elm Fri Feb 14 19:34:27 2025 +0100
+++ b/src/Tools/Find_Facts/web/src/Utils.elm Fri Feb 14 20:10:57 2025 +0100
@@ -51,13 +51,26 @@
Ok nodes -> span [] (Html.Parser.Util.toVirtualDom nodes)
_ -> text (String.stripTags html)
-view_code: String -> Int -> Html msg
-view_code src start =
+view_code: String -> Int -> Maybe Int -> Html msg
+view_code src start max_lines =
let
view_line i line =
"<div style=\"width:5ch; color:gray; text-align:right; display:inline-block\">" ++ (String.fromInt (start + i)) ++ "</div> " ++ line
- src1 = split_lines src |> List.indexedMap view_line |> String.join "\n"
- in Html.pre [class "source"] [view_html src1]
+ lines = split_lines src
+ fade = """
+linear-gradient(
+ to bottom,
+ rgba(0,0,0, 1) 0,
+ rgba(0,0,0, 1) 80%,
+ rgba(0,0,0, 0) 95%,
+ rgba(0,0,0, 0) 0)
+100% 50% / 100% 100% repeat-x
+ """
+ limit f =
+ max_lines
+ |> Maybe.filter ((>) (List.length lines)) |> Maybe.map f |> Maybe.withDefault identity
+ src1 = lines |> limit List.take |> List.indexedMap view_line |> String.join "\n"
+ in Html.pre (limit (always ((::) (style "mask" fade))) [class "source"]) [view_html src1]
outside_elem: String -> Decode.Decoder Bool