more exports;
authorwenzelm
Sun May 13 15:55:30 2018 +0200 (12 months ago)
changeset 68165a7a2174ac014
parent 68164 738071699826
child 68166 021c6fecaf5c
more exports;
misc tuning and clarification;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Sun May 13 15:05:31 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Sun May 13 15:55:30 2018 +0200
     1.3 @@ -6,56 +6,77 @@
     1.4  
     1.5  signature EXPORT_THEORY =
     1.6  sig
     1.7 -  val export_table_diff: ('a -> XML.tree list option) ->
     1.8 -    'a Name_Space.table list -> 'a Name_Space.table -> XML.tree list
     1.9  end;
    1.10  
    1.11  structure Export_Theory: EXPORT_THEORY =
    1.12  struct
    1.13  
    1.14 -(* export namespace table *)
    1.15 +(* name space entries *)
    1.16  
    1.17 -fun export_table_diff export_decl prev_tables table =
    1.18 -  (table, []) |-> Name_Space.fold_table (fn (name, decl) =>
    1.19 -    if exists (fn prev => Name_Space.defined prev name) prev_tables then I
    1.20 +fun export_decls export_decl parents space decls =
    1.21 +  (decls, []) |-> fold (fn (name, decl) =>
    1.22 +    if exists (fn space => Name_Space.declared space name) parents then I
    1.23      else
    1.24        (case export_decl decl of
    1.25          NONE => I
    1.26        | SOME body =>
    1.27 -          let val markup = Name_Space.markup_def (Name_Space.space_of_table table) name
    1.28 +          let val markup = Name_Space.markup_def space name
    1.29            in cons (name, XML.Elem (markup, body)) end))
    1.30    |> sort_by #1 |> map #2;
    1.31  
    1.32  
    1.33  (* present *)
    1.34  
    1.35 -fun present get export name thy =
    1.36 +fun present get_space get_decls export name thy =
    1.37    if Options.default_bool "export_theory" then
    1.38 -    (case export (map get (Theory.parents_of thy)) (get thy) of
    1.39 +    (case export (map get_space (Theory.parents_of thy)) (get_space thy) (get_decls thy) of
    1.40        [] => ()
    1.41      | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
    1.42    else ();
    1.43  
    1.44 +fun present_decls get_space get_decls =
    1.45 +  present get_space get_decls o export_decls;
    1.46 +
    1.47 +val setup_presentation = Theory.setup o Thy_Info.add_presentation;
    1.48 +
    1.49  
    1.50  (* types *)
    1.51  
    1.52 -val present_types = present (#types o Type.rep_tsig o Sign.tsig_of) o export_table_diff;
    1.53 +local
    1.54  
    1.55 -fun export_logical_type (Type.LogicalType n) = SOME (XML.Encode.int n)
    1.56 -  | export_logical_type _ = NONE;
    1.57 +val present_types =
    1.58 +  present_decls Sign.type_space (Name_Space.dest_table o #types o Type.rep_tsig o Sign.tsig_of);
    1.59  
    1.60 -fun export_abbreviation (Type.Abbreviation (vs, U, _)) =
    1.61 -      let open XML.Encode Term_XML.Encode
    1.62 -      in SOME (pair (list string) typ (vs, U)) end
    1.63 -  | export_abbreviation _ = NONE;
    1.64 +val encode_type =
    1.65 +  let open XML.Encode Term_XML.Encode
    1.66 +  in pair (list string) (option typ) end;
    1.67  
    1.68 -fun export_nonterminal Type.Nonterminal = SOME []
    1.69 -  | export_nonterminal _ = NONE;
    1.70 +fun export_type (Type.LogicalType n) = SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
    1.71 +  | export_type (Type.Abbreviation (args, U, false)) = SOME (encode_type (args, SOME U))
    1.72 +  | export_type _ = NONE;
    1.73  
    1.74 -val _ =
    1.75 -  Theory.setup
    1.76 -    (Thy_Info.add_presentation (present_types export_logical_type "types") #>
    1.77 -     Thy_Info.add_presentation (present_types export_abbreviation "type_synonyms") #>
    1.78 -     Thy_Info.add_presentation (present_types export_nonterminal "nonterminals"));
    1.79 +in
    1.80 +
    1.81 +val _ = setup_presentation (present_types export_type "types");
    1.82  
    1.83  end;
    1.84 +
    1.85 +
    1.86 +(* consts *)
    1.87 +
    1.88 +local
    1.89 +
    1.90 +val present_consts =
    1.91 +  present_decls Sign.const_space (#constants o Consts.dest o Sign.consts_of);
    1.92 +
    1.93 +val encode_const =
    1.94 +  let open XML.Encode Term_XML.Encode
    1.95 +  in pair typ (option term) end;
    1.96 +
    1.97 +in
    1.98 +
    1.99 +val _ = setup_presentation (present_consts (SOME o encode_const) "consts");
   1.100 +
   1.101 +end;
   1.102 +
   1.103 +end;