# HG changeset patch
# User aspinall
# Date 1167854424 -3600
# Node ID 4bb32c127529cd7ed4da63ec628a2c314ed14876
# Parent  d22f7e3c5ad9d2f13549fc872f976b66847cfdbf
Selected functions from syntax module

diff -r d22f7e3c5ad9 -r 4bb32c127529 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
+