src/Tools/Code/code_scala.ML
changeset 37337 c0cf8b6c2c26
parent 37243 6e2ac5358d6e
child 37384 5aba26803073
     1.1 --- a/src/Tools/Code/code_scala.ML	Fri Jun 04 19:36:40 2010 +0200
     1.2 +++ b/src/Tools/Code/code_scala.ML	Fri Jun 04 19:36:41 2010 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4                    concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
     1.5                      str "=>", print_typ tyvars NOBR ty];
     1.6              fun print_classparam_val (classparam, ty) =
     1.7 -              concat [str "val", (str o suffix "$:" o deresolve_base) classparam,
     1.8 +              concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam,
     1.9                  (print_tupled_typ o Code_Thingol.unfold_fun) ty]
    1.10              fun print_classparam_def (classparam, ty) =
    1.11                let
    1.12 @@ -239,7 +239,7 @@
    1.13                  val head = print_defhead tyvars vars' ((str o deresolve) classparam) vs params tys [p_implicit] ty;
    1.14                in
    1.15                  concat [head, applify "(" ")" NOBR
    1.16 -                  (Pretty.block [str implicit, str ".", (str o suffix "$" o deresolve_base) classparam])
    1.17 +                  (Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam])
    1.18                    (map (str o lookup_var vars') params)]
    1.19                end;
    1.20            in
    1.21 @@ -268,7 +268,7 @@
    1.22                    [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
    1.23                      auxs tys), str "=>"]];
    1.24                in 
    1.25 -                concat ([str "val", (str o suffix "$" o deresolve_base) classparam,
    1.26 +                concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
    1.27                    str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
    1.28                end;
    1.29            in