Skip to content

C
cpdt
Commit 475c6b74 authored by Adam Chlipala's avatar Adam Chlipala
Browse files
Options

Switch [input_line] to [read_line]

parent e450fe0b
Show whitespace changes
Inline Side-by-side
Showing with 5 additions and 5 deletions
tools/make_template.ml
View file @ 475c6b74
let input_line () = let read_line () =
try try
Some (input_line stdin) Some (read_line ())
with End_of_file -> None with End_of_file -> None
let rec initial last_was_empty = let rec initial last_was_empty =
match input_line () with match read_line () with
| None -> () | None -> ()
| Some "(* begin thide *)" -> thide last_was_empty | Some "(* begin thide *)" -> thide last_was_empty
| Some "" -> | Some "" ->
...@@ -23,7 +23,7 @@ let rec initial last_was_empty = ...@@ -23,7 +23,7 @@ let rec initial last_was_empty =
end end
and comment last_was_empty = and comment last_was_empty =
match input_line () with match read_line () with
| None -> () | None -> ()
| Some line -> | Some line ->
if String.length line >= 2 && line.[String.length line - 2] = '*' if String.length line >= 2 && line.[String.length line - 2] = '*'
...@@ -33,7 +33,7 @@ and comment last_was_empty = ...@@ -33,7 +33,7 @@ and comment last_was_empty =
comment last_was_empty comment last_was_empty
and thide last_was_empty = and thide last_was_empty =
match input_line () with match read_line () with
| None -> () | None -> ()
| Some "(* end thide *)" -> initial last_was_empty | Some "(* end thide *)" -> initial last_was_empty
| Some _ -> thide last_was_empty | Some _ -> thide last_was_empty
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment