misc tuning and clarification;
authorwenzelm
Thu May 17 14:01:13 2018 +0200 (12 months ago)
changeset 68201dee993b88a7b
parent 68200 5859c688102a
child 68202 a99180ad3441
misc tuning and clarification;
src/Pure/Thy/export_theory.ML
     1.1 --- a/src/Pure/Thy/export_theory.ML	Thu May 17 07:42:33 2018 +0200
     1.2 +++ b/src/Pure/Thy/export_theory.ML	Thu May 17 14:01:13 2018 +0200
     1.3 @@ -6,90 +6,88 @@
     1.4  
     1.5  signature EXPORT_THEORY =
     1.6  sig
     1.7 +  val setup_presentation: (Thy_Info.presentation_context -> theory -> unit) -> unit
     1.8 +  val export_body: theory -> string -> XML.body -> unit
     1.9  end;
    1.10  
    1.11  structure Export_Theory: EXPORT_THEORY =
    1.12  struct
    1.13  
    1.14 -(* name space entries *)
    1.15 -
    1.16 -fun entity_markup adjust_pos space name =
    1.17 -  let
    1.18 -    val {serial, pos, ...} = Name_Space.the_entry space name;
    1.19 -    val props = Markup.serial_properties serial @ Position.offset_properties_of (adjust_pos pos);
    1.20 -  in (Markup.entityN, (Markup.nameN, name) :: props) end;
    1.21 -
    1.22 -fun export_decls export_decl parents thy adjust_pos 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 thy name decl of
    1.27 -        NONE => I
    1.28 -      | SOME body => cons (name, XML.Elem (entity_markup adjust_pos space name, body))))
    1.29 -  |> sort_by #1 |> map #2;
    1.30 +(* general setup *)
    1.31  
    1.32 -
    1.33 -(* present *)
    1.34 +fun setup_presentation f =
    1.35 +  Theory.setup (Thy_Info.add_presentation (fn context => fn thy =>
    1.36 +    if Options.bool (#options context) "export_theory" then f context thy else ()));
    1.37  
    1.38 -fun present get_space get_decls export name adjust_pos thy =
    1.39 -  if Options.default_bool "export_theory" then
    1.40 -    (case
    1.41 -      export (map get_space (Theory.parents_of thy)) thy adjust_pos (get_space thy) (get_decls thy)
    1.42 -     of
    1.43 -      [] => ()
    1.44 -    | body => Export.export thy ("theory/" ^ name) [YXML.string_of_body body])
    1.45 -  else ();
    1.46 -
    1.47 -fun present_decls get_space get_decls =
    1.48 -  present get_space get_decls o export_decls;
    1.49 -
    1.50 -val setup_presentation = Theory.setup o Thy_Info.add_presentation;
    1.51 +fun export_body thy name body =
    1.52 +  Export.export thy ("theory/" ^ name) [YXML.string_of_body body];
    1.53  
    1.54  
    1.55 -(* types *)
    1.56 +(* presentation *)
    1.57 +
    1.58 +val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
    1.59 +  let
    1.60 +    (* entities *)
    1.61  
    1.62 -local
    1.63 -
    1.64 -val present_types =
    1.65 -  present_decls Sign.type_space (Name_Space.dest_table o #types o Type.rep_tsig o Sign.tsig_of);
    1.66 +    fun entity_markup space name =
    1.67 +      let
    1.68 +        val {serial, pos, ...} = Name_Space.the_entry space name;
    1.69 +        val props =
    1.70 +          Markup.serial_properties serial @
    1.71 +          Position.offset_properties_of (adjust_pos pos);
    1.72 +      in (Markup.entityN, (Markup.nameN, name) :: props) end;
    1.73  
    1.74 -val encode_type =
    1.75 -  let open XML.Encode Term_XML.Encode
    1.76 -  in pair (list string) (option typ) end;
    1.77 -
    1.78 -fun export_type (Type.LogicalType n) = SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
    1.79 -  | export_type (Type.Abbreviation (args, U, false)) = SOME (encode_type (args, SOME U))
    1.80 -  | export_type _ = NONE;
    1.81 -
    1.82 -in
    1.83 -
    1.84 -val _ = setup_presentation (present_types (K (K export_type)) "types" o #adjust_pos);
    1.85 -
    1.86 -end;
    1.87 +    fun export_entities export_name export get_space decls =
    1.88 +      let val elems =
    1.89 +        let
    1.90 +          val parent_spaces = map get_space (Theory.parents_of thy);
    1.91 +          val space = get_space thy;
    1.92 +        in
    1.93 +          (decls, []) |-> fold (fn (name, decl) =>
    1.94 +            if exists (fn space => Name_Space.declared space name) parent_spaces then I
    1.95 +            else
    1.96 +              (case export name decl of
    1.97 +                NONE => I
    1.98 +              | SOME body => cons (name, XML.Elem (entity_markup space name, body))))
    1.99 +          |> sort_by #1 |> map #2
   1.100 +        end;
   1.101 +      in if null elems then () else export_body thy export_name elems end;
   1.102  
   1.103  
   1.104 -(* consts *)
   1.105 +    (* types *)
   1.106  
   1.107 -local
   1.108 +    val encode_type =
   1.109 +      let open XML.Encode Term_XML.Encode
   1.110 +      in pair (list string) (option typ) end;
   1.111  
   1.112 -val present_consts =
   1.113 -  present_decls Sign.const_space (#constants o Consts.dest o Sign.consts_of);
   1.114 +    fun export_type (Type.LogicalType n) =
   1.115 +          SOME (encode_type (Name.invent Name.context Name.aT n, NONE))
   1.116 +      | export_type (Type.Abbreviation (args, U, false)) =
   1.117 +          SOME (encode_type (args, SOME U))
   1.118 +      | export_type _ = NONE;
   1.119  
   1.120 -val encode_const =
   1.121 -  let open XML.Encode Term_XML.Encode
   1.122 -  in triple (list string) typ (option term) end;
   1.123 +    val _ =
   1.124 +      export_entities "types" (K export_type) Sign.type_space
   1.125 +        (Name_Space.dest_table (#types (Type.rep_tsig (Sign.tsig_of thy))));
   1.126 +
   1.127  
   1.128 -fun export_const thy c (T, abbrev) =
   1.129 -  let
   1.130 -    val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
   1.131 -    val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
   1.132 -    val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
   1.133 -  in SOME (encode_const (args, T', abbrev')) end;
   1.134 +    (* consts *)
   1.135 +
   1.136 +    val encode_const =
   1.137 +      let open XML.Encode Term_XML.Encode
   1.138 +      in triple (list string) typ (option term) end;
   1.139  
   1.140 -in
   1.141 +    fun export_const c (T, abbrev) =
   1.142 +      let
   1.143 +        val T' = T |> Logic.unvarifyT_global |> Type.strip_sorts;
   1.144 +        val abbrev' = abbrev |> Option.map (Logic.unvarify_global #> map_types Type.strip_sorts);
   1.145 +        val args = map (#1 o dest_TFree) (Consts.typargs (Sign.consts_of thy) (c, T'));
   1.146 +      in SOME (encode_const (args, T', abbrev')) end;
   1.147  
   1.148 -val _ = setup_presentation (present_consts export_const "consts" o #adjust_pos);
   1.149 +    val _ =
   1.150 +      export_entities "consts" export_const Sign.const_space
   1.151 +        (#constants (Consts.dest (Sign.consts_of thy)));
   1.152 +
   1.153 +    in () end);
   1.154  
   1.155  end;
   1.156 -
   1.157 -end;