equal
deleted
inserted
replaced
5 Derived Isar commands. |
5 Derived Isar commands. |
6 *) |
6 *) |
7 |
7 |
8 signature ISAR_CMD = |
8 signature ISAR_CMD = |
9 sig |
9 sig |
10 val generic_setup: (string * Position.T) option -> theory -> theory |
10 val generic_setup: string * Position.T -> theory -> theory |
11 val parse_ast_translation: bool * (string * Position.T) -> theory -> theory |
11 val parse_ast_translation: bool * (string * Position.T) -> theory -> theory |
12 val parse_translation: bool * (string * Position.T) -> theory -> theory |
12 val parse_translation: bool * (string * Position.T) -> theory -> theory |
13 val print_translation: bool * (string * Position.T) -> theory -> theory |
13 val print_translation: bool * (string * Position.T) -> theory -> theory |
14 val typed_print_translation: bool * (string * Position.T) -> theory -> theory |
14 val typed_print_translation: bool * (string * Position.T) -> theory -> theory |
15 val print_ast_translation: bool * (string * Position.T) -> theory -> theory |
15 val print_ast_translation: bool * (string * Position.T) -> theory -> theory |
132 |
132 |
133 (** theory declarations **) |
133 (** theory declarations **) |
134 |
134 |
135 (* generic_setup *) |
135 (* generic_setup *) |
136 |
136 |
137 fun generic_setup NONE = (fn thy => thy |> Context.setup ()) |
137 fun generic_setup (txt, pos) = |
138 | generic_setup (SOME (txt, pos)) = |
138 ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt |
139 ML_Context.use_let pos "val setup: theory -> theory" "Context.map_theory setup" txt |
139 |> Context.theory_map; |
140 |> Context.theory_map; |
|
141 |
140 |
142 |
141 |
143 (* translation functions *) |
142 (* translation functions *) |
144 |
143 |
145 local |
144 local |