equal
deleted
inserted
replaced
1177 translation functions may depend on the current theory or proof |
1177 translation functions may depend on the current theory or proof |
1178 context. This allows to implement advanced syntax mechanisms, as |
1178 context. This allows to implement advanced syntax mechanisms, as |
1179 translations functions may refer to specific theory declarations or |
1179 translations functions may refer to specific theory declarations or |
1180 auxiliary proof data. |
1180 auxiliary proof data. |
1181 |
1181 |
1182 See also \cite{isabelle-ref} for more information on the general |
|
1183 concept of syntax transformations in Isabelle. |
|
1184 |
|
1185 %FIXME proper antiquotations |
1182 %FIXME proper antiquotations |
1186 \begin{ttbox} |
1183 \begin{ttbox} |
1187 val parse_ast_translation: |
1184 val parse_ast_translation: |
1188 (string * (Proof.context -> ast list -> ast)) list |
1185 (string * (Proof.context -> ast list -> ast)) list |
1189 val parse_translation: |
1186 val parse_translation: |
1193 val typed_print_translation: |
1190 val typed_print_translation: |
1194 (string * (Proof.context -> typ -> term list -> term)) list |
1191 (string * (Proof.context -> typ -> term list -> term)) list |
1195 val print_ast_translation: |
1192 val print_ast_translation: |
1196 (string * (Proof.context -> ast list -> ast)) list |
1193 (string * (Proof.context -> ast list -> ast)) list |
1197 \end{ttbox} |
1194 \end{ttbox} |
|
1195 |
|
1196 \medskip See also the chapter on ``Syntax Transformations'' in old |
|
1197 \cite{isabelle-ref} for further details on translations on parse |
|
1198 trees. |
1198 *} |
1199 *} |
1199 |
1200 |
1200 end |
1201 end |