equal
deleted
inserted
replaced
201 def cartouche: Parser[String] = |
201 def cartouche: Parser[String] = |
202 cartouche_depth(0) ^? { case (x, d) if d == 0 => x } |
202 cartouche_depth(0) ^? { case (x, d) if d == 0 => x } |
203 |
203 |
204 def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] = |
204 def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] = |
205 { |
205 { |
206 val depth = |
206 def cartouche_context(d: Int): Line_Context = |
207 ctxt match { |
207 if (d == 0) Finished else Cartouche(d) |
208 case Finished => 0 |
208 |
209 case Cartouche(d) => d |
209 ctxt match { |
210 case _ => -1 |
210 case Finished => |
211 } |
211 cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) } |
212 if (depth >= 0) |
212 case Cartouche(depth) => |
213 cartouche_depth(depth) ^^ |
213 cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) } |
214 { case (x, 0) => (x, Finished) |
214 case _ => failure("") |
215 case (x, d) => (x, Cartouche(d)) } |
215 } |
216 else failure("") |
|
217 } |
216 } |
218 |
217 |
219 val recover_cartouche: Parser[String] = |
218 val recover_cartouche: Parser[String] = |
220 cartouche_depth(0) ^^ (_._1) |
219 cartouche_depth(0) ^^ (_._1) |
221 |
220 |