src/Pure/PIDE/document.ML
changeset 38355 8cb265fb12fe
parent 38150 67fc24df3721
child 38363 af7f41a8a0a8
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Aug 11 18:44:06 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Aug 11 22:41:26 2010 +0200
     1.3 @@ -7,10 +7,12 @@
     1.4  
     1.5  signature DOCUMENT =
     1.6  sig
     1.7 -  type state_id = string
     1.8 -  type command_id = string
     1.9 -  type version_id = string
    1.10 -  val no_id: string
    1.11 +  type state_id = int
    1.12 +  type command_id = int
    1.13 +  type version_id = int
    1.14 +  val no_id: int
    1.15 +  val parse_id: string -> int
    1.16 +  val print_id: int -> string
    1.17    type edit = string * ((command_id * command_id option) list) option
    1.18  end;
    1.19  
    1.20 @@ -19,11 +21,18 @@
    1.21  
    1.22  (* unique identifiers *)
    1.23  
    1.24 -type state_id = string;
    1.25 -type command_id = string;
    1.26 -type version_id = string;
    1.27 +type state_id = int;
    1.28 +type command_id = int;
    1.29 +type version_id = int;
    1.30 +
    1.31 +val no_id = 0;
    1.32  
    1.33 -val no_id = "";
    1.34 +fun parse_id s =
    1.35 +  (case Int.fromString s of
    1.36 +    SOME i => i
    1.37 +  | NONE => raise Fail ("Bad id: " ^ quote s));
    1.38 +
    1.39 +val print_id = signed_string_of_int;
    1.40  
    1.41  
    1.42  (* edits *)