added comments, fixed history, added loadList to browser

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index ec4d042ff38223eb61cd6151c84b7f19171c8d99..5045f36d1aa5148bd3ec80c2f3c3a7fa4b46ed26 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -63,7 +63,8 @@ class gui () =
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
-
+    val mutable script_fname = None 
+   
     initializer
         (* glade's check widgets *)
       List.iter (fun w -> w#check_widgets ())
@@ -155,33 +156,37 @@ class gui () =
              (sprintf "Uncaught exception: %s" (Printexc.to_string exn)));
         (* script *)
       let s () = MatitaScript.instance () in
-      let script_fname = ref None in
-      let enable_save_to f =
-        script_fname := Some f;
-        self#main#saveMenuItem#misc#set_sensitive true
-      in
-      let disable_save () =
-        script_fname := None;
+      let disableSave () =
+        script_fname <- None;
         self#main#saveMenuItem#misc#set_sensitive false
       in
       let loadScript () =
         let script = s () in
         match self#chooseFile () with
-        | Some f -> script#reset (); script#loadFrom f; enable_save_to f
+        | Some f -> 
+              script#reset (); 
+              script#loadFrom f; 
+              console#message ("'"^f^"' loaded.");
+              self#_enableSaveTo f
         | None -> ()
       in
       let saveAsScript () =
         let script = s () in
         match self#chooseFile ~ok_not_exists:true () with
-        | Some f -> script#saveTo f; enable_save_to f
+        | Some f -> 
+              script#saveTo f; 
+              console#message ("'"^f^"' saved.");
+              self#_enableSaveTo f
         | None -> ()
       in
       let saveScript () =
-        match !script_fname with
+        match script_fname with
         | None -> saveAsScript ()
-        | Some f -> (s ())#saveTo f
+        | Some f -> 
+              (s ())#saveTo f;
+              console#message ("'"^f^"' saved.");
       in
-      let newScript () = (s ())#reset (); disable_save () in
+      let newScript () = (s ())#reset (); disableSave () in
       let cursor () =
         let buf = self#main#scriptTextView#buffer in
         buf#place_cursor (buf#get_iter_at_mark (`NAME "locked"))
@@ -228,6 +233,18 @@ class gui () =
       self#main#hintHighImage#set_file "icons/matita-bulb-high.png";
         (* focus *)
       self#main#scriptTextView#misc#grab_focus ()
+    
+    method loadScript file =       
+      let script = MatitaScript.instance () in
+      script#reset (); 
+      script#loadFrom file; 
+      console#message ("'"^file^"' loaded.");
+      self#_enableSaveTo file
+        
+    method private _enableSaveTo file =
+      script_fname <- Some file;
+      self#main#saveMenuItem#misc#set_sensitive true
+        
 
     method console = console
 
@@ -237,6 +254,30 @@ class gui () =
 
     method newBrowserWin () =
       let win = new browserWin () in
+      win#whelpImage2#set_file "icons/whelp.png";
+      win#whelpBarToggleButton#set_active false;   
+      win#whelpBarBox#misc#hide ();
+      win#mathOrListNotebook#set_show_tabs false;
+      connect_toggle_button win#whelpBarToggleButton 
+        (fun () -> 
+          if win#whelpBarToggleButton#active then
+            win#whelpBarBox#misc#show ()
+          else
+            win#whelpBarBox#misc#hide ());
+      let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in
+      let combo,(combo_store,combo_column) = 
+        GEdit.combo_box_text ~strings:queries () 
+      in
+      combo#set_active 0;
+      win#comboVbox#add (combo :> GObj.widget);
+      let start_query () = 
+        let query = String.lowercase (List.nth queries combo#active) in
+        let input = win#queryInputText#text in
+        let statement = "whelp " ^ query ^ " " ^ input ^ "." in
+        (MatitaScript.instance ())#advance ~statement ()
+      in
+      ignore(win#queryInputText#connect#activate ~callback:start_query);
+      ignore(combo#connect#changed ~callback:start_query);
       win#check_widgets ();
       win
 
@@ -312,7 +353,8 @@ let is_var_uri s =
 
 let interactive_uri_choice
   ?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
-  ?(msg = "") ?(nonvars_button = false) ()
+  ?(msg = "") ?(nonvars_button = false) ?(hide_uri_entry=false) 
+  ?(hide_try=false) ?(ok_label="_Auto") ?copy_cb ()
   ~id uris
 =
   let gui = instance () in
@@ -323,11 +365,28 @@ let interactive_uri_choice
     Lazy.force nonvars_uris
   else begin
     let dialog = gui#newUriDialog () in
+    if hide_uri_entry then
+      dialog#uriEntryHBox#misc#hide ();
+    if hide_try then
+      begin
+      dialog#uriChoiceSelectedButton#misc#hide ();
+      dialog#uriChoiceConstantsButton#misc#hide ();
+      end;
+    dialog#okLabel#set_label ok_label;  
     dialog#uriChoiceTreeView#selection#set_mode
       (selection_mode :> Gtk.Tags.selection_mode);
     let model = new stringListModel dialog#uriChoiceTreeView in
     let choices = ref None in
     let nonvars = ref false in
+    (match copy_cb with
+    | None -> ()
+    | Some cb ->
+        dialog#copyButton#misc#show ();
+        connect_button dialog#copyButton 
+        (fun _ ->
+          match model#easy_selection () with
+          | [u] -> (cb u)
+          | _ -> ()));
     dialog#uriChoiceDialog#set_title title;
     dialog#uriChoiceLabel#set_text msg;
     List.iter model#easy_append uris;