(** {2 Initialization} *)
let grafite_status = (ref [] : GrafiteTypes.status list ref)
-let lexicon_status = (ref [] : LexiconEngine.status list ref)
let run_script is eval_function =
- let lexicon_status',grafite_status' =
- match !lexicon_status,!grafite_status with
- | ss::_, s::_ -> ss,s
- | _,_ -> assert false
+ let grafite_status' =
+ match !grafite_status with
+ | s::_ -> s
+ | _ -> assert false
in
let cb = fun _ _ -> () in
let matita_debug = Helm_registry.get_bool "matita.debug" in
try
- match eval_function lexicon_status' grafite_status' is cb with
+ match eval_function grafite_status' is cb with
[] -> raise End_of_file
- | ((grafite_status'',lexicon_status''),None)::_ ->
- lexicon_status := lexicon_status''::!lexicon_status;
+ | (grafite_status'',None)::_ ->
grafite_status := grafite_status''::!grafite_status
| (s,Some _)::_ -> raise AttemptToInsertAnAlias
with
match !grafite_status with
[] -> exit n
| grafite_status::_ ->
- try
- let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
+ let baseuri = grafite_status#baseuri in
LibraryClean.clean_baseuris ~verbose:false [baseuri];
exit n
- with GrafiteTypes.Option_error("baseuri", "not found") ->
- (* no baseuri ==> nothing to clean yet *)
- exit n
let terminate n =
let terminator = String.make 1 (Char.chr 249) in
| n,_::l -> drop (n-1,l)
| _,[] -> assert false
in
- let to_be_dropped = List.length !lexicon_status - n in
+ let to_be_dropped = List.length !grafite_status - n in
let safe_hd = function [] -> assert false | he::_ -> he in
- let cur_lexicon_status = safe_hd !lexicon_status in
let cur_grafite_status = safe_hd !grafite_status in
- lexicon_status := drop (to_be_dropped, !lexicon_status) ;
grafite_status := drop (to_be_dropped, !grafite_status) ;
- let lexicon_status = safe_hd !lexicon_status in
let grafite_status = safe_hd !grafite_status in
LexiconSync.time_travel
- ~present:cur_lexicon_status ~past:lexicon_status;
- GrafiteSync.time_travel
~present:cur_grafite_status ~past:grafite_status;
+ GrafiteSync.time_travel
+ ~present:cur_grafite_status ~past:grafite_status ();
interactive_loop (Some n)
| `Do command ->
let str = Ulexing.from_utf8_string command in
- let watch_statuses lexicon_status grafite_status =
- match grafite_status.GrafiteTypes.proof_status with
+ let watch_statuses grafite_status =
+ match grafite_status#proof_status with
GrafiteTypes.Incomplete_proof
{GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
GrafiteTypes.stack = stack } ->
(List.map
(fun i ->
ApplyTransformation.txt_of_cic_sequent 80 metasenv
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
(List.find (fun (j,_,_) -> j=i) metasenv)
) open_goals))
| _ -> ()
in
run_script str
- (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
+ (MatitaEngine.eval_from_stream ~first_statement_only:true
~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
- interactive_loop (Some (List.length !lexicon_status))
+ interactive_loop (Some (List.length !grafite_status))
with
| GrafiteEngine.Macro (floc,_) ->
let x, y = HExtlib.loc_of_floc floc in
);
(* must be called after init since args are set by cmdline parsing *)
let system_mode = Helm_registry.get_bool "matita.system" in
- Helm_registry.set_int "matita.verbosity" 0;
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
- grafite_status := [GrafiteSync.init ()];
- lexicon_status :=
- [CicNotation2.load_notation ~include_paths
- BuildTimeConf.core_notation_script] ;
+ grafite_status := [GrafiteSync.init (CicNotation2.load_notation ~include_paths
+ (new LexiconEngine.status) BuildTimeConf.core_notation_script) "cic:/matita/tests/"];
Sys.catch_break true;
let origcb = HLog.get_log_callback () in
let origcb t s = origcb t ((if system_mode then "[S] " else "") ^ s) in
| End_of_file -> ()
| GrafiteEngine.Drop -> clean_exit 1
);
- let proof_status,moo_content_rev,metadata,lexicon_content_rev =
- match !lexicon_status,!grafite_status with
- | ss::_, s::_ ->
- s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
- ss.LexiconEngine.lexicon_content_rev
- | _,_ -> assert false
+ let proof_status,moo_content_rev,lexicon_content_rev,dump =
+ match !grafite_status with
+ | s::_ ->
+ s#proof_status, s#moo_content_rev,
+ s#lstatus.LexiconEngine.lexicon_content_rev, s#dump
+ | _ -> assert false
in
if proof_status <> GrafiteTypes.No_proof then
begin
else
begin
let baseuri =
- GrafiteTypes.get_string_option
- (match !grafite_status with
- [] -> assert false
- | s::_ -> s) "baseuri" in
+ (match !grafite_status with
+ [] -> assert false
+ | s::_ -> s)#baseuri
+ in
let moo_fname =
LibraryMisc.obj_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- let metadata_fname =
- LibraryMisc.metadata_file_of_baseuri
- ~must_exist:false ~baseuri ~writable:true
- in
GrafiteMarshal.save_moo moo_fname moo_content_rev;
- LibraryNoDb.save_metadata metadata_fname metadata;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+ NCicLibrary.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri) dump;
exit 0
end
with