doc-src/IsarRef/Thy/document/Inner_Syntax.tex
changeset 46294 f9a1cd2599dd
parent 46293 f248b5f2783a
child 46483 10a9c31a22b4
equal deleted inserted replaced
46293:f248b5f2783a 46294:f9a1cd2599dd
  1424   translation functions may depend on the current theory or proof
  1424   translation functions may depend on the current theory or proof
  1425   context.  This allows to implement advanced syntax mechanisms, as
  1425   context.  This allows to implement advanced syntax mechanisms, as
  1426   translations functions may refer to specific theory declarations or
  1426   translations functions may refer to specific theory declarations or
  1427   auxiliary proof data.
  1427   auxiliary proof data.
  1428 
  1428 
  1429   See also \cite{isabelle-ref} for more information on the general
       
  1430   concept of syntax transformations in Isabelle.
       
  1431 
       
  1432 %FIXME proper antiquotations
  1429 %FIXME proper antiquotations
  1433 \begin{ttbox}
  1430 \begin{ttbox}
  1434 val parse_ast_translation:
  1431 val parse_ast_translation:
  1435   (string * (Proof.context -> ast list -> ast)) list
  1432   (string * (Proof.context -> ast list -> ast)) list
  1436 val parse_translation:
  1433 val parse_translation:
  1439   (string * (Proof.context -> term list -> term)) list
  1436   (string * (Proof.context -> term list -> term)) list
  1440 val typed_print_translation:
  1437 val typed_print_translation:
  1441   (string * (Proof.context -> typ -> term list -> term)) list
  1438   (string * (Proof.context -> typ -> term list -> term)) list
  1442 val print_ast_translation:
  1439 val print_ast_translation:
  1443   (string * (Proof.context -> ast list -> ast)) list
  1440   (string * (Proof.context -> ast list -> ast)) list
  1444 \end{ttbox}%
  1441 \end{ttbox}
       
  1442 
       
  1443   \medskip See also the chapter on ``Syntax Transformations'' in old
       
  1444   \cite{isabelle-ref} for further details on translations on parse
       
  1445   trees.%
  1445 \end{isamarkuptext}%
  1446 \end{isamarkuptext}%
  1446 \isamarkuptrue%
  1447 \isamarkuptrue%
  1447 %
  1448 %
  1448 \isadelimtheory
  1449 \isadelimtheory
  1449 %
  1450 %