20 \<^scala>\<open>scala_toplevel\<close> source |
20 \<^scala>\<open>scala_toplevel\<close> source |
21 |> YXML.parse_body |
21 |> YXML.parse_body |
22 |> let open XML.Decode in list string end |
22 |> let open XML.Decode in list string end |
23 in if null errors then () else error (cat_lines errors) end; |
23 in if null errors then () else error (cat_lines errors) end; |
24 |
24 |
25 fun static_check source = |
25 fun static_check (source, pos) = |
26 toplevel ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }"); |
26 toplevel ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }") |
|
27 handle ERROR msg => error (msg ^ Position.here pos); |
27 |
28 |
28 |
29 |
29 (* antiquotations *) |
30 (* antiquotations *) |
30 |
31 |
31 local |
32 local |
60 in |
61 in |
61 |
62 |
62 val _ = |
63 val _ = |
63 Theory.setup |
64 Theory.setup |
64 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala\<close> |
65 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala\<close> |
65 (Scan.lift Parse.embedded) (fn _ => tap static_check) #> |
66 (Scan.lift Args.embedded_position) |
|
67 (fn _ => fn (s, pos) => (static_check (s, pos); s)) #> |
66 |
68 |
67 Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_type\<close> |
69 Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_type\<close> |
68 (Scan.lift (Parse.embedded -- (types >> print_types))) |
70 (Scan.lift (Args.embedded_position -- (types >> print_types))) |
69 (fn _ => fn (t, type_args) => |
71 (fn _ => fn ((t, pos), type_args) => |
70 (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args); |
72 (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args, pos); |
71 scala_name (t ^ type_args))) #> |
73 scala_name (t ^ type_args))) #> |
72 |
74 |
73 Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_object\<close> |
75 Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_object\<close> |
74 (Scan.lift Parse.embedded) |
76 (Scan.lift Args.embedded_position) |
75 (fn _ => fn object => (static_check ("val _test_ = " ^ object); scala_name object)) #> |
77 (fn _ => fn (x, pos) => (static_check ("val _test_ = " ^ x, pos); scala_name x)) #> |
76 |
78 |
77 Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_method\<close> |
79 Thy_Output.antiquotation_raw_embedded \<^binding>\<open>scala_method\<close> |
78 (Scan.lift (class -- Parse.embedded -- types -- args)) |
80 (Scan.lift (class -- Args.embedded_position -- types -- args)) |
79 (fn _ => fn (((class_context, method), method_types), method_args) => |
81 (fn _ => fn (((class_context, (method, pos)), method_types), method_args) => |
80 let |
82 let |
81 val class_types = (case class_context of SOME (_, Ts) => Ts | NONE => []); |
83 val class_types = (case class_context of SOME (_, Ts) => Ts | NONE => []); |
82 val def = "def _test_" ^ print_types (merge (op =) (method_types, class_types)); |
84 val def = "def _test_" ^ print_types (merge (op =) (method_types, class_types)); |
83 val def_context = |
85 val def_context = |
84 (case class_context of |
86 (case class_context of |
85 NONE => def ^ " = " |
87 NONE => def ^ " = " |
86 | SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_."); |
88 | SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_."); |
87 val source = def_context ^ method ^ method_args; |
89 val source = def_context ^ method ^ method_args; |
88 val _ = static_check source; |
90 val _ = static_check (source, pos); |
89 val text = (case class_context of NONE => method | SOME c => print_class c ^ "." ^ method); |
91 val text = (case class_context of NONE => method | SOME c => print_class c ^ "." ^ method); |
90 in scala_name text end)); |
92 in scala_name text end)); |
91 |
93 |
92 end; |
94 end; |
93 |
95 |