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 *)
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
(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,_) ->
| `Warning -> "<div style='color:yellow'>Warn: " ^ msg ^ "</div><br/>\n"
| `Error -> "<div style='color:red'>Error: " ^ msg ^ "</div><br/>\n"
in
- output_string stdout s;
- flush stdout
+ output_string stderr s;
+ flush stderr
);
(* must be called after init since args are set by cmdline parsing *)
let system_mode = Helm_registry.get_bool "matita.system" in