X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fxoa%2Fxoa.ml;h=3d35f1932145b3e050c63d8c126d33557831d8c3;hb=ef225b816c82d4fad37993f963804e51152f4dac;hp=64ce87b175ce1b96d17b4d2ce9bb64e9f9aa75b3;hpb=b161347767b1cb67c4f5b115e4414b85ac4b2183;p=helm.git diff --git a/matita/components/binaries/xoa/xoa.ml b/matita/components/binaries/xoa/xoa.ml index 64ce87b17..3d35f1932 100644 --- a/matita/components/binaries/xoa/xoa.ml +++ b/matita/components/binaries/xoa/xoa.ml @@ -18,6 +18,9 @@ module E = Engine let incremental = ref true let separate = ref false +let preamble = + L.get_preamble () + let clear () = incremental := true; separate := false; @@ -33,7 +36,7 @@ let unm_and s = Scanf.sscanf s "%u" A.mk_and let process_centralized conf = - let preamble = L.get_preamble conf in + R.load_from conf; if R.has "xoa.objects" && R.has "xoa.notations" then begin let ooch = L.open_out true preamble (R.get_string "xoa.objects") in let noch = L.open_out false preamble (R.get_string "xoa.notations") in @@ -71,7 +74,7 @@ let generate (p, o, n) d = end let process_distributed conf = - let preamble = L.get_preamble conf in + R.load_from conf; if R.has "xoa.objects" && R.has "xoa.notations" then begin let st = preamble, R.get_string "xoa.objects", R.get_string "xoa.notations" in List.iter (generate st) (R.get_list unm_ex "xoa.ex");