# HG changeset patch
# User haftmann
# Date 1167420858 -3600
# Node ID dc9366853df18aafd69ec2771f95839be079b7ac
# Parent  56abe5f3c612a0886e959ec9030e014cde1b0bee
improved print of constructors in OCaml

diff -r 56abe5f3c612 -r dc9366853df1 src/Pure/Tools/codegen_serializer.ML
--- a/src/Pure/Tools/codegen_serializer.ML	Fri Dec 29 20:34:17 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML	Fri Dec 29 20:34:18 2006 +0100
@@ -721,15 +721,15 @@
             )
           end
     and pr_app' vars (app as ((c, (iss, ty)), ts)) =
-      if is_cons c then let
-        val k = (length o fst o CodegenThingol.unfold_fun) ty
-      in if k = 0 then 
-        [(str o deresolv) c]
-      else if k = length ts then
-        [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
-      else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
-        (str o deresolv) c
-          :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
+      if is_cons c then
+        if (length o fst o CodegenThingol.unfold_fun) ty = length ts
+        then case ts
+         of [] => [(str o deresolv) c]
+          | [t] => [(str o deresolv) c, pr_term vars BR t]
+          | _ => [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
+        else [pr_term vars BR (CodegenThingol.eta_expand app ((length o fst o CodegenThingol.unfold_fun) ty))]
+      else (str o deresolv) c
+        :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts)
     and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =
       mk_app (pr_app' vars) (pr_term vars) const_syntax fxy app;
     fun pr_def (MLFuns (funns as funn :: funns')) =
@@ -757,7 +757,7 @@
                   |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames)
                       (insert (op =)) ts []);
               in (Pretty.block o Pretty.breaks) [
-                (Pretty.block o Pretty.commas) (map (pr_term vars BR) ts),
+                (Pretty.block o Pretty.commas) (map (pr_term vars NOBR) ts),
                 str "->",
                 pr_term vars NOBR t
               ] end;
@@ -1952,7 +1952,7 @@
         str "->",
         pr_typ (INFX (1, R)) ty2
       ]))
-  (*IntInt resp. Big_int are added later when CODE extraction for numerals is set up*)
+  (*IntInt resp. Big_int are added later when code extraction for numerals is set up*)
   #> add_reserved "SML" "o" (*dictionary projections use it already*)
   #> fold (add_reserved "Haskell") [
       "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",