58 |
58 |
59 (* generic setup *) |
59 (* generic setup *) |
60 |
60 |
61 fun global_setup source = |
61 fun global_setup source = |
62 ML_Lex.read_source false source |
62 ML_Lex.read_source false source |
63 |> ML_Context.expression (#range source) |
63 |> ML_Context.expression (#range source) "setup" "theory -> theory" |
64 "val setup: theory -> theory" "Context.map_theory setup" |
64 "Context.map_theory setup" |
65 |> Context.theory_map; |
65 |> Context.theory_map; |
66 |
66 |
67 fun local_setup source = |
67 fun local_setup source = |
68 ML_Lex.read_source false source |
68 ML_Lex.read_source false source |
69 |> ML_Context.expression (#range source) |
69 |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory" |
70 "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup" |
70 "Context.map_proof local_setup" |
71 |> Context.proof_map; |
71 |> Context.proof_map; |
72 |
72 |
73 |
73 |
74 (* translation functions *) |
74 (* translation functions *) |
75 |
75 |
76 fun parse_ast_translation source = |
76 fun parse_ast_translation source = |
77 ML_Lex.read_source false source |
77 ML_Lex.read_source false source |
78 |> ML_Context.expression (#range source) |
78 |> ML_Context.expression (#range source) "parse_ast_translation" |
79 "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list" |
79 "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list" |
80 "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)" |
80 "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)" |
81 |> Context.theory_map; |
81 |> Context.theory_map; |
82 |
82 |
83 fun parse_translation source = |
83 fun parse_translation source = |
84 ML_Lex.read_source false source |
84 ML_Lex.read_source false source |
85 |> ML_Context.expression (#range source) |
85 |> ML_Context.expression (#range source) "parse_translation" |
86 "val parse_translation: (string * (Proof.context -> term list -> term)) list" |
86 "(string * (Proof.context -> term list -> term)) list" |
87 "Context.map_theory (Sign.parse_translation parse_translation)" |
87 "Context.map_theory (Sign.parse_translation parse_translation)" |
88 |> Context.theory_map; |
88 |> Context.theory_map; |
89 |
89 |
90 fun print_translation source = |
90 fun print_translation source = |
91 ML_Lex.read_source false source |
91 ML_Lex.read_source false source |
92 |> ML_Context.expression (#range source) |
92 |> ML_Context.expression (#range source) "print_translation" |
93 "val print_translation: (string * (Proof.context -> term list -> term)) list" |
93 "(string * (Proof.context -> term list -> term)) list" |
94 "Context.map_theory (Sign.print_translation print_translation)" |
94 "Context.map_theory (Sign.print_translation print_translation)" |
95 |> Context.theory_map; |
95 |> Context.theory_map; |
96 |
96 |
97 fun typed_print_translation source = |
97 fun typed_print_translation source = |
98 ML_Lex.read_source false source |
98 ML_Lex.read_source false source |
99 |> ML_Context.expression (#range source) |
99 |> ML_Context.expression (#range source) "typed_print_translation" |
100 "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list" |
100 "(string * (Proof.context -> typ -> term list -> term)) list" |
101 "Context.map_theory (Sign.typed_print_translation typed_print_translation)" |
101 "Context.map_theory (Sign.typed_print_translation typed_print_translation)" |
102 |> Context.theory_map; |
102 |> Context.theory_map; |
103 |
103 |
104 fun print_ast_translation source = |
104 fun print_ast_translation source = |
105 ML_Lex.read_source false source |
105 ML_Lex.read_source false source |
106 |> ML_Context.expression (#range source) |
106 |> ML_Context.expression (#range source) "print_ast_translation" |
107 "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list" |
107 "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list" |
108 "Context.map_theory (Sign.print_ast_translation print_ast_translation)" |
108 "Context.map_theory (Sign.print_ast_translation print_ast_translation)" |
109 |> Context.theory_map; |
109 |> Context.theory_map; |
110 |
110 |
111 |
111 |
112 (* translation rules *) |
112 (* translation rules *) |
158 |
158 |
159 (* declarations *) |
159 (* declarations *) |
160 |
160 |
161 fun declaration {syntax, pervasive} source = |
161 fun declaration {syntax, pervasive} source = |
162 ML_Lex.read_source false source |
162 ML_Lex.read_source false source |
163 |> ML_Context.expression (#range source) |
163 |> ML_Context.expression (#range source) "declaration" "Morphism.declaration" |
164 "val declaration: Morphism.declaration" |
|
165 ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \ |
164 ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \ |
166 \pervasive = " ^ Bool.toString pervasive ^ "} declaration)") |
165 \pervasive = " ^ Bool.toString pervasive ^ "} declaration)") |
167 |> Context.proof_map; |
166 |> Context.proof_map; |
168 |
167 |
169 |
168 |
170 (* simprocs *) |
169 (* simprocs *) |
171 |
170 |
172 fun simproc_setup name lhss source identifier = |
171 fun simproc_setup name lhss source identifier = |
173 ML_Lex.read_source false source |
172 ML_Lex.read_source false source |
174 |> ML_Context.expression (#range source) |
173 |> ML_Context.expression (#range source) "proc" |
175 "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option" |
174 "Morphism.morphism -> Proof.context -> cterm -> thm option" |
176 ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \ |
175 ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \ |
177 \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ |
176 \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \ |
178 \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") |
177 \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})") |
179 |> Context.proof_map; |
178 |> Context.proof_map; |
180 |
179 |