X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=87e9a44178a47a18b5bad6f9e9b3961e0825e71f;hb=48ccd3ca2b890b89775f1fbf7827bf617cf7aa19;hp=883cf3284fb835cbbcab30afe1764375f3cc7d41;hpb=c113a2d7c7a2963d98bb5ce75d53cd7a4f482d6b;p=helm.git diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 883cf3284..87e9a4417 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -66,13 +66,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 = 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 @@ -124,6 +120,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 *) @@ -155,7 +155,7 @@ let rec interactive_loop () = let watch_statuses lexicon_status grafite_status = match grafite_status.GrafiteTypes.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,16 +163,15 @@ 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) ; + (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,_) -> @@ -201,15 +200,14 @@ let main () = | `Warning -> "