From 156e9d172f3fd2fd7f2d5f0f88c8662c2c0fd796 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 21 Jan 2008 17:30:35 +0000 Subject: [PATCH] Hack for code extraction re-linked, but disactivated. --- helm/software/matita/matitacLib.ml | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml index 83e833ebe..fc64479f1 100644 --- a/helm/software/matita/matitacLib.ml +++ b/helm/software/matita/matitacLib.ml @@ -109,12 +109,28 @@ let get_include_paths options = include_paths ;; +let activate_extraction baseuri fname = + if false then + let mangled_baseuri = + let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in + let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in + String.uncapitalize baseuri in + let f = + open_out + (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in + LibrarySync.set_object_declaration_hook + (fun _ obj -> + output_string f (CicExportation.ppobj baseuri obj); + flush f); +;; + let compile options fname = let matita_debug = Helm_registry.get_bool "matita.debug" in let include_paths = get_include_paths options in let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in if Http_getter_storage.is_read_only baseuri then assert false; + activate_extraction baseuri fname ; let grafite_status = GrafiteSync.init baseuri in let lexicon_status = CicNotation2.load_notation ~include_paths:[] -- 2.39.5