equal
deleted
inserted
replaced
451 } |
451 } |
452 } |
452 } |
453 |
453 |
454 def get(lines: List[String]): List[String] = |
454 def get(lines: List[String]): List[String] = |
455 unapply(lines) getOrElse |
455 unapply(lines) getOrElse |
456 error("Missing delimiters:" + |
456 error("Missing delimiters:" + if_proper(bg, " ") + bg + if_proper(en, " ") + en) |
457 (if (bg.nonEmpty) " " else "") + bg + |
|
458 (if (en.nonEmpty) " " else "") + en) |
|
459 } |
457 } |
460 |
458 |
461 |
459 |
462 /* isabelle-users mailing list */ |
460 /* isabelle-users mailing list */ |
463 |
461 |