# HG changeset patch
# User wenzelm
# Date 1189947148 -7200
# Node ID 6689effe75d1ba34d6d60329fde8d45f915329e6
# Parent  1547ea587f5a23f7ba12a12b1dd1c85b99e34c63
Minimal parsing for SML -- fixing integer numerals.

diff -r 1547ea587f5a -r 6689effe75d1 src/Pure/ML/ml_parse.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_parse.ML	Sun Sep 16 14:52:28 2007 +0200
@@ -0,0 +1,65 @@
+(*  Title:      Pure/ML/ml_parse.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Minimal parsing for SML -- fixing integer numerals.
+*)
+
+signature ML_PARSE =
+sig
+  val fix_ints: string -> string
+end;
+
+structure ML_Parse: ML_PARSE =
+struct
+
+structure T = ML_Lex;
+
+
+(** error handling **)
+
+fun !!! scan =
+  let
+    fun get_pos [] = " (past end-of-file!)"
+      | get_pos (tok :: _) = T.pos_of tok;
+
+    fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
+      | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
+  in Scan.!! err scan end;
+
+fun bad_input x =
+  (Scan.some (fn tok => (case T.kind_of tok of T.Error msg => SOME msg | _ => NONE)) :|--
+    (fn msg => Scan.fail_with (K msg))) x;
+
+
+(** basic parsers **)
+
+fun $$$ x = Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.val_of tok = x) >> T.val_of;
+val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.val_of;
+
+val regular = Scan.one T.is_regular >> T.val_of;
+val improper = Scan.one T.is_improper >> T.val_of;
+
+val blanks = Scan.repeat improper >> implode;
+
+
+(* fix_ints *)
+
+(*approximation only -- corrupts numeric record field patterns *)
+val fix_int =
+  $$$ "#" ^^ blanks ^^ int ||
+  ($$$ "infix" || $$$ "infixr") ^^ blanks ^^ int ||
+  int >> (fn x => "(" ^ x ^ ":int)") ||
+  regular ||
+  bad_input;
+
+fun do_fix_ints s =
+  Source.of_string s
+  |> T.source
+  |> Source.source T.stopper (Scan.bulk (!!! fix_int)) NONE
+  |> Source.exhaust
+  |> implode;
+
+val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
+
+end;