src/Pure/PIDE/document.ML
changeset 38414 49f1f657adc2
parent 38373 e8197eea3cd0
child 38418 9a7af64d71bb
     1.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 14 21:25:20 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 14 22:45:23 2010 +0200
     1.3 @@ -29,12 +29,8 @@
     1.4  
     1.5  val no_id = 0;
     1.6  
     1.7 -fun parse_id s =
     1.8 -  (case Int.fromString s of
     1.9 -    SOME i => i
    1.10 -  | NONE => raise Fail ("Bad id: " ^ quote s));
    1.11 -
    1.12 -val print_id = signed_string_of_int;
    1.13 +val parse_id = Markup.parse_int;
    1.14 +val print_id = Markup.print_int;
    1.15  
    1.16  
    1.17  (* edits *)