diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 35 | ||||
| -rw-r--r-- | ide/ideutils.ml | 2 | ||||
| -rw-r--r-- | ide/undo.ml | 4 | ||||
| -rw-r--r-- | ide/utils/configwin_ihm.ml | 4 |
4 files changed, 21 insertions, 24 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 956a275a9..48bb19cb6 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -807,7 +807,7 @@ object(self) goal_nb (if goal_nb<=1 then "" else "s")); List.iter - (fun ((_,_,_,(s,_)) as hyp) -> + (fun ((_,_,_,(s,_)) as _hyp) -> proof_buffer#insert (s^"\n")) hyps; proof_buffer#insert (String.make 38 '_' ^ "(1/"^ @@ -1364,7 +1364,6 @@ Please restart and report NOW."; if Mutex.try_lock c#lock then begin c#clear (); let current_gls = try get_current_goals () with _ -> [] in - let gls_nb = List.length current_gls in let set_goal i (s,t) = let gnb = string_of_int i in @@ -1481,19 +1480,17 @@ Please restart and report NOW."; (input_view#event#connect#key_press self#active_keypress_handler); prerr_endline "CONNECTED active : "; print_id (out_some act_id); - let dir = (match - (out_some ((Vector.get input_views index).analyzed_view)) - #filename - with - | None -> () - | Some f -> - if not (is_in_coq_path f) then - begin - let dir = Filename.dirname f in - ignore (Coq.interp false - (Printf.sprintf "Add LoadPath \"%s\". " dir)) - end) - in () + match + (out_some ((Vector.get input_views index).analyzed_view)) #filename + with + | None -> () + | Some f -> + if not (is_in_coq_path f) then + begin + let dir = Filename.dirname f in + ignore (Coq.interp false + (Printf.sprintf "Add LoadPath \"%s\". " dir)) + end @@ -1832,7 +1829,7 @@ let main files = let load_f () = match select_file ~title:"Load file" () with | None -> () - | (Some f) as fn -> load f + | Some f -> load f in ignore (load_m#connect#activate (load_f)); @@ -1906,7 +1903,7 @@ let main files = let saveall_f () = Vector.iter (function - | {view = view ; analyzed_view = Some av} as full -> + | {view = view ; analyzed_view = Some av} -> begin match av#filename with | None -> () | Some f -> @@ -1929,7 +1926,7 @@ let main files = let revert_f () = Vector.iter (function - {view = view ; analyzed_view = Some av} as full -> + {view = view ; analyzed_view = Some av} -> (try match av#filename,av#stats with | Some f,Some stats -> @@ -2359,7 +2356,7 @@ let main files = let auto_save_f () = Vector.iter (function - {view = view ; analyzed_view = Some av} as full -> + {view = view ; analyzed_view = Some av} -> (try av#auto_save with _ -> ()) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index e8cccf9cc..a71d14c82 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -228,7 +228,7 @@ let rec print_list print fmt = function let browse f url = let l,r = !current.cmd_browse in - let (s,res) = System.run_command try_convert f (l ^ url ^ r) in + let _ = System.run_command try_convert f (l ^ url ^ r) in () let url_for_keyword = diff --git a/ide/undo.ml b/ide/undo.ml index dc723db9d..0b4ea1726 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -107,8 +107,8 @@ object(self) Queue.iter (fun e -> Stack.push e history) redo; Queue.clear redo; end; - let pos = it#offset in -(* if Stack.is_empty history or +(* let pos = it#offset in + if Stack.is_empty history or s=" " or s="\t" or s="\n" or (match Stack.top history with | Insert(old,opos,olen) -> diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index 03ca706c8..275a730b6 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -560,8 +560,8 @@ class font_param_box param = let _ = dialog#connect#destroy GMain.Main.quit in let _ = wb_ok#connect#clicked (fun () -> - let font_opt = dialog#selection#font_name in -(* we#set_text (match font_opt with None -> "" | Some s -> s) ; +(* let font_opt = dialog#selection#font_name in + we#set_text (match font_opt with None -> "" | Some s -> s) ; set_entry_font font_opt;*) dialog#destroy () ) |