src/Pure/Syntax/syn_ext.ML
changeset 19004 a72c7a1eb129
parent 18977 f24c416a4814
child 19012 2577ac76cdc6
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Feb 10 02:22:52 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Feb 10 02:22:54 2006 +0100
     1.3 @@ -53,6 +53,7 @@
     1.4        print_ast_translation:
     1.5          (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
     1.6        token_translation: (string * string * (string -> string * real)) list}
     1.7 +  val mfix_delims: string -> string list
     1.8    val mfix_args: string -> int
     1.9    val escape_mfix: string -> string
    1.10    val unlocalize_mfix: string -> string
    1.11 @@ -155,19 +156,10 @@
    1.12  val max_pri = 1000;   (*maximum legal priority*)
    1.13  val chain_pri = ~1;   (*dummy for chain productions*)
    1.14  
    1.15 -
    1.16 -(* delims_of *)
    1.17 -
    1.18  fun delims_of xprods =
    1.19 -  let
    1.20 -    fun del_of (Delim s) = SOME s
    1.21 -      | del_of _ = NONE;
    1.22 -
    1.23 -    fun dels_of (XProd (_, xsymbs, _, _)) =
    1.24 -      List.mapPartial del_of xsymbs;
    1.25 -  in
    1.26 -    map Symbol.explode (gen_distinct (op =) (List.concat (map dels_of xprods)))
    1.27 -  end;
    1.28 +  fold (fn XProd (_, xsymbs, _, _) =>
    1.29 +    fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
    1.30 +  |> map Symbol.explode;
    1.31  
    1.32  
    1.33  
    1.34 @@ -198,42 +190,49 @@
    1.35  val typ_to_nonterm1 = typ_to_nt logic;
    1.36  
    1.37  
    1.38 -(* read_mixfix *)
    1.39 +(* read mixfix annotations *)
    1.40  
    1.41  local
    1.42 -  fun is_meta c = c mem ["(", ")", "/", "_", "\\<index>"];
    1.43 +
    1.44 +fun is_meta c = c mem ["(", ")", "/", "_", "\\<index>"];
    1.45 +
    1.46 +val scan_delim_char =
    1.47 +  $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
    1.48 +  Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
    1.49 +
    1.50 +fun read_int ["0", "0"] = ~1
    1.51 +  | read_int cs = #1 (Library.read_int cs);
    1.52  
    1.53 -  val scan_delim_char =
    1.54 -    $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
    1.55 -    Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
    1.56 -
    1.57 -  fun read_int ["0", "0"] = ~1
    1.58 -    | read_int cs = #1 (Library.read_int cs);
    1.59 +val scan_sym =
    1.60 +  $$ "_" >> K (Argument ("", 0)) ||
    1.61 +  $$ "\\<index>" >> K index ||
    1.62 +  $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
    1.63 +  $$ ")" >> K En ||
    1.64 +  $$ "/" -- $$ "/" >> K (Brk ~1) ||
    1.65 +  $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
    1.66 +  Scan.any1 Symbol.is_blank >> (Space o implode) ||
    1.67 +  Scan.repeat1 scan_delim_char >> (Delim o implode);
    1.68  
    1.69 -  val scan_sym =
    1.70 -    $$ "_" >> K (Argument ("", 0)) ||
    1.71 -    $$ "\\<index>" >> K index ||
    1.72 -    $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o read_int) ||
    1.73 -    $$ ")" >> K En ||
    1.74 -    $$ "/" -- $$ "/" >> K (Brk ~1) ||
    1.75 -    $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
    1.76 -    Scan.any1 Symbol.is_blank >> (Space o implode) ||
    1.77 -    Scan.repeat1 scan_delim_char >> (Delim o implode);
    1.78 +val scan_symb =
    1.79 +  scan_sym >> SOME ||
    1.80 +  $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
    1.81 +
    1.82 +val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
    1.83 +val read_symbs = List.mapPartial I o the o Scan.read Symbol.stopper scan_symbs;
    1.84  
    1.85 -  val scan_symb =
    1.86 -    scan_sym >> SOME ||
    1.87 -    $$ "'" -- Scan.one Symbol.is_blank >> K NONE;
    1.88 +fun unique_index xsymbs =
    1.89 +  if length (List.filter is_index xsymbs) <= 1 then xsymbs
    1.90 +  else error "Duplicate index arguments (\\<index>)";
    1.91  
    1.92 -  val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
    1.93 -  val read_symbs = List.mapPartial I o the o Scan.read Symbol.stopper scan_symbs;
    1.94 +in
    1.95  
    1.96 -  fun unique_index xsymbs =
    1.97 -    if length (List.filter is_index xsymbs) <= 1 then xsymbs
    1.98 -    else error "Duplicate index arguments (\\<index>)";
    1.99 -in
   1.100 -  val read_mixfix = unique_index o read_symbs o Symbol.explode;
   1.101 -  val mfix_args = length o List.filter is_argument o read_mixfix;
   1.102 -  val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
   1.103 +val read_mfix = unique_index o read_symbs o Symbol.explode;
   1.104 +
   1.105 +fun mfix_delims sy = fold_rev (fn Delim s => cons s | _ => I) (read_mfix sy) [];
   1.106 +val mfix_args = length o List.filter is_argument o read_mfix;
   1.107 +
   1.108 +val escape_mfix = implode o map (fn s => if is_meta s then "'" ^ s else s) o Symbol.explode;
   1.109 +
   1.110  end;
   1.111  
   1.112  val unlocalize_mfix =
   1.113 @@ -287,7 +286,7 @@
   1.114        | logify_types _ a = a;
   1.115  
   1.116  
   1.117 -    val raw_symbs = read_mixfix sy handle ERROR msg => err_in_mfix msg mfix;
   1.118 +    val raw_symbs = read_mfix sy handle ERROR msg => err_in_mfix msg mfix;
   1.119      val args = List.filter (fn Argument _ => true | _ => false) raw_symbs;
   1.120      val (const', typ', parse_rules) =
   1.121        if not (exists is_index args) then (const, typ, [])