X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaGtkMisc.ml;h=9c00dfddef4aa1b7879026c85e12fa1df0c3700d;hb=b2abc81f0b76224f6f4f526feaf1fefd6178ae7d;hp=6407ae35d1e8654fb89022b574704f50fea84422;hpb=cbcd34fe15122eb9835a5226b98be1050b097d6a;p=helm.git

diff --git a/matita/matitaGtkMisc.ml b/matita/matitaGtkMisc.ml
index 6407ae35d..9c00dfdde 100644
--- a/matita/matitaGtkMisc.ml
+++ b/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