(** {2 Initialization} *)
-let _ = MatitaInit.initialize_all ()
+let _ = MatitaInit.initialize_all ()
+let _ = Paramodulation.Saturation.init () (* ALB to link paramodulation *)
(** {2 GUI callbacks} *)
(CicEnvironment.list_obj ()));
addDebugItem "print selections" (fun () ->
let cicMathView = MatitaMathView.cicMathView_instance () in
- List.iter MatitaLog.debug (cicMathView#string_of_selections));
- addDebugItem "dump getter settings" (fun _ ->
- prerr_endline (Http_getter_env.env_to_string ()));
- addDebugItem "getter: getalluris" (fun _ ->
- List.iter prerr_endline (Http_getter.getalluris ()));
+ List.iter HLog.debug (cicMathView#string_of_selections));
addDebugItem "dump script status" script#dump;
addDebugItem "dump configuration file to ./foo.conf.xml" (fun _ ->
Helm_registry.save_to "./foo.conf.xml");
addDebugItem "dump metasenv"
(fun _ ->
if script#onGoingProof () then
- MatitaLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
+ HLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
addDebugItem "dump coercions Db" (fun _ ->
List.iter
(fun (s,t,u) ->
- MatitaLog.debug
+ HLog.debug
(UriManager.name_of_uri u ^ ":"
^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
(CoercDb.to_list ()));
(List.map (fun (g, _, _) -> string_of_int g)
(MatitaScript.current ())#proofMetasenv));
prerr_endline ("stack: " ^ Continuationals.Stack.pp
- (MatitaMisc.get_stack (MatitaScript.current ())#status)));
+ (MatitaTypes.get_stack (MatitaScript.current ())#status)));
+(* addDebugItem "ask record choice"
+ (fun _ ->
+ HLog.debug (string_of_int
+ (MatitaGtkMisc.ask_record_choice ~gui ~title:"title" ~message:"msg"
+ ~fields:["a"; "b"; "c"]
+ ~records:[
+ ["0"; "0"; "0"]; ["0"; "0"; "1"]; ["0"; "1"; "0"]; ["0"; "1"; "1"];
+ ["1"; "0"; "0"]; ["1"; "0"; "1"]; ["1"; "1"; "0"]; ["1"; "1"; "1"]]
+ ()))); *)
addDebugItem "rotate light bulbs"
(fun _ ->
let nb = gui#main#hintNotebook in
nb#goto_page ((nb#current_page + 1) mod 3));
+ addDebugItem "print runtime dir"
+ (fun _ ->
+ prerr_endline BuildTimeConf.runtime_base_dir);
+ addDebugItem "disable all (pretty printing) notations"
+ (fun _ -> CicNotation.set_active_notations []);
+ addDebugItem "enable all (pretty printing) notations"
+ (fun _ ->
+ CicNotation.set_active_notations
+ (List.map fst (CicNotation.get_all_notations ())));
end
(** Debugging }}} *)