annotate tools/make_template.ml @ 574:1dc1d41620b6

Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents 3fc43e261f67
children
rev   line source
adam@571 1 let read_line () =
adamc@22 2 try
adamc@23 3 Some (read_line ())
adamc@22 4 with End_of_file -> None
adamc@22 5
adamc@22 6 let rec initial last_was_empty =
adamc@23 7 match read_line () with
adamc@22 8 | None -> ()
adamc@22 9 | Some "(* begin thide *)" -> thide last_was_empty
adamc@22 10 | Some "" ->
adam@571 11 if not (last_was_empty) then
adam@571 12 print_newline ();
adam@571 13 initial true
adamc@22 14 | Some line ->
adam@571 15 let idx = try Some (String.index line '(') with Not_found -> None in
adam@571 16 match idx with
adam@571 17 | Some idx ->
adam@571 18 if String.length line > idx+1 && line.[idx+1] = '*'
adam@571 19 && not (String.length line > idx+4 && String.sub line (idx+2) 3 = " EX") then
adam@571 20 if line.[String.length line - 2] = '*' && line.[String.length line - 1] = ')' then
adam@571 21 initial last_was_empty
adam@571 22 else
adam@571 23 comment 1 last_was_empty
adam@571 24 else begin
adam@571 25 print_endline line;
adam@571 26 initial false
adam@571 27 end
adam@571 28 | None ->
adam@571 29 print_endline line;
adam@571 30 initial false
adamc@22 31
adamc@77 32 and comment count last_was_empty =
adamc@23 33 match read_line () with
adamc@22 34 | None -> ()
adamc@22 35 | Some line ->
adam@571 36 if String.length line >= 2 && line.[0] = '(' && line.[1] = '*' then
adam@571 37 if String.length line >= 2 && line.[String.length line - 2] = '*'
adam@571 38 && line.[String.length line - 1] = ')' then
adam@571 39 comment count last_was_empty
adamc@22 40 else
adam@571 41 comment (count+1) last_was_empty
adam@571 42 else if String.length line >= 2 && line.[String.length line - 2] = '*'
adam@571 43 && line.[String.length line - 1] = ')' then
adam@571 44 if try
adam@571 45 let idx = String.index line '(' in
adam@571 46 idx < String.length line - 1 && line.[idx + 1] = '*'
adam@571 47 with Not_found -> false then
adam@571 48 comment count last_was_empty
adam@571 49 else if count = 1 then
adam@571 50 initial last_was_empty
adam@571 51 else
adam@571 52 comment (count-1) last_was_empty
adam@571 53 else
adam@571 54 comment count last_was_empty
adamc@22 55
adamc@22 56 and thide last_was_empty =
adamc@23 57 match read_line () with
adamc@22 58 | None -> ()
adamc@22 59 | Some "(* end thide *)" -> initial last_was_empty
adamc@22 60 | Some _ -> thide last_was_empty
adamc@22 61
adamc@22 62 let () = initial false