src/Pure/Thy/export_theory.ML
changeset 68264 bb9a3be6952a
parent 68235 a3bd410db5b2
child 68295 781a98696638
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 24 09:18:29 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu May 24 16:56:14 2018 +0200
     1.3 @@ -27,6 +27,9 @@
     1.4  
     1.5  val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
     1.6    let
     1.7 +    val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
     1.8 +
     1.9 +
    1.10      (* parents *)
    1.11  
    1.12      val parents = Theory.parents_of thy;
    1.13 @@ -76,7 +79,7 @@
    1.14  
    1.15      val _ =
    1.16        export_entities "types" (K export_type) Sign.type_space
    1.17 -        (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))));
    1.18 +        (Name_Space.dest_table (#types rep_tsig));
    1.19  
    1.20  
    1.21      (* consts *)
    1.22 @@ -120,6 +123,24 @@
    1.23        export_entities "facts" (K (SOME o export_fact)) (Facts.space_of o Global_Theory.facts_of)
    1.24          (Facts.dest_static true [] (Global_Theory.facts_of thy));
    1.25  
    1.26 +
    1.27 +    (* type classes *)
    1.28 +
    1.29 +    val encode_class =
    1.30 +      let open XML.Encode Term_XML.Encode
    1.31 +      in pair (list (pair string typ)) (list term) end;
    1.32 +
    1.33 +    fun export_class name =
    1.34 +      (case try (Axclass.get_info thy) name of
    1.35 +        NONE => ([], [])
    1.36 +      | SOME {params, axioms, ...} =>
    1.37 +          (params, map (Logic.unvarify_global o Thm.full_prop_of) axioms))
    1.38 +      |> encode_class |> SOME;
    1.39 +
    1.40 +    val _ =
    1.41 +      export_entities "classes" (fn name => fn () => export_class name)
    1.42 +        Sign.class_space (map (rpair ()) (Graph.keys (Sorts.classes_of (#2 (#classes rep_tsig)))));
    1.43 +
    1.44      in () end);
    1.45  
    1.46  end;