src/Pure/PIDE/document.ML
changeset 38414 49f1f657adc2
parent 38373 e8197eea3cd0
child 38418 9a7af64d71bb
--- a/src/Pure/PIDE/document.ML	Sat Aug 14 21:25:20 2010 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Aug 14 22:45:23 2010 +0200
@@ -29,12 +29,8 @@
 
 val no_id = 0;
 
-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;
+val parse_id = Markup.parse_int;
+val print_id = Markup.print_int;
 
 
 (* edits *)