1467 obscurity in the implementation. |
1467 obscurity in the implementation. |
1468 |
1468 |
1469 @{rail " |
1469 @{rail " |
1470 ( @@{command parse_ast_translation} | @@{command parse_translation} | |
1470 ( @@{command parse_ast_translation} | @@{command parse_translation} | |
1471 @@{command print_translation} | @@{command typed_print_translation} | |
1471 @@{command print_translation} | @@{command typed_print_translation} | |
1472 @@{command print_ast_translation}) ('(' @'advanced' ')')? @{syntax text} |
1472 @@{command print_ast_translation}) @{syntax text} |
1473 ; |
1473 ; |
1474 (@@{ML_antiquotation class_syntax} | |
1474 (@@{ML_antiquotation class_syntax} | |
1475 @@{ML_antiquotation type_syntax} | |
1475 @@{ML_antiquotation type_syntax} | |
1476 @@{ML_antiquotation const_syntax} | |
1476 @@{ML_antiquotation const_syntax} | |
1477 @@{ML_antiquotation syntax_const}) name |
1477 @@{ML_antiquotation syntax_const}) name |
1484 @{syntax text} argument that refers to an ML expression of |
1484 @{syntax text} argument that refers to an ML expression of |
1485 appropriate type, which are as follows by default: |
1485 appropriate type, which are as follows by default: |
1486 |
1486 |
1487 \medskip |
1487 \medskip |
1488 {\footnotesize |
1488 {\footnotesize |
1489 \begin{tabular}{ll} |
1489 \begin{tabular}{l} |
1490 @{command parse_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\ |
1490 @{command parse_ast_translation} : \\ |
1491 @{command parse_translation} & : @{ML_type "(string * (term list -> term)) list"} \\ |
1491 \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\ |
1492 @{command print_translation} & : @{ML_type "(string * (term list -> term)) list"} \\ |
1492 @{command parse_translation} : \\ |
1493 @{command typed_print_translation} & : @{ML_type "(string * (typ -> term list -> term)) list"} \\ |
1493 \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\ |
1494 @{command print_ast_translation} & : @{ML_type "(string * (Ast.ast list -> Ast.ast)) list"} \\ |
1494 @{command print_translation} : \\ |
|
1495 \quad @{ML_type "(string * (Proof.context -> term list -> term)) list"} \\ |
|
1496 @{command typed_print_translation} : \\ |
|
1497 \quad @{ML_type "(string * (Proof.context -> typ -> term list -> term)) list"} \\ |
|
1498 @{command print_ast_translation} : \\ |
|
1499 \quad @{ML_type "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"} \\ |
1495 \end{tabular}} |
1500 \end{tabular}} |
1496 \medskip |
1501 \medskip |
1497 |
1502 |
1498 The argument list consists of @{text "(c, tr)"} pairs, where @{text |
1503 The argument list consists of @{text "(c, tr)"} pairs, where @{text |
1499 "c"} is the syntax name of the formal entity involved, and @{text |
1504 "c"} is the syntax name of the formal entity involved, and @{text |
1500 "tr"} a function that translates a syntax form @{text "c args"} into |
1505 "tr"} a function that translates a syntax form @{text "c args"} into |
1501 @{text "tr args"}. The ML naming convention for parse translations |
1506 @{text "tr ctxt args"} (depending on the context). The ML naming |
1502 is @{text "c_tr"} and for print translations @{text "c_tr'"}. |
1507 convention for parse translations is @{text "c_tr"} and for print |
|
1508 translations @{text "c_tr'"}. |
1503 |
1509 |
1504 The @{command_ref print_syntax} command displays the sets of names |
1510 The @{command_ref print_syntax} command displays the sets of names |
1505 associated with the translation functions of a theory under @{text |
1511 associated with the translation functions of a theory under @{text |
1506 "parse_ast_translation"} etc. |
1512 "parse_ast_translation"} etc. |
1507 |
|
1508 If the @{verbatim "("}@{keyword "advanced"}@{verbatim ")"} option is |
|
1509 given, the corresponding translation functions depend on the current |
|
1510 theory or proof context as additional argument. This allows to |
|
1511 implement advanced syntax mechanisms, as translations functions may |
|
1512 refer to specific theory declarations or auxiliary proof data. |
|
1513 |
1513 |
1514 \item @{text "@{class_syntax c}"}, @{text "@{type_syntax c}"}, |
1514 \item @{text "@{class_syntax c}"}, @{text "@{type_syntax c}"}, |
1515 @{text "@{const_syntax c}"} inline the authentic syntax name of the |
1515 @{text "@{const_syntax c}"} inline the authentic syntax name of the |
1516 given formal entities into the ML source. This is the |
1516 given formal entities into the ML source. This is the |
1517 fully-qualified logical name prefixed by a special marker to |
1517 fully-qualified logical name prefixed by a special marker to |