X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathita%2Fmathita.ml;h=f22a035a5537b5ffd2ad56fc8bd7a2259bc3daca;hb=07287062d5b84a0f2b66380d0d380bbf68217a27;hp=b1cfaddccd9c2e3026b4698a528563126d5dbd07;hpb=9c70cabfe7bcf809e746f2499902aa7f2f45ca6a;p=helm.git diff --git a/helm/mathita/mathita.ml b/helm/mathita/mathita.ml index b1cfaddcc..f22a035a5 100644 --- a/helm/mathita/mathita.ml +++ b/helm/mathita/mathita.ml @@ -26,14 +26,16 @@ exception Not_implemented of string let not_implemented feature = raise (Not_implemented feature) + (** exceptions whose content should be presented to the user *) +exception Failure of string +let error s = raise (Failure s) + let _ = Helm_registry.load_from "mathita.conf.xml" let _ = GMain.Main.init () let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file") -(* let interactive_user_uri_choice - ~selection_mode:[`MULTIPLE|`SINGLE] ?(ok="Ok") - ?(enable_button_for_non_vars=false) ~title ~msg + ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=false) ~title ~msg uris = let only_constant_choices = @@ -42,123 +44,53 @@ let interactive_user_uri_choice (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var")) uris) in - if selection_mode <> `SINGLE && !auto_disambiguation then + if (selection_mode <> `SINGLE) && + (Helm_registry.get_bool "mathita.auto_disambiguation") + then Lazy.force only_constant_choices else begin + let win = gui#uriChoice in let choices = ref [] in let chosen = ref false in let use_only_constants = ref false in - gui#uriChoice#uriChoiceDialog#set_title title; - gui#uriChoice#uriChoiceLabel#set_text msg; - FINQUI - - let clist = - let expected_height = 18 * List.length uris in - let height = if expected_height > 400 then 400 else expected_height in - GList.clist ~columns:1 ~packing:scrolled_window#add - ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in - let _ = List.map (function x -> clist#append [x]) uris in - let hbox2 = - GPack.hbox ~border_width:0 - ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in - let explain_label = - GMisc.label ~text:"None of the above. Try this one:" - ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in - let manual_input = - GEdit.entry ~editable:true - ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in - let hbox = - GPack.hbox ~border_width:0 ~packing:window#action_area#add () in - let okb = - GButton.button ~label:ok - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - let _ = okb#misc#set_sensitive false in - let nonvarsb = - GButton.button - ~packing: - (function w -> - if enable_button_for_non_vars then - hbox#pack ~expand:false ~fill:false ~padding:5 w) - ~label:"Try constants only" () in - let autob = - GButton.button - ~packing: - (fun w -> - if enable_button_for_non_vars then - hbox#pack ~expand:false ~fill:false ~padding:5 w) - ~label:"Auto" () in - let checkb = - GButton.button ~label:"Check" - ~packing:(hbox#pack ~padding:5) () in - let _ = checkb#misc#set_sensitive false in - let cancelb = - GButton.button ~label:"Abort" - ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in - (* actions *) - let check_callback () = - assert (List.length !choices > 0) ; - check_window !choices + win#uriChoiceDialog#set_title title; + win#uriChoiceLabel#set_text msg; + gui#uriChoices#list_store#clear (); + List.iter gui#uriChoices#easy_append uris; + win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; + let bye = ref (fun () -> ()) in + let id1 = + win#uriChoiceConstantsButton#connect#clicked (fun _ -> + use_only_constants := true; + !bye ()) in - ignore (window#connect#destroy GMain.Main.quit) ; - ignore (cancelb#connect#clicked window#destroy) ; - ignore - (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ; - ignore - (nonvarsb#connect#clicked - (function () -> - use_only_constants := true ; - chosen := true ; - window#destroy () - )) ; - ignore (autob#connect#clicked (fun () -> - auto_disambiguation := true; - (rendering_window ())#set_auto_disambiguation true; + let id2 = + win#uriChoiceAutoButton#connect#clicked (fun _ -> use_only_constants := true ; - chosen := true; - window#destroy ())); - ignore (checkb#connect#clicked check_callback) ; - ignore - (clist#connect#select_row - (fun ~row ~column ~event -> - checkb#misc#set_sensitive true ; - okb#misc#set_sensitive true ; - choices := (List.nth uris row)::!choices)) ; - ignore - (clist#connect#unselect_row - (fun ~row ~column ~event -> - choices := - List.filter (function uri -> uri != (List.nth uris row)) !choices)) ; - ignore - (manual_input#connect#changed - (fun _ -> - if manual_input#text = "" then - begin - choices := [] ; - checkb#misc#set_sensitive false ; - okb#misc#set_sensitive false ; - clist#misc#set_sensitive true - end - else - begin - choices := [manual_input#text] ; - clist#unselect_all () ; - checkb#misc#set_sensitive true ; - okb#misc#set_sensitive true ; - clist#misc#set_sensitive false - end)); - window#set_position `CENTER ; - window#show () ; - GtkThread.main (); - if !chosen then - if !use_only_constants then - Lazy.force only_constant_choices - else - if List.length !choices > 0 then !choices else raise NoChoice - else - raise NoChoice + Helm_registry.set_bool "mathita.auto_disambiguation" true; + !bye ()) + in + let id3 = + win#uriChoiceSelectedButton#connect#clicked (fun _ -> + choices := gui#uriChoices#easy_selection (); + !bye ()) + in + bye := (fun () -> + win#uriChoiceDialog#misc#hide (); + win#uriChoiceConstantsButton#misc#disconnect id1; + win#uriChoiceAutoButton#misc#disconnect id2; + win#uriChoiceSelectedButton#misc#disconnect id3; + prerr_endline "quit"; + GMain.Main.quit ()); + win#uriChoiceDialog#show (); + GtkThread.main (); + if !use_only_constants then + Lazy.force only_constant_choices + else + match !choices with + | [] -> error "No choice" + | choices -> choices end - ;; -*) (* module DisambiguateCallbacks = @@ -173,9 +105,50 @@ module DisambiguateCallbacks = end *) +let debugDialog () = + let dialog = + new MathitaGeneratedGui.debug + ~file:(Helm_registry.get "mathita.glade_file") () + in + let retval = ref None in + let return v = + retval := Some v; + dialog#debug#destroy (); + GMain.Main.quit () + in + ignore (dialog#debug#event#connect#delete (fun _ -> true)); + ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1)); + ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2)); + dialog#debug#show (); + GtkThread.main (); + (match !retval with None -> assert false | Some v -> v) + +let _ = + gui#main#debugMenuItem2#connect#activate (fun _ -> + prerr_endline (string_of_int (debugDialog ()))) + (** quit program, possibly asking for confirmation *) let quit () = GMain.Main.quit () let _ = gui#setQuitCallback quit +let _ = + gui#main#debugMenuItem0#connect#activate (fun _ -> + let uris = + interactive_user_uri_choice + ~selection_mode:`MULTIPLE + ~nonvars_button:false + ~title:"titolo" + ~msg:"messaggio" + ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con"; + "cic:/cinque.var"] + in + List.iter prerr_endline uris; print_newline ()) +let _ = + gui#main#debugMenuItem1#connect#activate (fun _ -> + Helm_registry.set_bool "mathita.auto_disambiguation" + (not (Helm_registry.get_bool "mathita.auto_disambiguation"))) -let _ = GtkThread.main () +let _ = +(* gui#uriChoices#easy_append "pippo"; *) +(* gui#uriChoices#list_store#clear (); *) + GtkThread.main ()