]> matita.cs.unibo.it Git - helm.git/commitdiff
Dead dialog window removed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Oct 2006 13:16:06 +0000 (13:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 18 Oct 2006 13:16:06 +0000 (13:16 +0000)
matita/matitaGtkMisc.ml
matita/matitaGtkMisc.mli

index 6407ae35d1e8654fb89022b574704f50fea84422..9c00dfddef4aa1b7879026c85e12fa1df0c3700d 100644 (file)
@@ -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
index 16b0591b2651a5a09856f5bdfad0c192c66d9c58..40fc9373bd68f7fd4aadb7dc757228af8235f640 100644 (file)
@@ -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 ->