diff options
Diffstat (limited to 'stdlib')
-rw-r--r-- | stdlib/obj.ml | 2 | ||||
-rw-r--r-- | stdlib/obj.mli | 2 | ||||
-rw-r--r-- | stdlib/pervasives.ml | 5 | ||||
-rw-r--r-- | stdlib/pervasives.mli | 4 | ||||
-rw-r--r-- | stdlib/sys.ml | 1 | ||||
-rw-r--r-- | stdlib/sys.mli | 1 |
6 files changed, 11 insertions, 4 deletions
diff --git a/stdlib/obj.ml b/stdlib/obj.ml index af7ac7b7d..8129fa6b9 100644 --- a/stdlib/obj.ml +++ b/stdlib/obj.ml @@ -23,3 +23,5 @@ external size : t -> int = "%obj_size" external field : t -> int -> t = "%obj_field" external set_field : t -> int -> t -> unit = "%obj_set_field" external new_block : int -> int -> t = "obj_block" +external marshal : t -> string = "output_value_to_string" +external unmarshal : string -> int -> t * int = "input_value_from_string" diff --git a/stdlib/obj.mli b/stdlib/obj.mli index a37e8a266..9640871a5 100644 --- a/stdlib/obj.mli +++ b/stdlib/obj.mli @@ -25,3 +25,5 @@ external size : t -> int = "%obj_size" external field : t -> int -> t = "%obj_field" external set_field : t -> int -> t -> unit = "%obj_set_field" external new_block : int -> int -> t = "obj_block" +external marshal : t -> string = "output_value_to_string" +external unmarshal : string -> int -> t * int = "input_value_from_string" diff --git a/stdlib/pervasives.ml b/stdlib/pervasives.ml index 0da573cfb..4b17cc35a 100644 --- a/stdlib/pervasives.ml +++ b/stdlib/pervasives.ml @@ -189,7 +189,8 @@ external output_value : out_channel -> 'a -> unit = "output_value" external seek_out : out_channel -> int -> unit = "seek_out" external pos_out : out_channel -> int = "pos_out" external out_channel_length : out_channel -> int = "channel_size" -external close_out : out_channel -> unit = "close_out" +external close_out_channel : out_channel -> unit = "close_channel" +let close_out oc = flush oc; close_out_channel oc (* General input functions *) @@ -250,7 +251,7 @@ external input_value : in_channel -> 'a = "input_value" external seek_in : in_channel -> int -> unit = "seek_in" external pos_in : in_channel -> int = "pos_in" external in_channel_length : in_channel -> int = "channel_size" -external close_in : in_channel -> unit = "close_in" +external close_in : in_channel -> unit = "close_channel" (* Output functions on standard output *) diff --git a/stdlib/pervasives.mli b/stdlib/pervasives.mli index e6bf9a5c2..027d5bffa 100644 --- a/stdlib/pervasives.mli +++ b/stdlib/pervasives.mli @@ -412,7 +412,7 @@ external out_channel_length : out_channel -> int = "channel_size" (* Return the total length (number of characters) of the given channel. This works only for regular files. On files of other kinds, the result is meaningless. *) -external close_out : out_channel -> unit = "close_out" +val close_out : out_channel -> unit (* Close the given channel, flushing all buffered write operations. The behavior is unspecified if any of the functions above is called on a closed channel. *) @@ -491,7 +491,7 @@ external in_channel_length : in_channel -> int = "channel_size" (* Return the total length (number of characters) of the given channel. This works only for regular files. On files of other kinds, the result is meaningless. *) -external close_in : in_channel -> unit = "close_in" +external close_in : in_channel -> unit = "close_channel" (* Close the given channel. Anything can happen if any of the functions above is called on a closed channel. *) diff --git a/stdlib/sys.ml b/stdlib/sys.ml index 1e76f3c9f..3f50f6ff2 100644 --- a/stdlib/sys.ml +++ b/stdlib/sys.ml @@ -54,6 +54,7 @@ let sigtstp = -17 let sigttin = -18 let sigttou = -19 let sigvtalrm = -20 +let sigprof = -21 exception Break diff --git a/stdlib/sys.mli b/stdlib/sys.mli index 450327487..d316a6e0e 100644 --- a/stdlib/sys.mli +++ b/stdlib/sys.mli @@ -74,6 +74,7 @@ val sigtstp: int (* Interactive stop *) val sigttin: int (* Terminal read from background process *) val sigttou: int (* Terminal write from background process *) val sigvtalrm: int (* Timeout in virtual time *) +val sigprof: int (* Profiling interrupt *) (* Signal numbers for the standard POSIX signals. *) exception Break |