src/Pure/Thy/export_theory.ML
changeset 68862 47e9912c53c3
parent 68830 44ec6fdaacf8
child 68864 1dacce27bc25
     1.1 --- a/src/Pure/Thy/export_theory.ML	Fri Aug 31 13:34:31 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Fri Aug 31 15:48:37 2018 +0200
     1.3 @@ -87,7 +87,6 @@
     1.4                      XML.Elem (entity_markup space name, body))))
     1.5            |> sort (int_ord o apply2 #1) |> map #2
     1.6          end;
     1.7 -
     1.8        in if null elems then () else export_body thy export_name elems end;
     1.9  
    1.10  
    1.11 @@ -196,6 +195,21 @@
    1.12      val _ = if null classrel then () else export_body thy "classrel" (encode_classrel classrel);
    1.13      val _ = if null arities then () else export_body thy "arities" (encode_arities arities);
    1.14  
    1.15 +
    1.16 +    (* locales *)
    1.17 +
    1.18 +    fun encode_locale {type_params, params, asm, defs} =
    1.19 +      (type_params, (map #1 params, (asm, defs))) |>
    1.20 +        let open XML.Encode Term_XML.Encode in
    1.21 +          pair (list (pair string sort))
    1.22 +            (pair (list (pair string typ))
    1.23 +              (pair (option term) (list term)))
    1.24 +        end;
    1.25 +
    1.26 +    val _ =
    1.27 +      export_entities "locales" (fn _ => SOME o encode_locale) Locale.locale_space
    1.28 +        (Locale.dest_locales thy);
    1.29 +
    1.30    in () end);
    1.31  
    1.32  end;