Scan.read;
authorwenzelm
Mon Nov 16 10:41:27 1998 +0100 (1998-11-16)
changeset 58705d4fc952be47
parent 5869 b279a84ac11c
child 5871 2c037ffa7287
Scan.read;
src/Pure/Syntax/symbol.ML
src/Pure/Syntax/syn_ext.ML
     1.1 --- a/src/Pure/Syntax/symbol.ML	Mon Nov 16 10:41:08 1998 +0100
     1.2 +++ b/src/Pure/Syntax/symbol.ML	Mon Nov 16 10:41:27 1998 +0100
     1.3 @@ -244,7 +244,7 @@
     1.4  fun sym_explode str =
     1.5    let val chs = explode str in
     1.6      if no_syms chs then chs     (*tune trivial case*)
     1.7 -    else map symbol (#1 (Scan.error (Scan.finite stopper (Scan.repeat scan)) chs))
     1.8 +    else map symbol (the (Scan.read stopper (Scan.repeat scan) chs))
     1.9    end;
    1.10  
    1.11  
     2.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon Nov 16 10:41:08 1998 +0100
     2.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Nov 16 10:41:27 1998 +0100
     2.3 @@ -187,7 +187,7 @@
     2.4      $$ "'" -- Scan.one Symbol.is_blank >> K None;
     2.5  
     2.6    val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
     2.7 -  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.stopper scan_symbs);
     2.8 +  val read_symbs = mapfilter I o the o Scan.read Symbol.stopper scan_symbs;
     2.9  in
    2.10    val read_mixfix = read_symbs o Symbol.explode;
    2.11  end;