From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 19 Jan 2006 22:34:29 +0000 Subject: Imported Upstream version 8.0pl3 --- ide/coq.ico | Bin 0 -> 96774 bytes ide/coq.ml | 6 +- ide/coq2.ico | Bin 0 -> 1526 bytes ide/coqide.ml | 448 ++++++++++++++++++++++------------------------ ide/ideutils.ml | 22 ++- ide/ideutils.mli | 5 +- ide/undo.ml | 4 +- ide/undo.mli | 35 ---- ide/undo_lablgtk_ge26.mli | 35 ++++ ide/undo_lablgtk_lt26.mli | 35 ++++ 10 files changed, 306 insertions(+), 284 deletions(-) create mode 100644 ide/coq.ico create mode 100755 ide/coq2.ico delete mode 100644 ide/undo.mli create mode 100644 ide/undo_lablgtk_ge26.mli create mode 100644 ide/undo_lablgtk_lt26.mli (limited to 'ide') diff --git a/ide/coq.ico b/ide/coq.ico new file mode 100644 index 00000000..390065bc Binary files /dev/null and b/ide/coq.ico differ diff --git a/ide/coq.ml b/ide/coq.ml index e582f2d9..31f9829b 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq.ml,v 1.38.2.1 2004/07/16 19:30:20 herbelin Exp $ *) +(* $Id: coq.ml,v 1.38.2.2 2005/11/16 17:22:38 barras Exp $ *) open Vernac open Vernacexpr @@ -95,10 +95,10 @@ let is_in_coq_path f = let _ = Library.locate_qualified_library (Libnames.make_qualid Names.empty_dirpath (Names.id_of_string base)) in - prerr_endline (f ^ "is in coq path"); + prerr_endline (f ^ " is in coq path"); true with _ -> - prerr_endline (f ^ "is NOT in coq path"); + prerr_endline (f ^ " is NOT in coq path"); false let is_in_proof_mode () = diff --git a/ide/coq2.ico b/ide/coq2.ico new file mode 100755 index 00000000..36964902 Binary files /dev/null and b/ide/coq2.ico differ diff --git a/ide/coqide.ml b/ide/coqide.ml index 08994010..a8179fb9 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml,v 1.99.2.3 2004/10/15 14:50:12 coq Exp $ *) +(* $Id: coqide.ml,v 1.99.2.6 2006/01/06 13:22:36 barras Exp $ *) open Preferences open Vernacexpr @@ -247,50 +247,43 @@ let break () = prerr_endline " ignored (not computing)" end -let full_do_if_not_computing text f x = - ignore - (Thread.create - (async - (fun () -> - if Mutex.try_lock coq_computing - then - begin - prerr_endline ("Launching thread " ^ text); - let w = Blaster_window.blaster_window () in - if not (Mutex.try_lock w#lock) then begin - break (); - let lck = Mutex.create () in - Mutex.lock lck; - prerr_endline "Waiting on blaster..."; - Condition.wait w#blaster_killed lck; - prerr_endline "Waiting on blaster ok"; - Mutex.unlock lck - end else Mutex.unlock w#lock; - let idle = - Glib.Timeout.add ~ms:300 - ~callback:(fun () -> !pulse ();true) in - begin - prerr_endline "Getting lock"; - try - f x; - Glib.Timeout.remove idle; - prerr_endline "Releasing lock"; - Mutex.unlock coq_computing; - with e -> - Glib.Timeout.remove idle; - prerr_endline "Releasing lock (on error)"; - Mutex.unlock coq_computing; - raise e - end - end - else - prerr_endline - "Discarded order (computations are ongoing)")) - ()) - let do_if_not_computing text f x = - ignore (full_do_if_not_computing text f x) - + let threaded_task () = + if Mutex.try_lock coq_computing + then + begin + prerr_endline ("Launching thread " ^ text); + let w = Blaster_window.blaster_window () in + if not (Mutex.try_lock w#lock) then begin + break (); + let lck = Mutex.create () in + Mutex.lock lck; + prerr_endline "Waiting on blaster..."; + Condition.wait w#blaster_killed lck; + prerr_endline "Waiting on blaster ok"; + Mutex.unlock lck + end else Mutex.unlock w#lock; + let idle = + Glib.Timeout.add ~ms:300 + ~callback:(fun () -> async !pulse ();true) in + begin + prerr_endline "Getting lock"; + try + f x; + Glib.Timeout.remove idle; + prerr_endline "Releasing lock"; + Mutex.unlock coq_computing; + with e -> + Glib.Timeout.remove idle; + prerr_endline "Releasing lock (on error)"; + Mutex.unlock coq_computing; + raise e + end + end + else + prerr_endline + "Discarded order (computations are ongoing)" in + ignore (Thread.create threaded_task ()) let add_input_view tv = Vector.append input_views tv @@ -948,27 +941,9 @@ object(self) end method send_to_coq verbosely replace phrase show_output show_error localize = - try - full_goal_done <- false; - prerr_endline "Send_to_coq starting now"; - if replace then begin - let r,info = -(* full_do_if_not_computing "coq eval and replace" *) - Coq.interp_and_replace ("Info " ^ phrase) - in - let msg = read_stdout () in - self#insert_message (if show_output then msg else ""); - - Some r - - end else begin - let r = Some (Coq.interp verbosely phrase) in - let msg = read_stdout () in - self#insert_message (if show_output then msg else ""); - r - end - with e -> - (if show_error then + let display_output msg = + self#insert_message (if show_output then msg else "") in + let display_error e = let (s,loc) = Coq.process_exn e in assert (Glib.Utf8.validate s); self#set_message s; @@ -986,8 +961,23 @@ object(self) input_buffer#apply_tag_by_name "error" ~start:starti ~stop:stopi; - input_buffer#place_cursor starti; - )); + input_buffer#place_cursor starti) in + try + full_goal_done <- false; + prerr_endline "Send_to_coq starting now"; + if replace then begin + let r,info = Coq.interp_and_replace ("info " ^ phrase) in + let msg = read_stdout () in + sync display_output msg; + Some r + end else begin + let r = Coq.interp verbosely phrase in + let msg = read_stdout () in + sync display_output msg; + Some r + end + with e -> + if show_error then sync display_error e; None method find_phrase_starting_at (start:GText.iter) = @@ -1068,149 +1058,148 @@ object(self) method process_next_phrase verbosely display_goals do_highlight = - begin - try - self#clear_message; - prerr_endline "process_next_phrase starting now"; - if do_highlight then begin - !push_info "Coq is computing"; - input_view#set_editable false; - end; - begin match (self#find_phrase_starting_at self#get_start_of_input) - with - | None -> + let get_next_phrase () = + self#clear_message; + prerr_endline "process_next_phrase starting now"; + if do_highlight then begin + !push_info "Coq is computing"; + input_view#set_editable false; + end; + match self#find_phrase_starting_at self#get_start_of_input with + | None -> if do_highlight then begin input_view#set_editable true; !pop_info (); - end; false + end; + None | Some(start,stop) -> prerr_endline "process_next_phrase : to_process highlight"; - let b = input_buffer in if do_highlight then begin input_buffer#apply_tag_by_name ~start ~stop "to_process"; prerr_endline "process_next_phrase : to_process applied"; end; prerr_endline "process_next_phrase : getting phrase"; - let phrase = start#get_slice ~stop in - let r = - match self#send_to_coq verbosely false phrase true true true with - | Some ast -> - begin - b#move_mark ~where:stop (`NAME "start_of_input"); - b#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - begin - b#place_cursor stop; - self#recenter_insert - end; - let start_of_phrase_mark = `MARK (b#create_mark start) in - let end_of_phrase_mark = `MARK (b#create_mark stop) in - push_phrase - start_of_phrase_mark - end_of_phrase_mark ast; - if display_goals then self#show_goals; - true - end - | None -> false - in - if do_highlight then begin - b#remove_tag_by_name ~start ~stop "to_process" ; - input_view#set_editable true; - !pop_info (); - end; - r; - end - with e -> raise e + Some((start,stop),start#get_slice ~stop) in + let remove_tag (start,stop) = + if do_highlight then begin + input_buffer#remove_tag_by_name ~start ~stop "to_process" ; + input_view#set_editable true; + !pop_info (); + end in + let mark_processed (start,stop) ast = + let b = input_buffer in + b#move_mark ~where:stop (`NAME "start_of_input"); + b#apply_tag_by_name "processed" ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + begin + b#place_cursor stop; + self#recenter_insert + end; + let start_of_phrase_mark = `MARK (b#create_mark start) in + let end_of_phrase_mark = `MARK (b#create_mark stop) in + push_phrase + start_of_phrase_mark + end_of_phrase_mark ast; + if display_goals then self#show_goals; + remove_tag (start,stop) in + begin + match sync get_next_phrase () with + | None -> false + | Some (loc,phrase) -> + (match self#send_to_coq verbosely false phrase true true true with + | Some ast -> sync (mark_processed loc) ast; true + | None -> sync remove_tag loc; false) end method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = - match self#send_to_coq false false coqphrase show_output show_msg localize with - | Some ast -> - begin - let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop insertphrase - else input_buffer#insert ~iter:stop ("\n"^insertphrase); - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME "start_of_input"); - input_buffer#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - input_buffer#place_cursor stop; - let start_of_phrase_mark = `MARK (input_buffer#create_mark start) - in - let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast; - self#show_goals; - (*Auto insert save on success... - try (match Coq.get_current_goals () with - | [] -> + let mark_processed ast = + let stop = self#get_start_of_input in + if stop#starts_line then + input_buffer#insert ~iter:stop insertphrase + else input_buffer#insert ~iter:stop ("\n"^insertphrase); + let start = self#get_start_of_input in + input_buffer#move_mark ~where:stop (`NAME "start_of_input"); + input_buffer#apply_tag_by_name "processed" ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + input_buffer#place_cursor stop; + let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in + let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in + push_phrase start_of_phrase_mark end_of_phrase_mark ast; + self#show_goals; + (*Auto insert save on success... + try (match Coq.get_current_goals () with + | [] -> (match self#send_to_coq "Save.\n" true true true with | Some ast -> - begin - let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop "Save.\n" - else input_buffer#insert ~iter:stop "\nSave.\n"; - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME "start_of_input"); - input_buffer#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - input_buffer#place_cursor stop; - let start_of_phrase_mark = `MARK (input_buffer#create_mark start) - in - let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast - end + begin + let stop = self#get_start_of_input in + if stop#starts_line then + input_buffer#insert ~iter:stop "Save.\n" + else input_buffer#insert ~iter:stop "\nSave.\n"; + let start = self#get_start_of_input in + input_buffer#move_mark ~where:stop (`NAME "start_of_input"); + input_buffer#apply_tag_by_name "processed" ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + input_buffer#place_cursor stop; + let start_of_phrase_mark = + `MARK (input_buffer#create_mark start) in + let end_of_phrase_mark = + `MARK (input_buffer#create_mark stop) in + push_phrase start_of_phrase_mark end_of_phrase_mark ast + end | None -> ()) - | _ -> ()) - with _ -> ()*) - true - end - | None -> self#insert_message ("Unsuccessfully tried: "^coqphrase); + | _ -> ()) + with _ -> ()*) in + match self#send_to_coq false false coqphrase show_output show_msg localize with + | Some ast -> sync mark_processed ast; true + | None -> + sync + (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) + (); false method process_until_iter_or_error stop = let stop' = `OFFSET stop#offset in let start = self#get_start_of_input#copy in let start' = `OFFSET start#offset in - input_buffer#apply_tag_by_name - ~start - ~stop - "to_process"; - input_view#set_editable false; + sync (fun _ -> + input_buffer#apply_tag_by_name ~start ~stop "to_process"; + input_view#set_editable false) (); !push_info "Coq is computing"; - process_pending (); +(* process_pending ();*) (try while ((stop#compare self#get_start_of_input>=0) && (self#process_next_phrase false false false)) do Util.check_for_interrupt () done with Sys.Break -> prerr_endline "Interrupted during process_until_iter_or_error"); - self#show_goals; - (* Start and stop might be invalid if an eol was added at eof *) - let start = input_buffer#get_iter start' in - let stop = input_buffer#get_iter stop' in - input_buffer#remove_tag_by_name ~start ~stop "to_process" ; - input_view#set_editable true; + sync (fun _ -> + self#show_goals; + (* Start and stop might be invalid if an eol was added at eof *) + let start = input_buffer#get_iter start' in + let stop = input_buffer#get_iter stop' in + input_buffer#remove_tag_by_name ~start ~stop "to_process" ; + input_view#set_editable true) (); !pop_info() method process_until_end_or_error = self#process_until_iter_or_error input_buffer#end_iter method reset_initial = - Stack.iter - (function inf -> - let start = input_buffer#get_iter_at_mark inf.start in - let stop = input_buffer#get_iter_at_mark inf.stop in - input_buffer#move_mark ~where:start (`NAME "start_of_input"); - input_buffer#remove_tag_by_name "processed" ~start ~stop; - input_buffer#delete_mark inf.start; - input_buffer#delete_mark inf.stop; - ) - processed_stack; - Stack.clear processed_stack; - self#clear_message; + sync (fun _ -> + Stack.iter + (function inf -> + let start = input_buffer#get_iter_at_mark inf.start in + let stop = input_buffer#get_iter_at_mark inf.stop in + input_buffer#move_mark ~where:start (`NAME "start_of_input"); + input_buffer#remove_tag_by_name "processed" ~start ~stop; + input_buffer#delete_mark inf.start; + input_buffer#delete_mark inf.stop; + ) + processed_stack; + Stack.clear processed_stack; + self#clear_message) (); Coq.reset_initial () @@ -1260,19 +1249,21 @@ object(self) (match undos with | None -> synchro () | Some n -> try Pfedit.undo n with _ -> synchro ()); - let start = if is_empty () then input_buffer#start_iter - else input_buffer#get_iter_at_mark (top ()).stop - in - prerr_endline "Removing (long) processed tag..."; - input_buffer#remove_tag_by_name - ~start - ~stop:self#get_start_of_input - "processed"; - prerr_endline "Moving (long) start_of_input..."; - input_buffer#move_mark ~where:start (`NAME "start_of_input"); - self#show_goals; - clear_stdout (); - self#clear_message; + sync (fun _ -> + let start = if is_empty () then input_buffer#start_iter + else input_buffer#get_iter_at_mark (top ()).stop + in + prerr_endline "Removing (long) processed tag..."; + input_buffer#remove_tag_by_name + ~start + ~stop:self#get_start_of_input + "processed"; + prerr_endline "Moving (long) start_of_input..."; + input_buffer#move_mark ~where:start (`NAME "start_of_input"); + self#show_goals; + clear_stdout (); + self#clear_message) + (); with _ -> !push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. Please restart and report NOW."; @@ -1315,7 +1306,7 @@ Please restart and report NOW."; begin match last_command with | {ast=_, (VernacSolve _ | VernacTime (VernacSolve _))} -> begin - try Pfedit.undo 1; ignore (pop ()); update_input () + try Pfedit.undo 1; ignore (pop ()); sync update_input () with _ -> self#backtrack_to_no_lock start end | {ast=_,t;reset_info=Reset (id, {contents=true})} -> @@ -1326,7 +1317,7 @@ Please restart and report NOW."; | VernacEndSegment _ -> reset_to_mod id | _ -> reset_to id); - update_input () + sync update_input () | { ast = _, ( VernacStartTheoremProof _ | VernacGoal _ | VernacDeclareTacticDefinition _ @@ -1340,10 +1331,10 @@ Please restart and report NOW."; prerr_endline "WARNING : found a closed environment"; raise e end); - update_input () + sync update_input () | { ast = (_, a) } when is_state_preserving a -> ignore (pop ()); - update_input () + sync update_input () | _ -> self#backtrack_to_no_lock start end; @@ -1356,7 +1347,6 @@ Please restart and report NOW."; method blaster () = - ignore (Thread.create (fun () -> prerr_endline "Blaster called"; @@ -1375,14 +1365,14 @@ Please restart and report NOW."; ("Goal "^gnb) s (fun () -> try_interptac t') - (fun () -> self#insert_command t'' t'') + (sync(fun () -> self#insert_command t'' t'')) in let set_current_goal (s,t) = c#set "Goal 1" s (fun () -> try_interptac ("progress "^t)) - (fun () -> self#insert_command t t) + (sync(fun () -> self#insert_command t t)) in begin match current_gls with | [] -> () @@ -1405,11 +1395,11 @@ Please restart and report NOW."; ()) method insert_command cp ip = - self#clear_message; + async(fun _ -> self#clear_message)(); ignore (self#insert_this_phrase_on_success true false false cp ip) method tactic_wizard l = - self#clear_message; + async(fun _ -> self#clear_message)(); ignore (List.exists (fun p -> @@ -1742,11 +1732,11 @@ let main files = ~width:!current.window_width ~height:!current.window_height ~title:"CoqIde" () in -(* - let icon_image = Filename.concat lib_ide "coq.ico" in - let icon = GdkPixbuf.from_file icon_image in - w#set_icon (Some icon); -*) + (try + let icon_image = lib_ide_file "coq2.ico" in + let icon = GdkPixbuf.from_file icon_image in + w#set_icon (Some icon) + with _ -> ()); let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in @@ -2064,21 +2054,21 @@ let main files = ignore (get_current_view()).view#clear_undo)); ignore(edit_f#add_separator ()); ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback: - (do_if_not_computing "cut" + (do_if_not_computing "cut" (sync (fun () -> GtkSignal.emit_unit (get_current_view()).view#as_view - GtkText.View.S.cut_clipboard))); + GtkText.View.S.cut_clipboard)))); ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback: (fun () -> GtkSignal.emit_unit (get_current_view()).view#as_view GtkText.View.S.copy_clipboard)); ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback: - (do_if_not_computing "paste" + (do_if_not_computing "paste" (sync (fun () -> try GtkSignal.emit_unit (get_current_view()).view#as_view GtkText.View.S.paste_clipboard - with _ -> prerr_endline "EMIT PASTE FAILED"))); + with _ -> prerr_endline "EMIT PASTE FAILED")))); ignore (edit_f#add_separator ()); @@ -2322,12 +2312,12 @@ let main files = *) ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback: - (do_if_not_computing "complete word" + (do_if_not_computing "complete word" (sync (fun () -> ignore ( let av = out_some ((get_current_view()).analyzed_view) in av#complete_at_offset (av#get_insert)#offset - )))); + ))))); ignore(edit_f#add_separator ()); (* external editor *) @@ -2352,7 +2342,7 @@ let main files = (GMain.Timeout.add ~ms:!current.global_auto_revert_delay ~callback: (fun () -> - do_if_not_computing "revert" (fun () -> revert_f ()) (); + do_if_not_computing "revert" (sync revert_f) (); true)) in reset_revert_timer (); (* to enable statup preferences timer *) @@ -2375,7 +2365,7 @@ let main files = (GMain.Timeout.add ~ms:!current.auto_save_delay ~callback: (fun () -> - do_if_not_computing "autosave" (fun () -> auto_save_f ()) (); + do_if_not_computing "autosave" (sync auto_save_f) (); true)) in reset_auto_save_timer (); (* to enable statup preferences timer *) @@ -2444,20 +2434,6 @@ let main files = ~key:GdkKeysyms._Up ~callback:(do_or_activate (fun a -> a#undo_last_step)) `GO_UP; -(* - add_to_menu_toolbar - "_Forward to" - ~tooltip:"Forward to" - ~key:GdkKeysyms._Right - ~callback:(do_or_activate (fun a -> a#process_until_insert_or_error)) - `GOTO_LAST; - add_to_menu_toolbar - "_Backward to" - ~tooltip:"Backward to" - ~key:GdkKeysyms._Left - ~callback:(do_or_activate (fun a-> a#backtrack_to_insert)) - `GOTO_FIRST; -*) add_to_menu_toolbar "_Go to" ~tooltip:"Go to cursor" @@ -2581,9 +2557,9 @@ let main files = in ignore (factory#add_item menu_text ~callback: - (do_if_not_computing "simple template" + (do_if_not_computing "simple template" (sync (fun () -> let {view = view } = get_current_view () in - ignore (view#buffer#insert_interactive text)))) + ignore (view#buffer#insert_interactive text))))) in List.iter (fun l -> @@ -2616,7 +2592,7 @@ let main files = in let add_complex_template (menu_text, text, offset, len, key) = (* Templates/Lemma *) - let callback = do_if_not_computing "complex template" + let callback = do_if_not_computing "complex template" (sync (fun () -> let {view = view } = get_current_view () in if view#buffer#insert_interactive text then begin @@ -2625,7 +2601,7 @@ let main files = view#buffer#move_mark `INSERT iter; ignore (iter#nocopy#backward_chars len); view#buffer#move_mark `SEL_BOUND iter; - end) + end)) in ignore (templates_factory#add_item menu_text ~callback ?key) in @@ -2695,9 +2671,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in ignore (factory#add_item menu_text ~callback: - (do_if_not_computing "simple template" + (do_if_not_computing "simple template" (sync (fun () -> let {view = view } = get_current_view () in - ignore (view#buffer#insert_interactive text)))) + ignore (view#buffer#insert_interactive text))))) in *) ignore (templates_factory#add_separator ()); @@ -2897,7 +2873,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let detach_menu = configuration_factory#add_item "Detach _Script Window" ~callback: - (do_if_not_computing "detach script window" + (do_if_not_computing "detach script window" (sync (fun () -> let nb = notebook () in if nb#misc#toplevel#get_oid=w#coerce#get_oid then @@ -2910,7 +2886,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); nw#add_accel_group accel_group; nb#misc#reparent nw#coerce end - )) + ))) in let detach_current_view = configuration_factory#add_item @@ -3208,7 +3184,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let _ = tv2#event#connect#motion_notify ~callback: (fun e -> - (do_if_not_computing "motion notify" + (do_if_not_computing "motion notify" (sync (fun e -> let win = match tv2#get_window `WIDGET with | None -> assert false @@ -3231,7 +3207,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); it#as_iter)) tags; false)) e; - false) + false)) in change_font := (fun fd -> @@ -3243,7 +3219,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ); let about (b:GText.buffer) = (try - let image = Filename.concat lib_ide "coq.png" in + let image = lib_ide_file "coq.ico" in let startup_image = GdkPixbuf.from_file image in b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; @@ -3291,7 +3267,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* ignore (faq_m#connect#activate ~callback:(fun () -> - load (Filename.concat lib_ide "FAQ"))); + load (lib_ide_file "FAQ"))); *) resize_window := (fun () -> @@ -3360,7 +3336,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let start () = let files = Coq.init () in ignore_break (); - GtkMain.Rc.add_default_file (Filename.concat lib_ide ".coqide-gtk2rc"); + GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc"); (try GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc"); with Not_found -> ()); diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 8ec0e9e4..dc3bcf71 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ideutils.ml,v 1.30.2.1 2004/07/16 19:30:20 herbelin Exp $ *) +(* $Id: ideutils.ml,v 1.30.2.4 2006/01/06 15:40:37 barras Exp $ *) open Preferences @@ -32,7 +32,12 @@ let prerr_endline s = let prerr_string s = if !debug then (prerr_string s;flush stderr) -let lib_ide = Filename.concat Coq_config.coqlib "ide" +let lib_ide_file f = + let coqlib = + if !Options.boot then Coq_config.coqtop + else + System.getenv_else "COQLIB" Coq_config.coqlib in + Filename.concat (Filename.concat coqlib "ide") f let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT @@ -210,10 +215,15 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) = let find_tag_limits (tag :GText.tag) (it:GText.iter) = (find_tag_start tag it , find_tag_stop tag it) -(* explanations ?? *) +(* explanations: Win32 threads won't work if events are produced + in a thread different from the thread of the Gtk loop. In this + case we must use GtkThread.async to push a callback in the + main thread. Beware that the synchronus version may produce + deadlocks. *) let async = - if Sys.os_type <> "Unix" then GtkThread.async else - (fun x -> x) + if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x) +let sync = + if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x) let stock_to_widget ?(size=`DIALOG) s = let img = GMisc.image () @@ -254,7 +264,7 @@ let browse f url = let url_for_keyword = let ht = Hashtbl.create 97 in begin try - let cin = open_in (Filename.concat lib_ide "index_urls.txt") in + let cin = open_in (lib_ide_file "index_urls.txt") in try while true do let s = input_line cin in try diff --git a/ide/ideutils.mli b/ide/ideutils.mli index d91faff4..cbdaefb9 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ideutils.mli,v 1.6.2.2 2005/01/21 17:21:33 herbelin Exp $ i*) +(*i $Id: ideutils.mli,v 1.6.2.4 2005/11/25 17:18:28 barras Exp $ i*) val async : ('a -> unit) -> 'a -> unit +val sync : ('a -> 'b) -> 'a -> 'b val browse : (string -> unit) -> string -> unit val browse_keyword : (string -> unit) -> string -> unit val byte_offset_to_char_offset : string -> int -> int @@ -24,7 +25,7 @@ val get_insert : < get_iter_at_mark : [> `INSERT] -> 'a; .. > -> 'a val is_char_start : char -> bool -val lib_ide : string +val lib_ide_file : string -> string val my_stat : string -> Unix.stats option val prerr_endline : string -> unit diff --git a/ide/undo.ml b/ide/undo.ml index 54449515..6f740667 100644 --- a/ide/undo.ml +++ b/ide/undo.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: undo.ml,v 1.8.2.1 2004/07/16 19:30:21 herbelin Exp $ *) +(* $Id: undo.ml,v 1.8.2.2 2005/11/16 17:22:39 barras Exp $ *) open GText open Ideutils @@ -18,7 +18,7 @@ let neg act = match act with | Insert (s,i,l) -> Delete (s,i,l) | Delete (s,i,l) -> Insert (s,i,l) -class undoable_view (tv:Gtk.text_view Gtk.obj) = +class undoable_view (tv:[>Gtk.text_view] Gtk.obj) = let undo_lock = ref true in object(self) inherit GText.view tv as super diff --git a/ide/undo.mli b/ide/undo.mli deleted file mode 100644 index 11613fdb..00000000 --- a/ide/undo.mli +++ /dev/null @@ -1,35 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* -object - inherit GText.view - method undo : bool - method redo : bool - method clear_undo : unit -end - -val undoable_view : - ?buffer:GText.buffer -> - ?editable:bool -> - ?cursor_visible:bool -> - ?justification:GtkEnums.justification -> - ?wrap_mode:GtkEnums.wrap_mode -> - ?border_width:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> - unit -> - undoable_view - - diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli new file mode 100644 index 00000000..d81d08d5 --- /dev/null +++ b/ide/undo_lablgtk_ge26.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Gtk.text_view] Gtk.obj -> +object + inherit GText.view + method undo : bool + method redo : bool + method clear_undo : unit +end + +val undoable_view : + ?buffer:GText.buffer -> + ?editable:bool -> + ?cursor_visible:bool -> + ?justification:GtkEnums.justification -> + ?wrap_mode:GtkEnums.wrap_mode -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> + undoable_view + + diff --git a/ide/undo_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli new file mode 100644 index 00000000..9c2176b0 --- /dev/null +++ b/ide/undo_lablgtk_lt26.mli @@ -0,0 +1,35 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* +object + inherit GText.view + method undo : bool + method redo : bool + method clear_undo : unit +end + +val undoable_view : + ?buffer:GText.buffer -> + ?editable:bool -> + ?cursor_visible:bool -> + ?justification:GtkEnums.justification -> + ?wrap_mode:GtkEnums.wrap_mode -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> + unit -> + undoable_view + + -- cgit v1.2.3