equal
deleted
inserted
replaced
72 Symbol_Pos.!!! "Rail lexical error: bad input" |
72 Symbol_Pos.!!! "Rail lexical error: bad input" |
73 (Scan.ahead (Scan.one Symbol_Pos.is_eof)); |
73 (Scan.ahead (Scan.one Symbol_Pos.is_eof)); |
74 |
74 |
75 in |
75 in |
76 |
76 |
77 fun tokenize text = |
77 val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan) o Symbol_Pos.explode; |
78 #1 (Scan.error (Scan.finite Symbol_Pos.stopper scan) (Symbol_Pos.explode text)); |
|
79 |
78 |
80 end; |
79 end; |
81 |
80 |
82 |
81 |
83 |
82 |
173 val rule = ident -- ($$$ ":" |-- !!! body) || body >> pair ""; |
172 val rule = ident -- ($$$ ":" |-- !!! body) || body >> pair ""; |
174 val rules = enum1 ";" (Scan.option rule) >> map_filter I; |
173 val rules = enum1 ";" (Scan.option rule) >> map_filter I; |
175 |
174 |
176 in |
175 in |
177 |
176 |
178 fun read text = |
177 val read = |
179 (case Scan.error (Scan.finite stopper rules) (tokenize text) of |
178 #1 o Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) o tokenize; |
180 (res, []) => res |
|
181 | (_, tok :: _) => error ("Malformed rail input: " ^ print tok)); |
|
182 |
179 |
183 end; |
180 end; |
184 |
181 |
185 |
182 |
186 (* latex output *) |
183 (* latex output *) |