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