X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitacLib.ml;fp=matita%2FmatitacLib.ml;h=fb4f3770f74eb6fd985a96a2b8935f6ea70e5676;hb=c3d1ee401a6ca0c86fcdde733f301e2fe6978143;hp=5495a6f78e9096558cd846be1dc6212930d07925;hpb=711e170c2deaa92289d9d4eb7c0e8aedbe62b5cb;p=helm.git diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index 5495a6f78..fb4f3770f 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -107,10 +107,11 @@ let get_include_paths options = include_paths ;; -let rec compile options fname = +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 + let root,baseuri,fname,_tgt = + Librarian.baseuri_of_script ~include_paths fname in let grafite_status = GrafiteSync.init baseuri in let lexicon_status = CicNotation2.load_notation ~include_paths:[] @@ -125,7 +126,8 @@ let rec compile options 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 + LibraryMisc.lexicon_file_of_baseuri + ~must_exist:false ~baseuri ~writable:true in if Http_getter_storage.is_read_only baseuri then HLog.error @@ -150,7 +152,8 @@ let rec compile options fname = HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri); if not (Helm_registry.get_bool "matita.verbose") then (let cc = - if Str.string_match(Str.regexp ".*opt$") Sys.argv.(0) 0 then "matitac.opt" + let rex = Str.regexp ".*opt$" in + if Str.string_match rex Sys.argv.(0) 0 then "matitac.opt" else "matitac" in let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in @@ -161,13 +164,29 @@ let rec compile options fname = else pp_ast_statement in let grafite_status, lexicon_status = + let rec aux_for_dump x = + try match MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths - lexicon_status grafite_status buf print_cb + lexicon_status grafite_status buf x with - | [] -> raise End_of_file + | [] -> grafite_status, lexicon_status | ((grafite,lexicon),None)::_ -> grafite, lexicon | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l) + + with MatitaEngine.EnrichedWithLexiconStatus + (GrafiteEngine.Macro (floc, f), lex_status) as exn -> + match f (get_macro_context (Some grafite_status)) with + | _, GrafiteAst.Inline (_, style, suri, prefix) -> + let str = + ApplyTransformation.txt_of_inline_macro style suri prefix + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") in + !out str; + aux_for_dump x + |_-> raise exn + in + aux_for_dump print_cb in let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = @@ -178,10 +197,12 @@ let rec compile options fname = (HLog.error "there are still incomplete proofs at the end of the script"; pp_times fname false big_bang; - LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; + LexiconSync.time_travel + ~present:lexicon_status ~past:initial_lexicon_status; clean_exit baseuri false) else - (if Helm_registry.get_bool "matita.moo" then begin + (if not (Helm_registry.get_bool "matita.moo" && + Filename.check_suffix fname ".mma") 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; @@ -197,31 +218,19 @@ let rec compile options fname = HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times fname true big_bang; - LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; + LexiconSync.time_travel + ~present:lexicon_status ~past:initial_lexicon_status; true) with (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *) | AttemptToInsertAnAlias lexicon_status -> pp_times fname false big_bang; - LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; + LexiconSync.time_travel + ~present:lexicon_status ~past:initial_lexicon_status; clean_exit baseuri false | MatitaEngine.EnrichedWithLexiconStatus (exn, lex_stat) -> (match exn with | Sys.Break -> HLog.error "user break!" - | GrafiteEngine.Macro (floc, f) -> - (try - match f (get_macro_context (Some grafite_status)) with - | _, GrafiteAst.Inline (_, style, suri, prefix) -> - let str = - ApplyTransformation.txt_of_inline_macro style suri prefix - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") in - (* the output of compilation is wrong in this way!! *) - !out str; ignore(compile options fname) - | _ -> - let x, y = HExtlib.loc_of_floc floc in - HLog.error (sprintf "A macro has been found at %d-%d" x y) - with exn -> HLog.error (snd (MatitaExcPp.to_string exn))) | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> let (x, y) = HExtlib.loc_of_floc floc in HLog.error (sprintf "Parse error at %d-%d: %s" x y err) @@ -229,10 +238,6 @@ let rec compile options fname = LexiconSync.time_travel ~present:lex_stat ~past:initial_lexicon_status; pp_times fname false big_bang; clean_exit baseuri false - | End_of_file -> (* this is CSC stuff ... or can only happen on empty files *) - HLog.error "End_of_file"; - pp_times fname false big_bang; - clean_exit baseuri false | Sys.Break as exn -> if matita_debug then raise exn; HLog.error "user break!"; @@ -240,7 +245,8 @@ let rec compile options fname = clean_exit baseuri false | exn -> if matita_debug then raise exn; - HLog.error ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn)); + HLog.error + ("Unwrapped exception, please fix: "^ snd (MatitaExcPp.to_string exn)); pp_times fname false big_bang; clean_exit baseuri false ;;