X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=553406635aac812e87ba39576f566bbe747f1e08;hb=112afe13b5aef27425d1a0bc9c71a70b491069bf;hp=619c1eadbbd5e229f3394baf883fc3b3a8367ecc;hpb=ebe70c001a623e0440f21cd16dc88f585edcf0ea;p=helm.git diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml index 619c1eadb..553406635 100644 --- a/helm/matita/matitaGtkMisc.ml +++ b/helm/matita/matitaGtkMisc.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + exception PopupClosed open Printf @@ -391,8 +393,6 @@ let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false) GtkThread.main (); (match !result with None -> raise MatitaTypes.Cancel | Some r -> r) -type combo_status = Free of string | Locked of string - let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "") ~fields ~records () = @@ -415,7 +415,6 @@ let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "") Array.iteri (fun i f -> model#easy_append f i toggles.(i)) fields; - let status = Array.map (fun s -> Free s) fields in let record_no = ref None in let return _ = dialog#recordChoiceDialog#destroy ();