X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fsyntax_extensions%2Fmake_table.ml;h=59204c6e47c0aaca4837193c4f2dfc1d8e05e8d4;hb=0ef9250d71eacd6b1022194128e6acfb74d52aac;hp=e8e453df4c1b842772642bf437214806281277fc;hpb=58955ec841575330f0b429033264f9ec7df319f9;p=helm.git

diff --git a/helm/software/components/syntax_extensions/make_table.ml b/helm/software/components/syntax_extensions/make_table.ml
index e8e453df4..59204c6e4 100644
--- a/helm/software/components/syntax_extensions/make_table.ml
+++ b/helm/software/components/syntax_extensions/make_table.ml
@@ -81,14 +81,17 @@ let parse_from_xml () =
 
 let main () =
   let oc = open_out Sys.argv.(1) in
+  let oc_doc = open_out Sys.argv.(2) in
   output_string oc "(* GENERATED by make_table: DO NOT EDIT! *)\n";
+  output_string oc_doc "(* GENERATED by make_table: DO NOT EDIT! *)\n";
   output_string oc "let macro2utf8 = Hashtbl.create 2000\n";
   output_string oc "let utf82macro = Hashtbl.create 2000\n";
   output_string oc "let data = [\n";
   let macro2utf8 = parse_from_xml () in
   Hashtbl.iter
     (fun macro utf8 ->
-      fprintf oc "  \"%s\", \"%s\";\n" macro (String.escaped utf8))
+            fprintf oc "  \"%s\", \"%s\";\n" macro (String.escaped utf8);
+            fprintf oc_doc "\\%s %s\n" macro utf8)
     macro2utf8;
   output_string oc "  ];;\n";
   output_string oc "let _ =\n";
@@ -97,7 +100,8 @@ let main () =
   output_string oc "      Hashtbl.replace macro2utf8 macro utf8;\n";
   output_string oc "      Hashtbl.replace utf82macro utf8 macro)\n";
   output_string oc "    data;;\n";
-  close_out oc
+  close_out oc;
+  close_out oc_doc
 
 let _ = main ()