4 Export foundational theory content. |
4 Export foundational theory content. |
5 *) |
5 *) |
6 |
6 |
7 signature EXPORT_THEORY = |
7 signature EXPORT_THEORY = |
8 sig |
8 sig |
|
9 val entity_markup: Name_Space.T -> string -> Markup.T |
9 end; |
10 end; |
10 |
11 |
11 structure Export_Theory: EXPORT_THEORY = |
12 structure Export_Theory: EXPORT_THEORY = |
12 struct |
13 struct |
13 |
14 |
14 (* name space entries *) |
15 (* name space entries *) |
15 |
16 |
|
17 fun entity_markup space name = |
|
18 let |
|
19 val kind = Name_Space.kind_of space; |
|
20 val {serial, pos, ...} = Name_Space.the_entry space name; |
|
21 val props = Markup.serial_properties serial @ Position.properties_of pos; |
|
22 in Markup.properties props (Markup.entity kind name) end; |
|
23 |
16 fun export_decls export_decl parents space decls = |
24 fun export_decls export_decl parents space decls = |
17 (decls, []) |-> fold (fn (name, decl) => |
25 (decls, []) |-> fold (fn (name, decl) => |
18 if exists (fn space => Name_Space.declared space name) parents then I |
26 if exists (fn space => Name_Space.declared space name) parents then I |
19 else |
27 else |
20 (case export_decl decl of |
28 (case export_decl decl of |
21 NONE => I |
29 NONE => I |
22 | SOME body => |
30 | SOME body => cons (name, XML.Elem (entity_markup space name, body)))) |
23 let val markup = Name_Space.markup_def space name |
|
24 in cons (name, XML.Elem (markup, body)) end)) |
|
25 |> sort_by #1 |> map #2; |
31 |> sort_by #1 |> map #2; |
26 |
32 |
27 |
33 |
28 (* present *) |
34 (* present *) |
29 |
35 |