1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ProofGeneral/syntax_standalone.ML	Wed Jan 03 21:00:24 2007 +0100
     1.3 @@ -0,0 +1,33 @@
     1.4 +(* Taken from ../Syntax/lexicon.ML, which otherwise pulls in whole
     1.5 +   term structure of Isabelle
     1.6 +*)
     1.7 +signature SYNTAX = 
     1.8 +sig
     1.9 +  val read_int: string -> int option
    1.10 +  val read_nat: string -> int option
    1.11 +end
    1.12 +
    1.13 +structure Syntax : SYNTAX = 
    1.14 +struct
    1.15 +
    1.16 +local
    1.17 +
    1.18 +val scan_digits1 = Scan.many1 Symbol.is_digit;
    1.19 +
    1.20 +fun nat cs =
    1.21 +  Option.map (#1 o Library.read_int)
    1.22 +    (Scan.read Symbol.stopper scan_digits1 cs);
    1.23 +
    1.24 +in
    1.25 +
    1.26 +val read_nat = nat o Symbol.explode;
    1.27 +
    1.28 +fun read_int s =
    1.29 +  (case Symbol.explode s of
    1.30 +    "-" :: cs => Option.map ~ (nat cs)
    1.31 +  | cs => nat cs);
    1.32 +
    1.33 +end;
    1.34 +
    1.35 +end
    1.36 +