equal
deleted
inserted
replaced
80 fun check_function ctxt arg = |
80 fun check_function ctxt arg = |
81 Completion.check_entity Markup.scala_functionN |
81 Completion.check_entity Markup.scala_functionN |
82 (functions () |> sort_strings |> map (fn a => (a, Resources.scala_function_pos a))) ctxt arg; |
82 (functions () |> sort_strings |> map (fn a => (a, Resources.scala_function_pos a))) ctxt arg; |
83 |
83 |
84 val _ = Theory.setup |
84 val _ = Theory.setup |
85 (ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close> |
85 (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close> |
|
86 (Scan.lift Parse.embedded_position) check_function #> |
|
87 ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close> |
86 (Args.context -- Scan.lift Parse.embedded_position |
88 (Args.context -- Scan.lift Parse.embedded_position |
87 >> (uncurry check_function #> ML_Syntax.print_string)) #> |
89 >> (uncurry check_function #> ML_Syntax.print_string)) #> |
88 ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close> |
90 ML_Antiquotation.value_embedded \<^binding>\<open>scala\<close> |
89 (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => |
91 (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => |
90 let val name = check_function ctxt arg |
92 let val name = check_function ctxt arg |