equal
deleted
inserted
replaced
64 |
64 |
65 fun entity_markup space name = |
65 fun entity_markup space name = |
66 let |
66 let |
67 val {serial, pos, ...} = Name_Space.the_entry space name; |
67 val {serial, pos, ...} = Name_Space.the_entry space name; |
68 val props = |
68 val props = |
69 Markup.serial_properties serial @ |
69 Position.offset_properties_of (adjust_pos pos) @ |
70 Position.offset_properties_of (adjust_pos pos); |
70 Position.id_properties_of pos @ |
|
71 Markup.serial_properties serial; |
71 in (Markup.entityN, (Markup.nameN, name) :: props) end; |
72 in (Markup.entityN, (Markup.nameN, name) :: props) end; |
72 |
73 |
73 fun export_entities export_name export get_space decls = |
74 fun export_entities export_name export get_space decls = |
74 let val elems = |
75 let val elems = |
75 let |
76 let |