# 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.")