# HG changeset patch # User wenzelm # Date 1167943012 -3600 # Node ID b0c966b3006607344d91e816915c48facaf18ef6 # Parent bfc462bfc574e948080212c7a978671f9b8b5320 approximate Syntax.read_int/nat by Int.fromString -- avoids dependency on Syntax module; diff -r bfc462bfc574 -r b0c966b30066 src/Pure/ProofGeneral/pgip_types.ML --- a/src/Pure/ProofGeneral/pgip_types.ML Thu Jan 04 21:18:05 2007 +0100 +++ b/src/Pure/ProofGeneral/pgip_types.ML Thu Jan 04 21:36:52 2007 +0100 @@ -198,15 +198,16 @@ | int_in_range (SOME min,SOME max) i = min<= i andalso i<=max in fun read_pgipint range s = - (case Syntax.read_int s of + (case Int.fromString s of SOME i => if int_in_range range i then i else raise PGIP ("Out of range integer value: " ^ quote s) | NONE => raise PGIP ("Invalid integer value: " ^ quote s)) end; fun read_pgipnat s = - (case Syntax.read_nat s of - SOME i => i + (case Int.fromString s of + SOME i => if i >= 0 then i + else raise PGIP ("Invalid natural number: " ^ quote s) | NONE => raise PGIP ("Invalid natural number: " ^ quote s)) (* NB: we can maybe do without xml decode/encode here. *) @@ -406,7 +407,7 @@ end fun pgipint_of_string err s = - case Syntax.read_int s of + case Int.fromString s of SOME i => i | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.")