4 Support for Scala at runtime. |
4 Support for Scala at runtime. |
5 *) |
5 *) |
6 |
6 |
7 signature SCALA = |
7 signature SCALA = |
8 sig |
8 sig |
|
9 val functions: unit -> string list |
|
10 val check_function: Proof.context -> string * Position.T -> string |
9 val promise_function: string -> string -> string future |
11 val promise_function: string -> string -> string future |
10 val function: string -> string -> string |
12 val function: string -> string -> string |
11 exception Null |
13 exception Null |
12 val check: string -> unit |
|
13 end; |
14 end; |
14 |
15 |
15 structure Scala: SCALA = |
16 structure Scala: SCALA = |
16 struct |
17 struct |
17 |
18 |
68 (fn [id, tag, res] => |
69 (fn [id, tag, res] => |
69 fulfill id tag res |
70 fulfill id tag res |
70 handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn); |
71 handle exn => if Exn.is_interrupt exn then () else Exn.reraise exn); |
71 |
72 |
72 |
73 |
|
74 (* registered functions *) |
73 |
75 |
74 (** check source snippet **) |
76 fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); |
75 |
77 |
76 fun check source = |
78 fun check_function ctxt (name, pos) = |
77 let val errors = |
79 let |
78 function "scala_check" source |
80 val kind = Markup.scala_functionN; |
79 |> YXML.parse_body |
81 val funs = functions (); |
80 |> let open XML.Decode in list string end |
82 in |
81 in if null errors then () else error (cat_lines errors) end; |
83 if member (op =) funs name then |
|
84 (Context_Position.report ctxt pos (Markup.scala_function name); name) |
|
85 else |
|
86 let |
|
87 val completion_report = |
|
88 Completion.make_report (name, pos) |
|
89 (fn completed => |
|
90 filter completed funs |
|
91 |> sort_strings |
|
92 |> map (fn a => (a, (kind, a)))); |
|
93 in error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos ^ completion_report) end |
|
94 end; |
|
95 |
|
96 val _ = Theory.setup |
|
97 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close> |
|
98 (Scan.lift Parse.embedded_position) check_function #> |
|
99 ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close> |
|
100 (Args.context -- Scan.lift Parse.embedded_position |
|
101 >> (uncurry check_function #> ML_Syntax.print_string)) #> |
|
102 ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close> |
|
103 (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => |
|
104 let val name = check_function ctxt arg |
|
105 in ML_Syntax.atomic ("Scala.function " ^ ML_Syntax.print_string name) end))); |
82 |
106 |
83 end; |
107 end; |