additional commit for version 0.8.2

[helm.git] / helm / software / helena / src / basic_rg / brgGrafite.ml

diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml
index 493ad3cac848532158ada852d01665d1062d69c8..7df37c2785fff4972a10a3f56e2372bf661cbc0e 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgGrafite.ml
+++ b/helm/software/helena/src/basic_rg/brgGrafite.ml
@@ -31,7 +31,7 @@ let ext = ".ma"
 let width = 70
 
 let out_preamble och =
-   let ich = open_in !G.ma_preamble in
+   let ich = open_in !G.preamble in
    let rec aux () = KP.fprintf och "%s\n" (input_line ich); aux () in
    try aux () with End_of_file -> close_in ich
 
@@ -104,18 +104,9 @@ let rec out_term st p e och = function
          op out_name a (out_term st false e) v (out_term st false ee) t cp
    | B.Bind (a, B.Void, t)   -> C.err ()
 
-(* Interface functions ******************************************************)
-
-let open_out fname =
-   let dir = KF.concat !G.ma_dir base in 
-   let path = KF.concat dir fname in
-   let och = open_out (path ^ ext) in
-   out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
-   out_include och "basics/pts";
-   och
+let close_out och () = close_out och
 
-let output_entity st och (_, na, s, b) =
+let output_entity och st (_, na, s, b) =
    out_comment och (KP.sprintf "constant %u" na.E.n_apix);
    match b with
       | E.Abbr t ->
@@ -124,4 +115,13 @@ let output_entity st och (_, na, s, b) =
          KP.fprintf och "axiom %a : %a.\n\n%!" out_uri s (out_term st false B.empty) t; !ok
       | E.Void   -> C.err ()
 
-let close_out och = close_out och
+(* Interface functions ******************************************************)
+
+let open_out fname =
+   let dir = KF.concat !G.manager_dir base in 
+   let path = KF.concat dir fname in
+   let och = open_out (path ^ ext) in
+   out_preamble och;
+   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_include och "basics/pts";
+   output_entity och, close_out och