X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fxoa%2Flib.ml;fp=matita%2Fcomponents%2Fbinaries%2Fxoa%2Flib.ml;h=9684dc55873f3998b3eaf1b8357f77ec37b79012;hp=f2bf31757a88a9887d1f13a167d5b3ddd004b129;hb=ef225b816c82d4fad37993f963804e51152f4dac;hpb=b161347767b1cb67c4f5b115e4414b85ac4b2183 diff --git a/matita/components/binaries/xoa/lib.ml b/matita/components/binaries/xoa/lib.ml index f2bf31757..9684dc558 100644 --- a/matita/components/binaries/xoa/lib.ml +++ b/matita/components/binaries/xoa/lib.ml @@ -14,51 +14,51 @@ module K = Sys module R = Helm_registry -let template = "matita.ma.templ" +let template = "../../../matita/matita.ma.templ" let myself = F.basename Sys.argv.(0) -let get_preamble conf = - R.load_from conf; - let rt_base_dir = R.get_string "matita.rt_base_dir" in - F.concat rt_base_dir template +let rt_base_dir = F.dirname Sys.argv.(0) + +let get_preamble () = + F.concat rt_base_dir template let copy_preamble preamble och = - let ich = open_in preamble in - let rec read () = - Printf.fprintf och "%s\n" (input_line ich); read () - in - try read () with End_of_file -> close_in ich + let ich = open_in preamble in + let rec read () = + Printf.fprintf och "%s\n" (input_line ich); read () + in + try read () with End_of_file -> close_in ich let print_header def och = let msg = if def then "LOGIC" else "GROUND NOTATION" in - let stars = String.make (72 - String.length msg) '*' in - Printf.fprintf och "(* %s %s*)\n\n" msg stars + let stars = String.make (72 - String.length msg) '*' in + Printf.fprintf och "(* %s %s*)\n\n" msg stars let print_comment och = - let msg = Printf.sprintf "NOTE: This file was generated by %s, do not edit" myself in - let stars = String.make (72 - String.length msg) '*' in - Printf.fprintf och "(* %s %s*)\n\n" msg stars + let msg = Printf.sprintf "NOTE: This file was generated by %s, do not edit" myself in + let stars = String.make (72 - String.length msg) '*' in + Printf.fprintf och "(* %s %s*)\n\n" msg stars let exists_out name = - let path = [ - R.get_string "xoa.output_dir"; - name - ] in - let name = List.fold_left F.concat "" path in - K.file_exists (name ^ ".ma") + let path = [ + R.get_string "xoa.output_dir"; + name + ] in + let name = List.fold_left F.concat "" path in + K.file_exists (name ^ ".ma") let open_out def preamble name = - let path = [ - R.get_string "xoa.output_dir"; - name - ] in - let name = List.fold_left F.concat "" path in - let och = open_out (name ^ ".ma") in - copy_preamble preamble och; - print_header def och; - print_comment och; - och + let path = [ + R.get_string "xoa.output_dir"; + name + ] in + let name = List.fold_left F.concat "" path in + let och = open_out (name ^ ".ma") in + copy_preamble preamble och; + print_header def och; + print_comment och; + och let out_include och s = - Printf.fprintf och "include \"%s\".\n\n" s + Printf.fprintf och "include \"%s\".\n\n" s