diff options
| author | Guillaume Melquiond | 2015-09-29 17:45:27 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-09-29 17:45:27 +0200 |
| commit | 05ab666a1283de5500dbc0520d18bdb05d95f286 (patch) | |
| tree | 538cb7b07372d4e83a6c7823d5cb59ee54606099 /lib/system.mli | |
| parent | 82a618e8a4945752698a7900c8af7a51091f7b1b (diff) | |
Make the interface of System.raw_extern_intern much saner.
There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
Diffstat (limited to 'lib/system.mli')
| -rw-r--r-- | lib/system.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/lib/system.mli b/lib/system.mli index 5797502e9f..247d528b97 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -36,11 +36,13 @@ val find_file_in_path : exception Bad_magic_number of string -val raw_extern_intern : int -> - (string -> out_channel) * (string -> in_channel) +val raw_extern_state : int -> string -> out_channel -val extern_intern : int -> - (string -> 'a -> unit) * (string -> 'a) +val raw_intern_state : int -> string -> in_channel + +val extern_state : int -> string -> 'a -> unit + +val intern_state : int -> string -> 'a val with_magic_number_check : ('a -> 'b) -> 'a -> 'b |