doc-src/IsarRef/Thy/Inner_Syntax.thy
changeset 46294 f9a1cd2599dd
parent 46293 f248b5f2783a
child 46483 10a9c31a22b4
equal deleted inserted replaced
46293:f248b5f2783a 46294:f9a1cd2599dd
  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