From 0111efe05b1a4c3644a1947d236cd3ca7011c3e8 Mon Sep 17 00:00:00 2001
From: Yoshihiro Imai <y.imai@aist.go.jp>
Date: Fri, 13 Dec 2024 10:39:55 +0900
Subject: [PATCH] refactor: Don't use sed in coq2html binary

---
 common.ml         | 34 ++++++++++++++++++++++++++++++++++
 common.mli        |  4 ++++
 generate_index.ml | 12 +++++++-----
 3 files changed, 45 insertions(+), 5 deletions(-)

diff --git a/common.ml b/common.ml
index 22a2c9a6..10d85119 100644
--- a/common.ml
+++ b/common.ml
@@ -5,3 +5,37 @@ let shell cmd =
     prerr_endline ("Common.shell Error: " ^ cmd);
     exit status
   end
+
+let wrap_result f x =
+  try Ok (f x) with
+  | exn -> Error exn
+
+let unwrap_result = function
+  | Ok x -> x
+  | Error exn -> raise exn
+
+let file_using_r filename f =
+  let read_ch = open_in filename in
+  let result = wrap_result f read_ch in
+  close_in read_ch;
+  unwrap_result result
+
+let file_using_w filename f =
+  let write_ch = open_out filename in
+  let result = wrap_result f write_ch in
+  close_out write_ch;
+  unwrap_result result
+
+let read_lines filename =
+  file_using_r filename begin fun read_ch ->
+    let rec iter store =
+      try iter (input_line read_ch :: store) with
+      | End_of_file -> List.rev store
+    in
+    iter []
+  end
+
+let write_lines filename lines =
+  file_using_w filename begin fun out_ch ->
+    List.iter (Printf.fprintf out_ch "%s\n") lines
+  end
diff --git a/common.mli b/common.mli
index f5628c29..f535ac5d 100644
--- a/common.mli
+++ b/common.mli
@@ -1 +1,5 @@
 val shell : string -> unit
+
+
+val read_lines : string -> string list
+val write_lines : string -> string list -> unit
diff --git a/generate_index.ml b/generate_index.ml
index 48002cf8..49eb6ea5 100644
--- a/generate_index.ml
+++ b/generate_index.ml
@@ -228,11 +228,13 @@ let overwrite_dot_file_with_url xref_table dot_file = (* dirty *)
     !%{|"%s" [URL="%s"]|}  name url
   in
   let links = String.concat "; " (List.map node_with_node all_hb_defs) in
-  let tmp = dot_file ^ ".sed" in
-  let cmd = !%{|sed '2i %s' %s > %s|} links dot_file tmp in
-  Common.shell cmd;
-  Common.shell (!%"mv %s %s" tmp dot_file)
-
+  let lines = Common.read_lines dot_file in
+  let lines = match lines with (* insert links to second line *)
+     | line1 :: rest -> line1 :: links :: rest
+     | [] ->
+       failwith ("empty lines: " ^ dot_file)
+  in
+  Common.write_lines dot_file lines
 
 let generate_hierarchy_graph title xref_table output_dir dot_file =
   overwrite_dot_file_with_url xref_table dot_file;