- 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")))
+ 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" ()));