# HG changeset patch # User wenzelm # Date 1590587470 -7200 # Node ID 1ca5623888bb09256e3f99a26d14fc75e21bf6f2 # Parent 70442ddbfb15fe9c2931e1de70c84e0bb03d22e3 tuned; diff -r 70442ddbfb15 -r 1ca5623888bb src/Pure/System/scala_compiler.ML --- a/src/Pure/System/scala_compiler.ML Wed May 27 14:33:03 2020 +0200 +++ b/src/Pure/System/scala_compiler.ML Wed May 27 15:51:10 2020 +0200 @@ -43,15 +43,15 @@ val types = Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") []; -val in_class = - Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.name -- types --| Parse.$$$ ")"); +val class = + Scan.option + (Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.name -- types --| Parse.$$$ ")")); val arguments = (Parse.nat >> (fn n => replicate n "_") || - Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args - || Scan.succeed " _"; + Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args; -val method_arguments = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _"; +val args = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _"; fun scala_name name = let val latex = Latex.string (Latex.output_ascii_breakable "." name) @@ -75,18 +75,19 @@ (fn _ => fn object => (static_check ("val _test_ = " ^ object); scala_name object)) #> Thy_Output.antiquotation_raw_embedded \<^binding>\scala_method\ - (Scan.lift (Scan.option in_class -- Parse.embedded -- types -- method_arguments)) - (fn _ => fn (((class, method), method_types), method_args) => + (Scan.lift (class -- Parse.embedded -- types -- args)) + (fn _ => fn (((class_context, method), method_types), method_args) => let - val class_types = (case class of SOME (_, Ts) => Ts | NONE => []); + val class_types = (case class_context of SOME (_, Ts) => Ts | NONE => []); val def = "def _test_" ^ print_types (merge (op =) (method_types, class_types)); val def_context = - (case class of + (case class_context of NONE => def ^ " = " | SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_."); val source = def_context ^ method ^ method_args; val _ = static_check source; - in scala_name (case class of NONE => method | SOME c => print_class c ^ "." ^ method) end)); + val text = (case class_context of NONE => method | SOME c => print_class c ^ "." ^ method); + in scala_name text end)); end;