let pp_ast_statement grafite_status stm =
let stm = GrafiteAstPp.pp_statement
~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
- ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term ~obj_pp:(CicNotationPp.pp_obj
- CicNotationPp.pp_term) stm
+ ~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 =
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:CicNotationPp.pp_term
+ GrafiteAstPp.pp_statement ~term_pp:NotationPp.pp_term
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
- ~lazy_term_pp:CicNotationPp.pp_term
- ~obj_pp:(CicNotationPp.pp_obj CicNotationPp.pp_term) stm
+ ~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 (_, G.Macro (_, G.Inline (_, uri, params))) ->
- let str =
- ApplyTransformation.txt_of_inline_macro params uri
- ~map_unicode_to_tex:
- (Helm_registry.get_bool "matita.paste_unicode_as_tex")
- in
- output_string och str
| G.Executable (loc, G.Command (_, G.Include (_, false, _, _))) -> ()
| stm ->
output_string och (pp_statement stm); nl (); nl ()
end
;;
-let get_macro_context = function
- | Some status when status#proof_status = GrafiteTypes.No_proof -> []
- | Some status ->
- let stack = GrafiteTypes.get_stack status in
- let goal = Continuationals.Stack.find_goal stack in
- GrafiteTypes.get_proof_context status goal
- | None -> assert false
+let get_macro_context = function _ -> []
;;
let pp_times fname rc big_bang big_bang_u big_bang_s =
;;
let activate_extraction baseuri fname =
+ ()
+ (* MATITA 1.0
if Helm_registry.get_bool "matita.extract" then
let mangled_baseuri =
let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
(fun ~add_obj ~add_coercion _ obj ->
output_string f (CicExportation.ppobj baseuri obj);
flush f; []);
+ *)
;;
let compile atstart options fname =
~must_exist:false ~baseuri ~writable:true
in
(* cleanup of previously compiled objects *)
- if (not (Http_getter_storage.is_empty ~local:true baseuri) ||
- LibraryClean.db_uris_of_baseuri baseuri <> [])
+ if (not (Http_getter_storage.is_empty ~local:true baseuri))
then begin
HLog.message ("baseuri " ^ baseuri ^ " is not empty");
HLog.message ("cleaning baseuri " ^ baseuri);
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
| (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
in
aux_for_dump print_cb grafite_status
in
let elapsed = Unix.time () -. time in
- let proof_status,moo_content_rev,lexicon_content_rev =
- grafite_status#proof_status, grafite_status#moo_content_rev,
+ let moo_content_rev,lexicon_content_rev =
+ grafite_status#moo_content_rev,
grafite_status#lstatus.LexiconEngine.lexicon_content_rev
in
- if proof_status <> GrafiteTypes.No_proof then
- (HLog.error
- "there are still incomplete proofs at the end of the script";
- pp_times fname false big_bang big_bang_u big_bang_s;
-(*
- LexiconSync.time_travel
- ~present:lexicon_status ~past:initial_lexicon_status;
-*)
- clean_exit baseuri false)
- else
(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;