equal
deleted
inserted
replaced
55 |
55 |
56 in |
56 in |
57 |
57 |
58 val _ = |
58 val _ = |
59 Theory.setup |
59 Theory.setup |
60 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_type\<close> |
60 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala\<close> |
|
61 (Scan.lift Parse.embedded) (fn _ => tap static_check) #> |
|
62 |
|
63 Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_type\<close> |
61 (Scan.lift (Parse.embedded -- (types >> print_types))) |
64 (Scan.lift (Parse.embedded -- (types >> print_types))) |
62 (fn _ => fn (t, type_args) => |
65 (fn _ => fn (t, type_args) => |
63 (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args); t ^ type_args)) #> |
66 (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args); t ^ type_args)) #> |
64 |
67 |
65 Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_object\<close> |
68 Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_object\<close> |