# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1739560257 -3600
# Node ID 812d9ed6925e633586a3f1205a2b9c0079146525
# Parent  0dd633d9ae63b2170b35d718872569c263b9b5fd
limit size of overly large blocks;

diff -r 0dd633d9ae63 -r 812d9ed6925e src/Tools/Find_Facts/web/src/Details.elm
--- 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]
diff -r 0dd633d9ae63 -r 812d9ed6925e src/Tools/Find_Facts/web/src/Results.elm
--- 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 =
diff -r 0dd633d9ae63 -r 812d9ed6925e src/Tools/Find_Facts/web/src/Utils.elm
--- 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