]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/syntax_extensions/make_table.ml
parameter sintax added to axiom statement
[helm.git] / helm / software / components / syntax_extensions / make_table.ml
index e8e453df4c1b842772642bf437214806281277fc..59204c6e47c0aaca4837193c4f2dfc1d8e05e8d4 100644 (file)
@@ -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 ()