- addDebugItem "interactive user uri choice" (fun _ ->
- try
- let uris =
- interactive_user_uri_choice ~gui ~selection_mode:`MULTIPLE
- ~msg:"messaggio" ~nonvars_button:true
- ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
- "cic:/cinque.var"]
- in
- List.iter prerr_endline uris
- with MatitaTypes.No_choice -> MatitaTypes.error "no choice");
- addDebugItem "toggle auto disambiguation" (fun _ ->
- Helm_registry.set_bool "matita.auto_disambiguation"
- (not (Helm_registry.get_bool "matita.auto_disambiguation")))
+ addDebugItem "dump environment to \"env.dump\"" (fun _ ->
+ let oc = open_out "env.dump" in
+ CicEnvironment.dump_to_channel oc;
+ close_out oc);
+ addDebugItem "load environment from \"env.dump\"" (fun _ ->
+ let ic = open_in "env.dump" in
+ CicEnvironment.restore_from_channel ic;
+ close_in ic);
+ addDebugItem "dump universes" (fun _ ->
+ List.iter (fun (u,_,g) ->
+ prerr_endline (UriManager.string_of_uri u);
+ CicUniv.print_ugraph g) (CicEnvironment.list_obj ())
+ );
+ addDebugItem "print selected terms" (fun () ->
+ let i = ref 0 in
+ List.iter
+ (fun t ->
+ incr i;
+ MatitaLog.debug (sprintf "%d: %s" !i (CicPp.ppterm t)))
+ (MatitaMathView.sequentViewer_instance ())#get_selected_terms);
+ addDebugItem "dump getter settings" (fun _ ->
+ prerr_endline (Http_getter_env.env_to_string ()));
+ addDebugItem "getter: update"
+ (fun _ ->
+ ignore (Thread.create (fun () ->
+ MatitaLog.message "Rebuilding getter maps in background ...";
+ Http_getter.update ();
+ MatitaLog.message "Getter maps successfully rebuilt.") ()));
+ addDebugItem "getter: getalluris" (fun _ ->
+ List.iter prerr_endline (Http_getter.getalluris ()));
+ addDebugItem "dump script status" script#dump;
+ addDebugItem "dump metasenv"
+ (fun _ ->
+ if script#onGoingProof () then
+ MatitaLog.debug (CicMetaSubst.ppmetasenv script#proofMetasenv []));
+ addDebugItem "rotate light bulbs"
+ (fun _ ->
+ let nb = gui#main#hintNotebook in
+ nb#goto_page ((nb#current_page + 1) mod 3));
+ (*
+ addDebugItem "print (on stdout) \"statement\" grammar entry"
+ (fun _ ->
+ Grammar.print_entry Format.std_formatter
+ (Grammar.Entry.obj CicTextualParser2.statement);
+ Format.pp_print_flush Format.std_formatter ());*)