1451 @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1451 @{command_def "parse_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1452 @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1452 @{command_def "parse_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1453 @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1453 @{command_def "print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1454 @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1454 @{command_def "typed_print_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1455 @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1455 @{command_def "print_ast_translation"} & : & @{text "theory \<rightarrow> theory"} \\ |
1456 @{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\ |
1456 @{ML_antiquotation_def "class_syntax"} & : & @{text "ML antiquotation"} \\ |
1457 @{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\ |
1457 @{ML_antiquotation_def "type_syntax"} & : & @{text "ML antiquotation"} \\ |
1458 @{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\ |
1458 @{ML_antiquotation_def "const_syntax"} & : & @{text "ML antiquotation"} \\ |
1459 @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\ |
1459 @{ML_antiquotation_def "syntax_const"} & : & @{text "ML antiquotation"} \\ |
1460 \end{matharray} |
1460 \end{matharray} |
1461 |
1461 |
1462 Syntax translation functions written in ML admit almost arbitrary |
1462 Syntax translation functions written in ML admit almost arbitrary |
1463 manipulations of inner syntax, at the expense of some complexity and |
1463 manipulations of inner syntax, at the expense of some complexity and |
1464 obscurity in the implementation. |
1464 obscurity in the implementation. |