X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=52d18f42a3ea5d43caaf6856d02d5aabb8377900;hb=c9a1672c725945b47f9ea8af3c23b67cf9026f01;hp=883cf3284fb835cbbcab30afe1764375f3cc7d41;hpb=c113a2d7c7a2963d98bb5ce75d53cd7a4f482d6b;p=helm.git diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 883cf3284..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 @@ -124,6 +118,10 @@ let outer_syntax_parser () = 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 *) @@ -137,25 +135,22 @@ 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,bo,ty,attrs ; + {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ; GrafiteTypes.stack = stack } -> let open_goals = Continuationals.Stack.open_goals stack in print_endline @@ -163,17 +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 - 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) ; - interactive_loop (Some (List.length !lexicon_status)) + (MatitaEngine.eval_from_stream ~first_statement_only:true + ~include_paths:(Lazy.force include_paths) ~watch_statuses) ; + interactive_loop (Some (List.length !grafite_status)) with | GrafiteEngine.Macro (floc,_) -> let x, y = HExtlib.loc_of_floc floc in @@ -201,18 +195,15 @@ let main () = | `Warning -> "