--- a/src/Tools/Code/code_scala.ML Fri Jun 04 19:36:40 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Fri Jun 04 19:36:41 2010 +0200
@@ -228,7 +228,7 @@
concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
str "=>", print_typ tyvars NOBR ty];
fun print_classparam_val (classparam, ty) =
- concat [str "val", (str o suffix "$:" o deresolve_base) classparam,
+ concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam,
(print_tupled_typ o Code_Thingol.unfold_fun) ty]
fun print_classparam_def (classparam, ty) =
let
@@ -239,7 +239,7 @@
val head = print_defhead tyvars vars' ((str o deresolve) classparam) vs params tys [p_implicit] ty;
in
concat [head, applify "(" ")" NOBR
- (Pretty.block [str implicit, str ".", (str o suffix "$" o deresolve_base) classparam])
+ (Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam])
(map (str o lookup_var vars') params)]
end;
in
@@ -268,7 +268,7 @@
[concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
auxs tys), str "=>"]];
in
- concat ([str "val", (str o suffix "$" o deresolve_base) classparam,
+ concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
end;
in