X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaWiki.ml;h=3c5607bd7df9ff1bf458d61f5f0dac65a3aea604;hb=e42a9a3eabac1d284a37a8f5e22d6e73b0dc887f;hp=883cf3284fb835cbbcab30afe1764375f3cc7d41;hpb=c113a2d7c7a2963d98bb5ce75d53cd7a4f482d6b;p=helm.git diff --git a/helm/software/matita/matitaWiki.ml b/helm/software/matita/matitaWiki.ml index 883cf3284..3c5607bd7 100644 --- a/helm/software/matita/matitaWiki.ml +++ b/helm/software/matita/matitaWiki.ml @@ -124,6 +124,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 +159,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 +167,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) ; + ~include_paths:(Lazy.force include_paths) ~watch_statuses) ; interactive_loop (Some (List.length !lexicon_status)) with | GrafiteEngine.Macro (floc,_) -> @@ -201,8 +204,8 @@ let main () = | `Warning -> "