917 def list: List[Chapter_Def] = rev_list.reverse |
917 def list: List[Chapter_Def] = rev_list.reverse |
918 |
918 |
919 override def toString: String = |
919 override def toString: String = |
920 list.map(_.name).mkString("Chapter_Defs(", ", ", ")") |
920 list.map(_.name).mkString("Chapter_Defs(", ", ", ")") |
921 |
921 |
922 private def find(chapter: String): Option[Chapter_Def] = |
922 def get(chapter: String): Option[Chapter_Def] = |
923 rev_list.find(_.name == chapter) |
923 rev_list.find(_.name == chapter) |
924 |
924 |
925 def apply(chapter: String): String = |
925 def + (entry: Chapter_Def): Chapter_Defs = |
926 find(chapter) match { |
926 if (entry.description.isEmpty) this |
927 case None => "" |
|
928 case Some(ch_def) => ch_def.description |
|
929 } |
|
930 |
|
931 def + (ch_def: Chapter_Def): Chapter_Defs = |
|
932 if (ch_def.description.isEmpty) this |
|
933 else { |
927 else { |
934 find(ch_def.name) match { |
928 get(entry.name) match { |
935 case None => new Chapter_Defs(ch_def :: rev_list) |
929 case None => new Chapter_Defs(entry :: rev_list) |
936 case Some(old_def) => |
930 case Some(old_entry) => |
937 error("Duplicate chapter definition " + quote(ch_def.name) + |
931 error("Duplicate chapter definition " + quote(entry.name) + |
938 Position.here(old_def.pos) + Position.here(ch_def.pos)) |
932 Position.here(old_entry.pos) + Position.here(entry.pos)) |
939 } |
933 } |
940 } |
934 } |
941 } |
935 } |
942 |
936 |
943 private object Parsers extends Options.Parsers { |
937 private object Parsers extends Options.Parsers { |