- 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 MatitaGtkMisc.Cancel -> 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 "mono line text input" (fun _ ->
- prerr_endline (ask_text ~gui ~title:"title" ~msg:"message" ()));
- addDebugItem "multi line text input" (fun _ ->
- prerr_endline
- (ask_text ~gui ~title:"title" ~multiline:true ~msg:"message" ()));
- addDebugItem "dump proof status to stdout" (fun _ ->
- print_endline ((get_proof ())#toString));
+ 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 "dump environment content" (fun _ ->
+ List.iter (fun (u,_,_) ->
+ prerr_endline (UriManager.string_of_uri u))
+ (CicEnvironment.list_obj ()));
+(* addDebugItem "print selections" (fun () ->
+ let cicMathView = MatitaMathView.cicMathView_instance () in
+ 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
+ HLog.debug (CicMetaSubst.ppmetasenv [] script#proofMetasenv));
+ addDebugItem "dump coercions Db" (fun _ ->
+ List.iter
+ (fun (s,t,u) ->
+ HLog.debug
+ (UriManager.name_of_uri u ^ ":"
+ ^ CoercDb.name_of_carr s ^ " -> " ^ CoercDb.name_of_carr t))
+ (CoercDb.to_list ()));
+ addDebugItem "print top-level grammar entries"
+ CicNotationParser.print_l2_pattern;
+ addDebugItem "dump moo to stderr" (fun _ ->
+ let grafite_status = (MatitaScript.current ())#grafite_status in
+ let moo = grafite_status.moo_content_rev in
+ List.iter
+ (fun cmd ->
+ prerr_endline (GrafiteAstPp.pp_command ~obj_pp:(fun _ -> assert false)
+ cmd))
+ (List.rev moo));
+ addDebugItem "print metasenv goals and stack to stderr"
+ (fun _ ->
+ prerr_endline ("metasenv goals: " ^ String.concat " "
+ (List.map (fun (g, _, _) -> string_of_int g)
+ (MatitaScript.current ())#proofMetasenv));
+ prerr_endline ("stack: " ^ Continuationals.Stack.pp
+ (GrafiteTypes.get_stack (MatitaScript.current ())#grafite_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 ())));