src/Pure/ProofGeneral/syntax_standalone.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ProofGeneral/syntax_standalone.ML	Wed Jan 03 21:00:24 2007 +0100
@@ -0,0 +1,33 @@
+(* Taken from ../Syntax/lexicon.ML, which otherwise pulls in whole
+   term structure of Isabelle
+*)
+signature SYNTAX = 
+sig
+  val read_int: string -> int option
+  val read_nat: string -> int option
+end
+
+structure Syntax : SYNTAX = 
+struct
+
+local
+
+val scan_digits1 = Scan.many1 Symbol.is_digit;
+
+fun nat cs =
+  Option.map (#1 o Library.read_int)
+    (Scan.read Symbol.stopper scan_digits1 cs);
+
+in
+
+val read_nat = nat o Symbol.explode;
+
+fun read_int s =
+  (case Symbol.explode s of
+    "-" :: cs => Option.map ~ (nat cs)
+  | cs => nat cs);
+
+end;
+
+end
+