# HG changeset patch
# User haftmann
# Date 1356638468 -3600
# Node ID e21485358c56f8c602609aa8bfb253ca47612c6d
# Parent  e3d25e751d05c93a937f2ff668ef7f0aceda9db7
uniform parentheses for constructor -- necessary to accomodate scala 10

diff -r e3d25e751d05 -r e21485358c56 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu Dec 27 21:01:08 2012 +0100
+++ b/src/Tools/Code/code_printer.ML	Thu Dec 27 21:01:08 2012 +0100
@@ -67,6 +67,7 @@
   val brackify: fixity -> Pretty.T list -> Pretty.T
   val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
+  val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
   val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
 
@@ -270,11 +271,16 @@
     else p
   end;
 
-fun applify opn cls f fxy_ctxt p [] = p
-  | applify opn cls f fxy_ctxt p ps =
+fun gen_applify strict opn cls f fxy_ctxt p [] =
+      if strict
+      then (if fixity BR fxy_ctxt then enclose "(" ")" else Pretty.block) [p, str "()"]
+      else p
+  | gen_applify strict opn cls f fxy_ctxt p ps =
       (if fixity BR fxy_ctxt then enclose "(" ")" else Pretty.block)
         (p @@ enum "," opn cls (map f ps));
 
+fun applify opn = gen_applify false opn;
+
 fun tuplify _ _ [] = NONE
   | tuplify print fxy [x] = SOME (print fxy x)
   | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
diff -r e3d25e751d05 -r e21485358c56 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Dec 27 21:01:08 2012 +0100
+++ b/src/Tools/Code/code_scala.ML	Thu Dec 27 21:01:08 2012 +0100
@@ -25,7 +25,7 @@
 (** Scala serializer **)
 
 fun print_scala_stmt tyco_syntax const_syntax reserved
-    args_num is_singleton_constr (deresolve, deresolve_full) =
+    args_num is_constr (deresolve, deresolve_full) =
   let
     fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
     fun intro_tyvars vs = intro_vars (map (first_upper o fst) vs);
@@ -75,10 +75,9 @@
         (app as ({ name = c, typargs, dom, ... }, ts)) =
       let
         val k = length ts;
-        val typargs' = if is_pat orelse
-          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else typargs;
+        val typargs' = if is_pat then [] else typargs;
         val (l, print') = case const_syntax c
-         of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
+         of NONE => (args_num c, fn fxy => fn ts => gen_applify (is_constr c ) "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR ((str o deresolve) c) typargs') ts)
@@ -206,22 +205,17 @@
       | print_stmt (name, Code_Thingol.Datatype (_, (vs, cos))) =
           let
             val tyvars = intro_tyvars (map (rpair []) vs) reserved;
-            fun print_co ((co, _), []) =
-                  concat [str "final", str "case", str "object", (str o deresolve) co,
-                    str "extends", applify "[" "]" I NOBR ((str o deresolve) name)
-                      (replicate (length vs) (str "Nothing"))]
-              | print_co ((co, vs_args), tys) =
-                  concat [applify "(" ")"
-                    (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg)) NOBR
-                    (applify "[" "]" (str o lookup_tyvar tyvars) NOBR ((concat o map str)
-                      ["final", "case", "class", deresolve co]) vs_args)
-                    (Name.invent_names (snd reserved) "a" tys),
-                    str "extends",
-                    applify "[" "]" (str o lookup_tyvar tyvars) NOBR
-                      ((str o deresolve) name) vs
-                  ];
+            fun print_co ((co, vs_args), tys) =
+              concat [Pretty.block ((applify "[" "]" (str o lookup_tyvar tyvars) NOBR
+                ((concat o map str) ["final", "case", "class", deresolve co]) vs_args)
+                @@ enum "," "(" ")" (map (fn (v, arg) => constraint (str v) (print_typ tyvars NOBR arg))
+                  (Name.invent_names (snd reserved) "a" tys))),
+                str "extends",
+                applify "[" "]" (str o lookup_tyvar tyvars) NOBR
+                  ((str o deresolve) name) vs
+              ];
           in
-            Pretty.chunks (applify "[" "]" (str o prefix "+" o lookup_tyvar tyvars)
+            Pretty.chunks (applify "[" "]" (str o lookup_tyvar tyvars)
               NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve name]) vs
                 :: map print_co cos)
           end
@@ -359,12 +353,9 @@
       | Code_Thingol.Classparam (_, class) =>
           (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
             (classparams_of_class class)) c;
-    fun is_singleton_constr c = case Graph.get_node program c
-     of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
-      | _ => false;
     fun print_stmt prefix_fragments = print_scala_stmt
       tyco_syntax const_syntax (make_vars reserved_syms) args_num
-      is_singleton_constr (deresolver prefix_fragments, deresolver []);
+      (Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver []);
 
     (* print modules *)
     fun print_implicit prefix_fragments implicit =