blob: b60fdf4a8c5fc8b91370599418a3c885efae53ee (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the GNU Lesser General Public License as *)
(* published by the Free Software Foundation, either version 2.1 of *)
(* the License, or (at your option) any later version. *)
(* This file is also distributed under the terms of the *)
(* INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(* Print lines from a file *)
type filebuf = {
chan: in_channel;
mutable lineno: int (* current line number *)
}
(* Invariant: the current position of [b.chan] is
the first character of line number [b.lineno]. *)
let openfile f =
{ chan = open_in_bin f;
lineno = 1 }
let close b =
close_in b.chan
(* Position [b] to the beginning of line [dest], which must be greater
or equal to the current line.
Return [true] if success, [false] if this line does not exist. *)
let forward b dest =
assert (dest >= b.lineno);
try
while b.lineno <> dest do
let c = input_char b.chan in
if c = '\n' then b.lineno <- b.lineno + 1;
done;
true
with End_of_file ->
false
(* Position [b] to the beginning of line [dest], which must be less than
the current line. *)
let backward_buf = lazy (Bytes.create 65536)
(* 65536 to match [IO_BUFFER_SIZE] in the OCaml runtime.
lazy to allocate on demand. *)
let backward b dest =
assert (1 <= dest && dest < b.lineno);
let buf = Lazy.force backward_buf in
let rec backward pos idx =
(* pos is the file position corresponding to index 0 in buf *)
(* idx is the current index in buf *)
if idx <= 0 then begin
if pos = 0 then begin
(* beginning of file reached = beginning of line 1. *)
(* assert (dest = 1 && b.lineno = 1) *)
seek_in b.chan 0;
b.lineno <- 1
end else begin
let pos' = max 0 (pos - Bytes.length buf) in
let len = pos - pos' in
seek_in b.chan pos';
really_input b.chan buf 0 len;
backward pos' (pos - pos')
end
end else if Bytes.get buf (idx-1) = '\n' then begin
(* Reached beginning of current line *)
if b.lineno = dest then begin
(* Found line number dest *)
seek_in b.chan (pos + idx)
end else begin
(* Move into previous line *)
b.lineno <- b.lineno - 1;
backward pos (idx - 1)
end
end else
backward pos (idx - 1)
in
backward (pos_in b.chan) 0
(* Absolute positioning *)
let move b dest =
if dest >= b.lineno then forward b dest else (backward b dest; true)
(* Main function: copy lines from [first] to [last] to [oc], prefixed
by [pref]. *)
let copy oc pref b first last =
if move b first then begin
output_string oc pref;
try
while b.lineno <= last do
let c = input_char b.chan in
output_char oc c;
if c = '\n' then begin
b.lineno <- b.lineno + 1;
if b.lineno <= last then output_string oc pref
end
done
with End_of_file ->
output_char oc '\n'
end
|
