From 598ce9ecef91264bd78555bd5b6fcca97a073d95 Mon Sep 17 00:00:00 2001 From: Marc Coquand Date: Mon, 10 Jun 2024 11:58:16 -0500 Subject: Hide file names by default --- lib/done.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'lib/done.ml') diff --git a/lib/done.ml b/lib/done.ml index 5b8ad2c..650b9f7 100644 --- a/lib/done.ml +++ b/lib/done.ml @@ -24,8 +24,9 @@ let title ~tag = let content_start = 2 let init ~goto_todo ~goto_headlines = + let hide_file_name = true in let content = Grep.get_done () |> Grep.parse_todo_string in - let content_pretty = Grep.pretty_format_todo content in + let content_pretty = Grep.pretty_format_todo ~hide_file_name content in { pos = 0, content_start ; scroll = 0 ; content = content |> Array.of_list @@ -34,7 +35,7 @@ let init ~goto_todo ~goto_headlines = ; goto_todo ; tag = "" ; output = None - ; hide_file_name = false + ; hide_file_name } @@ -122,7 +123,7 @@ let rec render t { state with content = content |> Array.of_list - ; content_pretty = content_pretty |> Array.of_list + ; content_pretty = content_pretty ~hide_file_name |> Array.of_list ; tag }) ; on_cancel = -- cgit v1.2.3