X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGtkMisc.ml;h=553406635aac812e87ba39576f566bbe747f1e08;hb=be5869cd0bbe16c8a67827723c97d2d4fce4c0bc;hp=3c0d1b4c359ba15ba418b70f1cd74585a6d27484;hpb=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git

diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml
index 3c0d1b4c3..553406635 100644
--- a/helm/matita/matitaGtkMisc.ml
+++ b/helm/matita/matitaGtkMisc.ml
@@ -23,11 +23,11 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 exception PopupClosed
 open Printf
 
-open MatitaTypes
-
 let wrap_callback f = f
 
 let connect_button (button: #GButton.button) callback =
@@ -340,7 +340,6 @@ let ask_confirmation ~title ~message ?parent () =
     !rc
 
 let report_error ~title ~message ?parent () =
-  let rc = ref false in
   let callback _ = () in
   let buttons = GWindow.Buttons.ok in
   try 
@@ -392,9 +391,7 @@ let ask_text ~(gui:#gui) ?(title = "") ?(message = "") ?(multiline = false)
   connect_button dialog#emptyDialogCancelButton (fun _ ->return None);
   dialog#emptyDialog#show ();
   GtkThread.main ();
-  (match !result with None -> raise Cancel | Some r -> r)
-
-type combo_status = Free of string | Locked of string
+  (match !result with None -> raise MatitaTypes.Cancel | Some r -> r)
 
 let ask_record_choice ~(gui:#gui) ?(title= "") ?(message = "")
   ~fields ~records ()
@@ -418,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 ();