From d1f310f1f31b6919aa6e5ac6afd41b539130aec5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 18 Oct 2006 13:16:06 +0000 Subject: [PATCH] Dead dialog window removed. --- helm/software/matita/matitaGtkMisc.ml | 45 -------------------------- helm/software/matita/matitaGtkMisc.mli | 11 ------- 2 files changed, 56 deletions(-) diff --git a/helm/software/matita/matitaGtkMisc.ml b/helm/software/matita/matitaGtkMisc.ml index 6407ae35d..9c00dfdde 100644 --- a/helm/software/matita/matitaGtkMisc.ml +++ b/helm/software/matita/matitaGtkMisc.ml @@ -254,7 +254,6 @@ class recordModel (tree_view:GTree.view) = class type gui = object method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end @@ -395,50 +394,6 @@ let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false) GtkThread.main (); (match !result with None -> raise MatitaTypes.Cancel | Some r -> r) -let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "") - ~fields ~records () -= - let fields = Array.of_list fields in - let fields_no = Array.length fields in - assert (fields_no > 0); - let dialog = gui#newRecordDialog () in - dialog#recordChoiceDialog#set_title title; - dialog#recordChoiceDialogLabel#set_label message; - let model = new recordModel dialog#recordChoiceTreeView in - dialog#recordChoiceTreeView#set_headers_visible true; - let combos = - Array.init fields_no - (fun _ -> GTree.store_of_list Gobject.Data.string ["a"; "b"; "c"]) - in - let (store, col) = combos.(0) in - store#set ~row:(store#append ()) ~column:col "uno"; - store#set ~row:(store#append ()) ~column:col "due"; - let toggles = Array.init fields_no (fun _ -> false) in - Array.iteri - (fun i f -> model#easy_append f i toggles.(i)) - fields; - let record_no = ref None in - let return _ = - dialog#recordChoiceDialog#destroy (); - GMain.Main.quit () - in - let fail _ = record_no := None; return () in - ignore (dialog#recordChoiceDialog#event#connect#delete (fun _ -> true)); - connect_button dialog#recordChoiceOkButton (fun _ -> - match !record_no with None -> () | Some _ -> return ()); - connect_button dialog#recordChoiceCancelButton fail; -(* ignore (dialog#recordChoiceTreeView#connect#row_activated (fun path _ -> - interp_no := Some (model#get_interp_no path); - return ())); - let selection = dialog#recordChoiceTreeView#selection in - ignore (selection#connect#changed (fun _ -> - match selection#get_selected_rows with - | [path] -> interp_no := Some (model#get_interp_no path) - | _ -> assert false)); *) - dialog#recordChoiceDialog#show (); - GtkThread.main (); - (match !record_no with Some n -> n | _ -> raise MatitaTypes.Cancel) - let utf8_parsed_text s floc = let start, stop = HExtlib.loc_of_floc floc in let start_bytes = Glib.Utf8.offset_to_pos s ~pos:0 ~off:start in diff --git a/helm/software/matita/matitaGtkMisc.mli b/helm/software/matita/matitaGtkMisc.mli index 16b0591b2..40fc9373b 100644 --- a/helm/software/matita/matitaGtkMisc.mli +++ b/helm/software/matita/matitaGtkMisc.mli @@ -113,7 +113,6 @@ class taggedStringListModel: class type gui = object (* minimal gui object requirements *) method newUriDialog: unit -> MatitaGeneratedGui.uriChoiceDialog - method newRecordDialog: unit -> MatitaGeneratedGui.recordChoiceDialog method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog method newEmptyDialog: unit -> MatitaGeneratedGui.emptyDialog end @@ -139,16 +138,6 @@ val ask_text: ?multiline:bool -> ?default:string -> unit -> string - (** @param fields field names - * @param records list of records, each record is a list of [fields] strings - * @return number of the chosen record, 0 for the first one *) -val ask_record_choice: - gui:#gui -> - ?title:string -> ?message:string -> - fields:string list -> records:string list list -> - unit -> - int - val report_error: title:string -> message:string -> ?parent:#GWindow.window_skel -> -- 2.39.2