clarified markup;
authorwenzelm
Sun May 13 16:51:50 2018 +0200 (12 months ago)
changeset 681707e1daf6f2578
parent 68169 395432e7516e
child 68171 13162bb3a677
clarified markup;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 13 16:37:36 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 13 16:51:50 2018 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature EXPORT_THEORY =
     1.6  sig
     1.7 +  val entity_markup: Name_Space.T -> string -> Markup.T
     1.8  end;
     1.9  
    1.10  structure Export_Theory: EXPORT_THEORY =
    1.11 @@ -13,15 +14,20 @@
    1.12  
    1.13  (* name space entries *)
    1.14  
    1.15 +fun entity_markup space name =
    1.16 +  let
    1.17 +    val kind = Name_Space.kind_of space;
    1.18 +    val {serial, pos, ...} = Name_Space.the_entry space name;
    1.19 +    val props = Markup.serial_properties serial @ Position.properties_of pos;
    1.20 +  in Markup.properties props (Markup.entity kind name) end;
    1.21 +
    1.22  fun export_decls export_decl parents space decls =
    1.23    (decls, []) |-> fold (fn (name, decl) =>
    1.24      if exists (fn space => Name_Space.declared space name) parents then I
    1.25      else
    1.26        (case export_decl decl of
    1.27          NONE => I
    1.28 -      | SOME body =>
    1.29 -          let val markup = Name_Space.markup_def space name
    1.30 -          in cons (name, XML.Elem (markup, body)) end))
    1.31 +      | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
    1.32    |> sort_by #1 |> map #2;
    1.33  
    1.34