tuned;
authorwenzelm
Sat Apr 30 20:58:36 2011 +0200 (2011-04-30)
changeset 42507651aef3cc854
parent 42506 876887b07e8d
child 42508 e21362bf1d93
tuned;
src/Pure/Thy/rail.ML
     1.1 --- a/src/Pure/Thy/rail.ML	Sat Apr 30 20:48:29 2011 +0200
     1.2 +++ b/src/Pure/Thy/rail.ML	Sat Apr 30 20:58:36 2011 +0200
     1.3 @@ -74,8 +74,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun tokenize text =
     1.8 -  #1 (Scan.error (Scan.finite Symbol_Pos.stopper scan) (Symbol_Pos.explode text));
     1.9 +val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan) o Symbol_Pos.explode;
    1.10  
    1.11  end;
    1.12  
    1.13 @@ -175,10 +174,8 @@
    1.14  
    1.15  in
    1.16  
    1.17 -fun read text =
    1.18 -  (case Scan.error (Scan.finite stopper rules) (tokenize text) of
    1.19 -    (res, []) => res
    1.20 -  | (_, tok :: _) => error ("Malformed rail input: " ^ print tok));
    1.21 +val read =
    1.22 +  #1 o Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) o tokenize;
    1.23  
    1.24  end;
    1.25