From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- lib/stateid.ml | 28 +++++++++++++--------------- 1 file changed, 13 insertions(+), 15 deletions(-) (limited to 'lib/stateid.ml') diff --git a/lib/stateid.ml b/lib/stateid.ml index 59cf206e..ae25735c 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Xml_datatype - type t = int let initial = 1 let dummy = 0 @@ -15,29 +13,29 @@ let fresh, in_range = let cur = ref initial in (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur) let to_string = string_of_int -let of_int id = assert(in_range id); id +let of_int id = + (* Coqide too to parse ids too, but cannot check if they are valid. + * Hence we check for validity only if we are an ide slave. *) + if !Flags.ide_slave then assert (in_range id); + id let to_int id = id let newer_than id1 id2 = id1 > id2 -let of_xml = function - | Element ("state_id",["val",i],[]) -> - let id = int_of_string i in - (* Coqide too to parse ids too, but cannot check if they are valid. - * Hence we check for validity only if we are an ide slave. *) - if !Flags.ide_slave then assert(in_range id); - id - | _ -> raise (Invalid_argument "to_state_id") -let to_xml i = Element ("state_id",["val",string_of_int i],[]) - let state_id_info : (t * t) Exninfo.t = Exninfo.make () -let add exn ?(valid = initial) id = +let add exn ~valid id = Exninfo.add exn state_id_info (valid, id) let get exn = Exninfo.get exn state_id_info let equal = Int.equal let compare = Int.compare -module Set = Set.Make(struct type t = int let compare = compare end) +module Self = struct + type t = int + let compare = compare + let equal = equal +end + +module Set = Set.Make(Self) type ('a,'b) request = { exn_info : t * t; -- cgit v1.2.3