Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/tools/make_template.ml Fri Sep 05 16:46:32 2008 -0400 +++ b/tools/make_template.ml Fri Sep 05 16:48:13 2008 -0400 @@ -1,10 +1,10 @@ -let input_line () = +let read_line () = try - Some (input_line stdin) + Some (read_line ()) with End_of_file -> None let rec initial last_was_empty = - match input_line () with + match read_line () with | None -> () | Some "(* begin thide *)" -> thide last_was_empty | Some "" -> @@ -23,7 +23,7 @@ end and comment last_was_empty = - match input_line () with + match read_line () with | None -> () | Some line -> if String.length line >= 2 && line.[String.length line - 2] = '*' @@ -33,7 +33,7 @@ comment last_was_empty and thide last_was_empty = - match input_line () with + match read_line () with | None -> () | Some "(* end thide *)" -> initial last_was_empty | Some _ -> thide last_was_empty