From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 4 Feb 2013 17:35:10 +0000 (+0000)
Subject: Pretty printing of ocaml files slightly improved.
X-Git-Tag: make_still_working~1278
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=59dfa0b85ba8a74f4b5c175f72ac7ebeed6fca7f

Pretty printing of ocaml files slightly improved.
---

diff --git a/matita/components/ng_extraction/common.ml b/matita/components/ng_extraction/common.ml
index 57a27e92b..fffc09974 100644
--- a/matita/components/ng_extraction/common.ml
+++ b/matita/components/ng_extraction/common.ml
@@ -32,8 +32,6 @@ let pr_binding = function
 
 let fnl () = stras (1000000,"") ++ fnl ()
 
-let fnl2 () = fnl () ++ fnl ()
-
 let space_if = function true -> str " " | false -> mt ()
 
 let is_invalid_id s =
diff --git a/matita/components/ng_extraction/common.mli b/matita/components/ng_extraction/common.mli
index 4bde847ac..2cf44e003 100644
--- a/matita/components/ng_extraction/common.mli
+++ b/matita/components/ng_extraction/common.mli
@@ -19,7 +19,6 @@ open OcamlExtractionTable
     we attach a big virtual size to [fnl] newlines. *)
 
 val fnl : unit -> std_ppcmds
-val fnl2 : unit -> std_ppcmds
 val space_if : bool -> std_ppcmds
 
 val pp_par : bool -> std_ppcmds -> std_ppcmds
diff --git a/matita/components/ng_extraction/ocaml.ml b/matita/components/ng_extraction/ocaml.ml
index a612c58d4..001845e35 100644
--- a/matita/components/ng_extraction/ocaml.ml
+++ b/matita/components/ng_extraction/ocaml.ml
@@ -438,7 +438,7 @@ and pp_fix status par env i (ids,bl) args =
 let pp_val status e typ =
  let status,res = pp_type status false [] typ in
   status,
-  hov 4 (str "(** val " ++ e ++ str " :" ++ spc ()++res++ str " **)") ++ fnl2 ()
+  hov 4 (str "(** val " ++ e ++ str " :" ++ spc ()++res++ str " **)") ++ fnl ()
 
 (*s Pretty-printing of [Dfix] *)
 
@@ -461,7 +461,7 @@ let pp_Dfix status (rv,c,t) =
         let status,res = pp_val status names.(i) t.(i) in
         let status,res2 = pp status false (i+1) in
         status,
-	(if init then mt () else fnl2 ()) ++ res ++
+	(if init then mt () else fnl ()) ++ res ++
 	str (if init then "let rec " else "and ") ++ names.(i) ++ def ++ res2
   in pp status true 0
 
diff --git a/matita/components/ng_extraction/ocamlExtraction.ml b/matita/components/ng_extraction/ocamlExtraction.ml
index 0022599a8..da7eee5ac 100644
--- a/matita/components/ng_extraction/ocamlExtraction.ml
+++ b/matita/components/ng_extraction/ocamlExtraction.ml
@@ -14,7 +14,7 @@ let print_ocaml_of_obj0 status ((_uri,_,_,_,_) as obj) =
    map_status status
     (fun status ml ->
       let status,cmds = Ocaml.pp_decl status ml in
-      print_ppcmds ~in_ml:true status (cmds ++ fnl ());
+      print_ppcmds ~in_ml:true status (cmds ++ fnl () ++ fnl ());
       status,()) res in
   status
  with