equal
deleted
inserted
replaced
73 |
73 |
74 fun message_pos ts = get_first get_pos ts |
74 fun message_pos ts = get_first get_pos ts |
75 and get_pos (elem as XML.Elem (name, atts, ts)) = |
75 and get_pos (elem as XML.Elem (name, atts, ts)) = |
76 if name = Markup.positionN then SOME (Position.of_properties atts) |
76 if name = Markup.positionN then SOME (Position.of_properties atts) |
77 else message_pos ts |
77 else message_pos ts |
78 | get_pos _ = NONE |
78 | get_pos _ = NONE; |
79 |
79 |
80 in |
80 in |
81 |
81 |
82 fun message ch body = |
82 fun message ch body = |
83 let |
83 let |