X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fsyntax_extensions%2Fmake_table.ml;fp=helm%2Fsoftware%2Fcomponents%2Fsyntax_extensions%2Fmake_table.ml;h=59204c6e47c0aaca4837193c4f2dfc1d8e05e8d4;hb=5de5d5d0d43dac0af692d84b004c03bcbe914457;hp=e8e453df4c1b842772642bf437214806281277fc;hpb=c7b6f4c93dd1fcdb4f226cf7ff22f75ae8728dba;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 ()