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 *)