--- a/src/Pure/PIDE/document.ML Wed Aug 11 18:44:06 2010 +0200
+++ b/src/Pure/PIDE/document.ML Wed Aug 11 22:41:26 2010 +0200
@@ -7,10 +7,12 @@
signature DOCUMENT =
sig
- type state_id = string
- type command_id = string
- type version_id = string
- val no_id: string
+ type state_id = int
+ type command_id = int
+ type version_id = int
+ val no_id: int
+ val parse_id: string -> int
+ val print_id: int -> string
type edit = string * ((command_id * command_id option) list) option
end;
@@ -19,11 +21,18 @@
(* unique identifiers *)
-type state_id = string;
-type command_id = string;
-type version_id = string;
+type state_id = int;
+type command_id = int;
+type version_id = int;
+
+val no_id = 0;
-val no_id = "";
+fun parse_id s =
+ (case Int.fromString s of
+ SOME i => i
+ | NONE => raise Fail ("Bad id: " ^ quote s));
+
+val print_id = signed_string_of_int;
(* edits *)