let och = open_out f in
let nl () = output_string och (pp_statement nl_ast) in
MatitaMisc.out_preamble och;
- let grafite_parser_cb status = function
- | G.Executable (_, G.Macro (_, G.Inline (_, style, uri, prefix, flavour))) ->
+ let grafite_parser_cb = function
+ | G.Executable (_, G.Macro (_, G.Inline (_, uri, params))) ->
let str =
- ApplyTransformation.txt_of_inline_macro style prefix uri
- ?flavour
+ 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 ()
in
- let lexicon_parser_cb status cmd =
+ let lexicon_parser_cb cmd =
output_string och (pp_lexicon cmd); nl (); nl ()
in
begin fun () ->
end,
begin fun x ->
close_out och;
- GrafiteParser.set_grafite_callback (fun _ _ -> ());
- GrafiteParser.set_lexicon_callback (fun _ _ -> ());
+ GrafiteParser.set_grafite_callback (fun _ -> ());
+ GrafiteParser.set_lexicon_callback (fun _ -> ());
Helm_registry.set_bool "matita.moo" true;
x
end
;;
let get_macro_context = function
- | Some {GrafiteTypes.proof_status = GrafiteTypes.No_proof} -> []
+ | 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
if Http_getter_storage.is_read_only baseuri then assert false;
activate_extraction baseuri fname ;
let lexicon_status =
- CicNotation2.load_notation ~include_paths:[]
+ CicNotation2.load_notation ~include_paths:[] (new LexiconEngine.status)
BuildTimeConf.core_notation_script
in
atstart (); (* FG: do not invoke before loading the core notation script *)
if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ())
else pp_ast_statement
in
- let lexicon_status, grafite_status =
- let rec aux_for_dump x lexicon_status grafite_status =
+ let grafite_status =
+ let rec aux_for_dump x grafite_status =
try
match
MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths
- lexicon_status grafite_status buf x
+ grafite_status buf x
with
- | [] -> lexicon_status, grafite_status
- | ((grafite,lexicon),None)::_ -> lexicon, grafite
- | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
+ | [] -> grafite_status
+ | (g,None)::_ -> g
+ | (g,Some _)::_ ->
+ raise (AttemptToInsertAnAlias (g :> LexiconEngine.status))
with MatitaEngine.EnrichedWithStatus
- (GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn ->
+ (GrafiteEngine.Macro (floc, f), grafite) as exn ->
match f (get_macro_context (Some grafite)) with
- | _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
+ | _, GrafiteAst.Inline (_, _suri, _params) ->
(*
let str =
ApplyTransformation.txt_of_inline_macro style prefix suri
in
!out str;
*)
- aux_for_dump x lexicon grafite
+ aux_for_dump x grafite
|_-> raise exn
in
- aux_for_dump print_cb lexicon_status grafite_status
+ 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,
- lexicon_status.LexiconEngine.lexicon_content_rev
+ grafite_status#proof_status, grafite_status#moo_content_rev,
+ grafite_status#lstatus.LexiconEngine.lexicon_content_rev
in
if proof_status <> GrafiteTypes.No_proof then
(HLog.error
(* 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
end;
let tm = Unix.gmtime elapsed in
let sec = string_of_int tm.Unix.tm_sec ^ "''" in
~present:lexicon_status ~past:initial_lexicon_status;
*)
clean_exit baseuri false
- | MatitaEngine.EnrichedWithStatus (exn, _lexicon, _grafite) as exn' ->
+ | MatitaEngine.EnrichedWithStatus (exn, _grafite) as exn' ->
(match exn with
| Sys.Break -> HLog.error "user break!"
| HExtlib.Localized (floc,CicNotationParser.Parse_error err) ->
Printf.printf "rm %s\n" generated; flush stdout; r
end
else
- compile ignore options fname
+ compact (compile ignore options fname)
;;
let load_deps_file = Librarian.load_deps_file;;