comparison tools/make_template.ml @ 23:c8070689f5ca

Switch [input_line] to [read_line]
author Adam Chlipala <adamc@hcoop.net>
date Fri, 05 Sep 2008 16:48:13 -0400
parents 91e247c68ee8
children d45ba7e9b266
comparison
equal deleted inserted replaced
22:91e247c68ee8 23:c8070689f5ca
1 let input_line () = 1 let read_line () =
2 try 2 try
3 Some (input_line stdin) 3 Some (read_line ())
4 with End_of_file -> None 4 with End_of_file -> None
5 5
6 let rec initial last_was_empty = 6 let rec initial last_was_empty =
7 match input_line () with 7 match read_line () with
8 | None -> () 8 | None -> ()
9 | Some "(* begin thide *)" -> thide last_was_empty 9 | Some "(* begin thide *)" -> thide last_was_empty
10 | Some "" -> 10 | Some "" ->
11 if not (last_was_empty) then 11 if not (last_was_empty) then
12 print_newline (); 12 print_newline ();
21 print_endline line; 21 print_endline line;
22 initial false 22 initial false
23 end 23 end
24 24
25 and comment last_was_empty = 25 and comment last_was_empty =
26 match input_line () with 26 match read_line () with
27 | None -> () 27 | None -> ()
28 | Some line -> 28 | Some line ->
29 if String.length line >= 2 && line.[String.length line - 2] = '*' 29 if String.length line >= 2 && line.[String.length line - 2] = '*'
30 && line.[String.length line - 1] = ')' then 30 && line.[String.length line - 1] = ')' then
31 initial last_was_empty 31 initial last_was_empty
32 else 32 else
33 comment last_was_empty 33 comment last_was_empty
34 34
35 and thide last_was_empty = 35 and thide last_was_empty =
36 match input_line () with 36 match read_line () with
37 | None -> () 37 | None -> ()
38 | Some "(* end thide *)" -> initial last_was_empty 38 | Some "(* end thide *)" -> initial last_was_empty
39 | Some _ -> thide last_was_empty 39 | Some _ -> thide last_was_empty
40 40
41 let () = initial false 41 let () = initial false