equal
deleted
inserted
replaced
712 |
712 |
713 link.content = inlines |
713 link.content = inlines |
714 |
714 |
715 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ anchor ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
715 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ anchor ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
716 |
716 |
717 anchor = element anchor { anchor.attributes } |
717 anchor = element anchor { anchor.attributes, anchor.content } |
718 |
718 |
719 anchor.attributes = |
719 anchor.attributes = |
720 anchor.id.attribute |
720 anchor.id.attribute |
721 anchor.id.attribute = attribute xml:id { xsd:ID } |
721 anchor.id.attribute = attribute xml:id { xsd:ID } |
|
722 |
|
723 anchor.content = inlines |
722 |
724 |
723 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ initial ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
725 # ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ initial ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
724 |
726 |
725 initial = element initial { initial.content } |
727 initial = element initial { initial.content } |
726 |
728 |