X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitacLib.ml;h=23a0ca15fa2cc3c22ce4effa407d0a7ab44c7bec;hb=cd664aefb80554952ed9b010f0c5199ce3a6f8f2;hp=706981937df97aace3cbf6369ff1321912962ad6;hpb=b8dac1f8f6b664b78e58c152cd3960e121713f5d;p=helm.git diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index 706981937..23a0ca15f 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -29,16 +29,13 @@ open Printf open GrafiteTypes -exception AttemptToInsertAnAlias of LexiconEngine.status +exception AttemptToInsertAnAlias of LexiconTypes.status let slash_n_RE = Pcre.regexp "\\n" ;; let pp_ast_statement grafite_status stm = - let stm = GrafiteAstPp.pp_statement + let stm = GrafiteAstPp.pp_statement stm ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") - ~term_pp:NotationPp.pp_term - ~lazy_term_pp:NotationPp.pp_term ~obj_pp:(NotationPp.pp_obj - NotationPp.pp_term) stm in let stm = Pcre.replace ~rex:slash_n_RE stm in let stm = @@ -52,45 +49,6 @@ let clean_exit baseuri rc = LibraryClean.clean_baseuris ~verbose:false [baseuri]; rc ;; -let dump f = - let module G = GrafiteAst in - let module L = LexiconAst in - let module H = HExtlib in - let floc = H.dummy_floc in - let nl_ast = G.Comment (floc, G.Note (floc, "")) in - let pp_statement stm = - GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - ~lazy_term_pp:NotationPp.pp_term - ~obj_pp:(NotationPp.pp_obj NotationPp.pp_term) stm - in - let pp_lexicon = LexiconAstPp.pp_command in - let och = open_out f in - let nl () = output_string och (pp_statement nl_ast) in - MatitaMisc.out_preamble och; - let grafite_parser_cb = function - | G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> () - | stm -> - output_string och (pp_statement stm); nl (); nl () - in - let lexicon_parser_cb cmd = - output_string och (pp_lexicon cmd); nl (); nl () - in - begin fun () -> - Helm_registry.set_bool "matita.moo" false; - GrafiteParser.set_grafite_callback grafite_parser_cb; - GrafiteParser.set_lexicon_callback lexicon_parser_cb - end, - begin fun x -> - close_out och; - GrafiteParser.set_grafite_callback (fun _ -> ()); - GrafiteParser.set_lexicon_callback (fun _ -> ()); - Helm_registry.set_bool "matita.moo" true; - x - end -;; - let get_macro_context = function _ -> [] ;; @@ -165,25 +123,18 @@ let compile atstart options fname = if Http_getter_storage.is_read_only baseuri then assert false; activate_extraction baseuri fname ; let lexicon_status = - CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status) + CicNotation2.load_notation ~include_paths:[] (new LexiconTypes.status) BuildTimeConf.core_notation_script in atstart (); (* FG: do not invoke before loading the core notation script *) - let grafite_status = GrafiteSync.init lexicon_status baseuri in + let grafite_status = + (new GrafiteTypes.status baseuri)#set_lstatus lexicon_status#lstatus in let big_bang = Unix.gettimeofday () in let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = Unix.times () in let time = Unix.time () in try - (* sanity checks *) - let moo_fname = - LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true - in - let lexicon_fname= - LibraryMisc.lexicon_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true - in (* cleanup of previously compiled objects *) if (not (Http_getter_storage.is_empty ~local:true baseuri)) then begin @@ -217,7 +168,6 @@ let compile atstart options fname = in let grafite_status = let rec aux_for_dump x grafite_status = - try match MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths grafite_status buf x @@ -225,36 +175,14 @@ let compile atstart options fname = | [] -> grafite_status | (g,None)::_ -> g | (g,Some _)::_ -> - raise (AttemptToInsertAnAlias (g :> LexiconEngine.status)) - with MatitaEngine.EnrichedWithStatus - (GrafiteEngine.Macro (floc, f), grafite) as exn -> - match f (get_macro_context (Some grafite)) with - | _, GrafiteAst.Inline (_, _suri, _params) -> -(* - let str = - ApplyTransformation.txt_of_inline_macro style prefix suri - ?flavour - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") - in - !out str; -*) - aux_for_dump x grafite - |_-> raise exn + raise (AttemptToInsertAnAlias (g :> LexiconTypes.status)) in aux_for_dump print_cb grafite_status in let elapsed = Unix.time () -. time in - let moo_content_rev,lexicon_content_rev = - grafite_status#moo_content_rev, - grafite_status#lstatus.LexiconEngine.lexicon_content_rev - in (if Helm_registry.get_bool "matita.moo" then begin - (* FG: we do not generate .moo when dumping .mma files *) - GrafiteMarshal.save_moo moo_fname moo_content_rev; - LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev; - NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) - grafite_status#dump + GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) + grafite_status#dump end; let tm = Unix.gmtime elapsed in let sec = string_of_int tm.Unix.tm_sec ^ "''" in @@ -354,32 +282,16 @@ module F = let matita_debug = Helm_registry.get_bool "matita.debug" in let compile atstart opts fname = try - GrafiteSync.push (); - GrafiteParser.push (); - let rc = compile atstart opts fname in - GrafiteParser.pop (); - GrafiteSync.pop (); - rc + (* MATITA 1.0: c'erano le push/pop per il parser; ma per + * l'environment nuovo? *) + compile atstart opts fname with - | Sys.Break -> - GrafiteParser.pop (); - GrafiteSync.pop (); - false + | Sys.Break -> false | exn when not matita_debug -> HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn)); assert false in - if Filename.check_suffix fname ".mma" then - let generated = Filename.chop_suffix fname ".mma" ^ ".ma" in - let atstart, atexit = dump generated in - let res = compile atstart options fname in - let r = compact (atexit res) in - if r then r else begin -(* Sys.remove generated; *) - Printf.printf "rm %s\n" generated; flush stdout; r - end - else - compact (compile ignore options fname) + compact (compile ignore options fname) ;; let load_deps_file = Librarian.load_deps_file;;