src/Pure/ML/ml_parse.ML
author wenzelm
Thu Aug 02 12:36:54 2012 +0200 (2012-08-02)
changeset 48646 91281e9472d8
parent 43948 8f5add916a99
child 48911 5debc3e4fa81
permissions -rw-r--r--
more official command specifications, including source position;
     1 (*  Title:      Pure/ML/ml_parse.ML
     2     Author:     Makarius
     3 
     4 Minimal parsing for SML -- fixing integer numerals.
     5 *)
     6 
     7 signature ML_PARSE =
     8 sig
     9   val fix_ints: string -> string
    10   val global_context: use_context
    11 end;
    12 
    13 structure ML_Parse: ML_PARSE =
    14 struct
    15 
    16 (** error handling **)
    17 
    18 fun !!! scan =
    19   let
    20     fun get_pos [] = " (past end-of-file!)"
    21       | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok);
    22 
    23     fun err (toks, NONE) = (fn () => "SML syntax error" ^ get_pos toks)
    24       | err (toks, SOME msg) = (fn () => "SML syntax error" ^ get_pos toks ^ ": " ^ msg ());
    25   in Scan.!! err scan end;
    26 
    27 fun bad_input x =
    28   (Scan.some (fn tok => (case ML_Lex.kind_of tok of ML_Lex.Error msg => SOME msg | _ => NONE)) :|--
    29     (fn msg => Scan.fail_with (K (fn () => msg)))) x;
    30 
    31 
    32 (** basic parsers **)
    33 
    34 fun $$$ x =
    35   Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Keyword andalso ML_Lex.content_of tok = x)
    36     >> ML_Lex.content_of;
    37 
    38 val int = Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Int) >> ML_Lex.content_of;
    39 
    40 val regular = Scan.one ML_Lex.is_regular >> ML_Lex.content_of;
    41 val improper = Scan.one ML_Lex.is_improper >> ML_Lex.content_of;
    42 
    43 val blanks = Scan.repeat improper >> implode;
    44 
    45 
    46 (* fix_ints *)
    47 
    48 (*approximation only -- corrupts numeric record field patterns *)
    49 val fix_int =
    50   $$$ "#" ^^ blanks ^^ int ||
    51   ($$$ "infix" || $$$ "infixr") ^^ blanks ^^ int ||
    52   int >> (fn x => "(" ^ x ^ ":int)") ||
    53   regular ||
    54   bad_input;
    55 
    56 val fix_ints =
    57   ML_System.is_smlnj ?
    58    (Source.of_string #>
    59     ML_Lex.source #>
    60     Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE #>
    61     Source.exhaust #>
    62     implode);
    63 
    64 
    65 (* global use_context *)
    66 
    67 val global_context: use_context =
    68  {tune_source = fix_ints,
    69   name_space = ML_Name_Space.global,
    70   str_of_pos = Position.str_of oo Position.line_file,
    71   print = writeln,
    72   error = error};
    73 
    74 end;