adapted to new scanner and abroque chars;
authorwenzelm
Mon Mar 09 16:11:50 1998 +0100 (1998-03-09)
changeset 4701be8a8d60d962
parent 4700 20ade76722d6
child 4702 ffbaf431665d
adapted to new scanner and abroque chars;
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon Mar 09 16:11:28 1998 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Mar 09 16:11:50 1998 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4    datatype xprod = XProd of string * xsymb list * string * int
     1.5    val max_pri: int
     1.6    val chain_pri: int
     1.7 -  val delims_of: xprod list -> string list
     1.8 +  val delims_of: xprod list -> string list list
     1.9    datatype mfix = Mfix of string * typ * string * int list * int
    1.10    datatype syn_ext =
    1.11      SynExt of {
    1.12 @@ -137,7 +137,7 @@
    1.13      fun dels_of (XProd (_, xsymbs, _, _)) =
    1.14        mapfilter del_of xsymbs;
    1.15    in
    1.16 -    distinct (flat (map dels_of xprods))
    1.17 +    map Symbol.explode (distinct (flat (map dels_of xprods)))
    1.18    end;
    1.19  
    1.20  
    1.21 @@ -166,38 +166,36 @@
    1.22  val typ_to_nonterm1 = typ_to_nt logic;
    1.23  
    1.24  
    1.25 -(* scan_mixfix, mixfix_args *)
    1.26 +(* read_mixfix, mfix_args *)
    1.27  
    1.28  local
    1.29    fun is_meta c = c mem ["(", ")", "/", "_"];
    1.30  
    1.31 -  fun scan_delim_char ("'" :: c :: cs) =
    1.32 -        if is_blank c then raise LEXICAL_ERROR else (c, cs)
    1.33 -    | scan_delim_char ["'"] = error "Trailing escape character"
    1.34 -    | scan_delim_char (chs as c :: cs) =
    1.35 -        if is_blank c orelse is_meta c then raise LEXICAL_ERROR else (c, cs)
    1.36 -    | scan_delim_char [] = raise LEXICAL_ERROR;
    1.37 +  val scan_delim_char =
    1.38 +    $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
    1.39 +    Scan.one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof);
    1.40  
    1.41    val scan_sym =
    1.42      $$ "_" >> K (Argument ("", 0)) ||
    1.43 -    $$ "(" -- Term.scan_int >> (Bg o #2) ||
    1.44 +    $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o #1 o Term.read_int) ||
    1.45      $$ ")" >> K En ||
    1.46      $$ "/" -- $$ "/" >> K (Brk ~1) ||
    1.47 -    $$ "/" -- scan_any is_blank >> (Brk o length o #2) ||
    1.48 -    scan_any1 is_blank >> (Space o implode) ||
    1.49 -    repeat1 scan_delim_char >> (Delim o implode);
    1.50 +    $$ "/" |-- Scan.any Symbol.is_blank >> (Brk o length) ||
    1.51 +    Scan.any1 Symbol.is_blank >> (Space o implode) ||
    1.52 +    Scan.repeat1 scan_delim_char >> (Delim o implode);
    1.53  
    1.54    val scan_symb =
    1.55      scan_sym >> Some ||
    1.56 -    $$ "'" -- scan_one is_blank >> K None;
    1.57 +    $$ "'" -- Scan.one Symbol.is_blank >> K None;
    1.58  
    1.59 -  val scan_symbs = mapfilter I o #1 o repeat scan_symb;
    1.60 +  val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
    1.61 +  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.eof scan_symbs);
    1.62  in
    1.63 -  val scan_mixfix = scan_symbs o SymbolFont.read_charnames o explode;
    1.64 +  val read_mixfix = read_symbs o Symbol.explode;
    1.65  end;
    1.66  
    1.67  fun mfix_args sy =
    1.68 -  foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, scan_mixfix sy);
    1.69 +  foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, read_mixfix sy);
    1.70  
    1.71  
    1.72  (* mfix_to_xprod *)
    1.73 @@ -255,7 +253,7 @@
    1.74        | logify_types _ a = a;
    1.75  
    1.76  
    1.77 -    val raw_symbs = scan_mixfix sy handle ERROR => err "";
    1.78 +    val raw_symbs = read_mixfix sy handle ERROR => err "";
    1.79      val (symbs, lhs) = add_args raw_symbs typ pris;
    1.80      val copy_prod =
    1.81        lhs mem ["prop", "logic"]