match !grafite_status with
[] -> exit n
| grafite_status::_ ->
- try
- let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in
+ let baseuri = GrafiteTypes.get_baseuri grafite_status 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
with
Failure _ -> assert false
;;
+
+let include_paths =
+ lazy (Helm_registry.get_list Helm_registry.string "matita.includes")
+;;
let rec interactive_loop () =
(* every loop is terminated by a terminator both on stdout and stderr *)
(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
- let include_paths =
- Helm_registry.get_list Helm_registry.string "matita.includes"
in
run_script str
- (MatitaEngine.eval_from_stream ~first_statement_only:true ~prompt:false
- ~include_paths ~watch_statuses) ;
+ (MatitaEngine.eval_from_stream ~first_statement_only:true
+ ~include_paths:(Lazy.force include_paths) ~watch_statuses) ;
interactive_loop (Some (List.length !lexicon_status))
with
| GrafiteEngine.Macro (floc,_) ->
);
(* 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 ()];
+ grafite_status := [GrafiteSync.init "cic:/matita/tests/"];
lexicon_status :=
[CicNotation2.load_notation ~include_paths
BuildTimeConf.core_notation_script] ;
| End_of_file -> ()
| GrafiteEngine.Drop -> clean_exit 1
);
- let proof_status,moo_content_rev,metadata,lexicon_content_rev =
+ let proof_status,moo_content_rev,lexicon_content_rev =
match !lexicon_status,!grafite_status with
| ss::_, s::_ ->
- s.proof_status, s.moo_content_rev, ss.LexiconEngine.metadata,
+ s.proof_status, s.moo_content_rev,
ss.LexiconEngine.lexicon_content_rev
| _,_ -> assert false
in
else
begin
let baseuri =
- GrafiteTypes.get_string_option
- (match !grafite_status with
+ GrafiteTypes.get_baseuri
+ (match !grafite_status with
[] -> assert false
- | s::_ -> s) "baseuri" in
+ | s::_ -> s)
+ 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;
exit 0
end