src/Pure/ML/ml_parse.ML
author wenzelm
Thu, 14 Aug 2008 20:13:43 +0200
changeset 27878 1ba19c9edd18
parent 27817 78cae5cca09e
child 29606 fedb8be05f24
permissions -rw-r--r--
report ML_source;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
24594
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML/ml_parse.ML
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     4
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     5
Minimal parsing for SML -- fixing integer numerals.
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     6
*)
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     7
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     8
signature ML_PARSE =
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
     9
sig
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    10
  val fix_ints: string -> string
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    11
end;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    12
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    13
structure ML_Parse: ML_PARSE =
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    14
struct
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    15
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    16
structure T = ML_Lex;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    17
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    18
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    19
(** error handling **)
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    20
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    21
fun !!! scan =
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    22
  let
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    23
    fun get_pos [] = " (past end-of-file!)"
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    24
      | get_pos (tok :: _) = T.pos_of tok;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    25
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    26
    fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    27
      | err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    28
  in Scan.!! err scan end;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    29
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    30
fun bad_input x =
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    31
  (Scan.some (fn tok => (case T.kind_of tok of T.Error msg => SOME msg | _ => NONE)) :|--
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    32
    (fn msg => Scan.fail_with (K msg))) x;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    33
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    34
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    35
(** basic parsers **)
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    36
27817
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 24594
diff changeset
    37
fun $$$ x =
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 24594
diff changeset
    38
  Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.content_of tok = x) >> T.content_of;
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 24594
diff changeset
    39
val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.content_of;
24594
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    40
27817
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 24594
diff changeset
    41
val regular = Scan.one T.is_regular >> T.content_of;
78cae5cca09e renamed ML_Lex.val_of to content_of;
wenzelm
parents: 24594
diff changeset
    42
val improper = Scan.one T.is_improper >> T.content_of;
24594
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    43
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    44
val blanks = Scan.repeat improper >> implode;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    45
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    46
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    47
(* fix_ints *)
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    48
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    49
(*approximation only -- corrupts numeric record field patterns *)
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    50
val fix_int =
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    51
  $$$ "#" ^^ blanks ^^ int ||
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    52
  ($$$ "infix" || $$$ "infixr") ^^ blanks ^^ int ||
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    53
  int >> (fn x => "(" ^ x ^ ":int)") ||
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    54
  regular ||
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    55
  bad_input;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    56
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    57
fun do_fix_ints s =
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    58
  Source.of_string s
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    59
  |> T.source
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    60
  |> Source.source T.stopper (Scan.bulk (!!! fix_int)) NONE
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    61
  |> Source.exhaust
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    62
  |> implode;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    63
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    64
val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    65
6689effe75d1 Minimal parsing for SML -- fixing integer numerals.
wenzelm
parents:
diff changeset
    66
end;