X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=52d18f42a3ea5d43caaf6856d02d5aabb8377900;hb=647b419e96770d90a82d7a9e5e8843566a9f93ee;hp=bbe8d2ed7247f60132ffa0f97e4c7e298959efc9;hpb=111df95ac03f2ee21dfa2422a7f531f675b1c16d;p=helm.git diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index bbe8d2ed7..52d18f42a 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -35,21 +35,19 @@ exception AttemptToInsertAnAlias (** {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 @@ -66,13 +64,9 @@ let clean_exit n = 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 @@ -141,23 +135,20 @@ let rec interactive_loop () = | 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 } -> @@ -167,14 +158,16 @@ let rec interactive_loop () = (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 @@ -207,13 +200,10 @@ let main () = ); (* 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 @@ -231,12 +221,12 @@ let main () = | End_of_file -> () | GrafiteEngine.Drop -> clean_exit 1 ); - 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.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 @@ -247,10 +237,10 @@ let main () = 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 @@ -261,6 +251,7 @@ let main () = in 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) dump; exit 0 end with