diff options
author | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-19 08:48:38 +0000 |
---|---|---|
committer | monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-19 08:48:38 +0000 |
commit | df0bf4b7226efb91b462221ca16463b7f5e93339 (patch) | |
tree | 28ed9422399c73c3f7e712bc45340a73ba8f666e | |
parent | cc9660a305171191a1446818a380a8f58c824f55 (diff) |
Coqide : les nouveaute d'aout
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4424 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | INSTALL.ide | 14 | ||||
-rw-r--r-- | ide/FAQ | 4 | ||||
-rw-r--r-- | ide/coq.ml | 5 | ||||
-rw-r--r-- | ide/coq.mli | 1 | ||||
-rw-r--r-- | ide/coqide.ml | 155 | ||||
-rw-r--r-- | ide/ideutils.ml | 3 | ||||
-rw-r--r-- | ide/ideutils.mli | 3 | ||||
-rw-r--r-- | ide/preferences.ml | 18 | ||||
-rw-r--r-- | ide/preferences.mli | 2 |
9 files changed, 147 insertions, 58 deletions
diff --git a/INSTALL.ide b/INSTALL.ide index 3619b3191..2d446f5ca 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -16,7 +16,7 @@ REQUIREMENT: You may still compile CoqIde with older 2.0.x versions and use all features. Run - "pkg-config --modversion gtk+-2.0 gthread-2.0" + "pkg-config --modversion gtk+-2.0" to check your version. All recent distributions have precompiled packages. Do not forget to install the developement headers packages. @@ -36,21 +36,21 @@ INSTALLATION 1) You need to install the OCaml stub library lablgtk2. See http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html - The latest CVS snapshot version is needed. + The latest CVS snapshot version is not enough. Use this one : - http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk2-20030707.tar.gz + http://www.lri.fr/~monate/download/lablgtk2-20030919.tar.gz If you are in a hurry just run : cd /tmp && \ - wget http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/dist/lablgtk2-20030707.tar.gz && \ - tar zxvf lablgtk2-20030707.tar.gz && \ - cd lablgtk2 && \ + wget http://www.lri.fr/~monate/download/lablgtk2-20030919.tar.gz && \ + tar zxvf lablgtk2-200919.tar.gz && \ + cd lablgtk2-20030919 && \ ./configure && \ make world && \ make install You must have write access to the OCaml standard library path. - If this fails read lablgtk2/README. + If this fails read lablgtk2-20030919/README. 2) Go into your Coq source directory and, as usual, configure with: @@ -1,7 +1,7 @@ CoqIde FAQ Q0) What is CoqIde? -R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more informations +R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more informations. Q1) How to enable Emacs keybindings? R1: Insert @@ -57,7 +57,7 @@ R6) Use Q7) How to customize the shortcuts for menus? R7) Two solutions are offered: - - Edit $HOME/.coqide.keys by hand + - Edit $HOME/.coqide.keys by hand or - Add "gtk-can-change-accels = 1" in your .coqiderc.gtk2 file. Then from CoqIde, you may select a menu entry and press the desired shortcut. Do not forget to save your preferences. diff --git a/ide/coq.ml b/ide/coq.ml index b166871c4..d6a6f3397 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -115,6 +115,11 @@ let interp s = last | None -> assert false +let interp_and_replace s = + let result = interp s in + let msg = read_stdout () in + result,msg + let nb_subgoals pf = List.length (fst (Refiner.frontier (Tacmach.proof_of_pftreestate pf))) diff --git a/ide/coq.mli b/ide/coq.mli index a420a1f4f..bc9ac6526 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -18,6 +18,7 @@ val version : unit -> string val init : unit -> string list val interp : string -> Util.loc * Vernacexpr.vernac_expr val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit +val interp_and_replace : string -> (Util.loc * Vernacexpr.vernac_expr) * string val is_tactic : Vernacexpr.vernac_expr -> bool val is_state_preserving : Vernacexpr.vernac_expr -> bool diff --git a/ide/coqide.ml b/ide/coqide.ml index 825311a62..d36b5a1a6 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -58,7 +58,8 @@ let set_tab_label i n = let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget in lbl#set_use_markup true; - lbl#set_text n (* lbl#set_label n *) + (* lbl#set_text n *) lbl#set_label n + let set_tab_image i s = let nb = notebook () in @@ -185,7 +186,7 @@ object('self) method recenter_insert : unit method reset_initial : unit method send_to_coq : - string -> + bool -> string -> bool -> bool -> bool -> (Util.loc * Vernacexpr.vernac_expr) option method set_message : string -> unit method show_goals : unit @@ -202,7 +203,7 @@ let (input_views:analyzed_views viewable_script Vector.t) = Vector.create () let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; Sys.sigill; Sys.sigpipe; Sys.sigquit; - (* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2] + (* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2] let crash_save i = (* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*) @@ -227,11 +228,11 @@ let crash_save i = Pervasives.prerr_endline "Done. Please report."; if i <> 127 then exit i -let ignore_break () = - List.iter - (fun i -> - try Sys.set_signal i (Sys.Signal_handle crash_save) - with _ -> prerr_endline "Signal ignored (normal if Win32)") +let ignore_break () = + List.iter + (fun i -> + try Sys.set_signal i (Sys.Signal_handle crash_save) + with _ -> prerr_endline "Signal ignored (normal if Win32)") signals_to_crash; Sys.set_signal Sys.sigint Sys.Signal_ignore @@ -331,22 +332,48 @@ let remove_current_view_page () = ((notebook ())#get_nth_page c)#misc#hide () -let starts_word it = it#starts_word && it#backward_char#char <> underscore -let ends_word it = it#ends_line || (it#ends_word && it#char <> underscore) -let inside_word it = it#inside_word || it#char = underscore || it#backward_char#char = underscore +let is_word_char c = + Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase + +let starts_word it = + prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'"); + (not it#copy#nocopy#backward_char || + (let c = it#backward_char#char in + not (is_word_char c))) + +let ends_word it = + (not it#copy#nocopy#forward_char || + let c = it#forward_char#char in + not (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase) + ) + +let inside_word it = + let c = it#char in + not (starts_word it) && + not (ends_word it) && + (Glib.Unichar.isalnum c || c = underscore || c = prime || c = arobase) + let is_on_word_limit it = inside_word it || ends_word it let rec find_word_start it = prerr_endline "Find word start"; - if starts_word it - then it - else find_word_start it#backward_char + if not it#nocopy#backward_char then + (prerr_endline "find_word_start: cannot backward"; it) + else if is_word_char it#char + then find_word_start it + else (it#nocopy#forward_char; + prerr_endline ("Word start at: "^(string_of_int it#offset));it) +let find_word_start (it:GText.iter) = find_word_start it#copy let rec find_word_end it = prerr_endline "Find word end"; - if ends_word it - then it - else find_word_end it#forward_char + if let c = it#char in c<>0 && is_word_char c + then begin + ignore (it#nocopy#forward_char); + find_word_end it + end else (prerr_endline ("Word end at: "^(string_of_int it#offset));it) +let find_word_end it = find_word_end it#copy + let get_word_around it = let start = find_word_start it in @@ -357,8 +384,9 @@ let get_word_around it = let rec complete_backward w (it:GText.iter) = prerr_endline "Complete backward..."; match it#backward_search w with - | None -> None + | None -> (prerr_endline "backward_search failed";None) | Some (start,stop) -> + prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset)); if starts_word start then let ne = find_word_end stop in if ne#compare stop = 0 @@ -395,7 +423,8 @@ let rec complete input_buffer w (offset:int) = | None -> last_completion := Some (lw,loffset, - (find_word_end (input_buffer#get_iter (`OFFSET loffset)))#offset , + (find_word_end + (input_buffer#get_iter (`OFFSET loffset)))#offset , false); None | Some (ss,start,stop) as result -> @@ -416,7 +445,8 @@ let rec complete input_buffer w (offset:int) = match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with | None -> last_completion := - Some (w,offset,(find_word_end (input_buffer#get_iter (`OFFSET offset)))#offset,false); + Some (w,offset,(find_word_end (input_buffer#get_iter + (`OFFSET offset)))#offset,false); complete input_buffer w offset | Some (ss,start,stop) as result -> last_completion := Some (w,offset,ss#offset,true); @@ -906,14 +936,23 @@ object(self) with e -> prerr_endline (Printexc.to_string e) end - method send_to_coq phrase show_output show_error localize = + method send_to_coq replace phrase show_output show_error localize = try full_goal_done <- false; prerr_endline "Send_to_coq starting now"; - let r = Some (Coq.interp phrase) in - let msg = read_stdout () in - self#insert_message (if show_output then msg else ""); - r + if replace then begin + let r,info = 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 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 (s,loc) = Coq.process_exn e in @@ -992,13 +1031,14 @@ object(self) let it () = input_buffer#get_iter (`OFFSET offset) in let iit = it () in let start = find_word_start iit in - if is_on_word_limit iit then + if ends_word iit then let w = input_buffer#get_text ~start ~stop:iit () in - prerr_endline ("Completion of prefix : " ^ w); + if String.length w <> 0 then begin + prerr_endline ("Completion of prefix : '" ^ w^"'"); match complete input_buffer w start#offset with | None -> false | Some (ss,start,stop) -> @@ -1007,7 +1047,9 @@ object(self) ignore (input_buffer#insert_interactive completion); input_buffer#move_mark `SEL_BOUND (it())#backward_char; true + end else false else false + method process_next_phrase display_goals do_highlight = begin @@ -1020,7 +1062,7 @@ object(self) end; begin match (self#find_phrase_starting_at self#get_start_of_input) with - | None -> + | None -> if do_highlight then begin input_view#set_editable true; !pop_info (); @@ -1031,12 +1073,11 @@ object(self) if do_highlight then begin input_buffer#apply_tag_by_name ~start ~stop "to_process"; prerr_endline "process_next_phrase : to_process applied"; - process_pending () end; prerr_endline "process_next_phrase : getting phrase"; let phrase = start#get_slice ~stop in let r = - match self#send_to_coq phrase true true true with + match self#send_to_coq false phrase true true true with | Some ast -> begin b#move_mark ~where:stop (`NAME "start_of_input"); @@ -1046,8 +1087,7 @@ object(self) b#place_cursor stop; self#recenter_insert end; - let start_of_phrase_mark = `MARK (b#create_mark start) - in + 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 @@ -1069,7 +1109,7 @@ object(self) method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = - match self#send_to_coq coqphrase show_output show_msg localize with + match self#send_to_coq false coqphrase show_output show_msg localize with | Some ast -> begin let stop = self#get_start_of_input in @@ -1697,6 +1737,7 @@ let main files = (* File/Load Menu *) let load f = try + prerr_endline "Loading file starts"; Vector.find_or_fail (function | {analyzed_view=Some av} -> @@ -1705,32 +1746,46 @@ let main files = | Some fn -> f=fn) | _ -> false) !input_views; + prerr_endline "Loading: must open"; let b = Buffer.create 1024 in + prerr_endline "Loading: get raw content"; with_file f ~f:(input_channel b); + prerr_endline "Loading: convert content"; let s = do_convert (Buffer.contents b) in + prerr_endline "Loading: create view"; let view = create_input_tab (Glib.Convert.filename_to_utf8 (Filename.basename f)) in + prerr_endline "Loading: change font"; view#misc#modify_font !current.text_font; + prerr_endline "Loading: adding view"; let index = add_input_view {view = view; analyzed_view = None; } in let av = (new analyzed_view index) in + prerr_endline "Loading: register view"; (get_input_view index).analyzed_view <- Some av; + prerr_endline "Loading: set filename"; av#set_filename (Some (if Filename.is_relative f then Filename.concat initial_cwd f else f )); + prerr_endline "Loading: stats"; av#update_stats; let input_buffer = view#buffer in + prerr_endline "Loading: fill buffer"; input_buffer#set_text s; input_buffer#place_cursor input_buffer#start_iter; + prerr_endline ("Loading: switch to view "^ string_of_int index); set_current_view index; + prerr_endline "Loading: highlight"; Highlight.highlight_all input_buffer; input_buffer#set_modified false; - av#view#clear_undo + prerr_endline "Loading: clear undo"; + av#view#clear_undo; + prerr_endline "Loading: success" with | Vector.Found i -> set_current_view i | e -> !flash_info ("Load failed: "^(Printexc.to_string e)) @@ -1988,16 +2043,16 @@ let main files = with _ -> prerr_endline "EMIT PASTE FAILED"))); ignore (edit_f#add_separator ()); - let toggle_auto_complete_i = + + let toggle_auto_complete_i = edit_f#add_check_item "_Auto Completion" - ~active:false - ~key:GdkKeysyms._B + ~active:!current.auto_complete ~callback:(fun b -> match (get_current_view()).analyzed_view with - | Some av -> av#set_auto_complete b - | None -> ()) - in - - let read_only_i = edit_f#add_check_item "Expert" ~active:false + | Some av -> av#set_auto_complete b + | None -> ()) + in + auto_complete := toggle_auto_complete_i#set_active ; + let read_only_i = edit_f#add_check_item "Expert" ~active:false ~key:GdkKeysyms._B ~callback:(fun b -> () ) @@ -2786,7 +2841,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ~pixbuf:startup_image; b#insert ~iter:b#start_iter "\t\t"; with _ -> ()); - b#insert "\nCoqIde: an experimental Gtk2 interface for Coq.\n\nVersion infomation\n--------\n"; + b#insert "\nCoqIde: an experimental Gtk2 interface for Coq.\n\nVersion information\n--------\n"; b#insert ((Coq.version ())); b#insert "\nAuthor: Benjamin Monate\nDo not hesitate to report bugs or missing features." in about tv2#buffer; @@ -2843,9 +2898,12 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); !current.window_width <- w; end )); - ignore(nb#connect#change_current_page + ignore(nb#connect#switch_page ~callback: - (fun i -> List.iter (function f -> f i) !to_do_on_page_switch) + (fun i -> + prerr_endline ("switch_page: starts " ^ string_of_int i); + List.iter (function f -> f i) !to_do_on_page_switch; + prerr_endline "switch_page: success") ); ignore(tv2#event#connect#enter_notify (fun _ -> @@ -2860,7 +2918,12 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); end; false; )); - List.iter load files; + List.iter (fun f -> + if Sys.file_exists f then load f else + if (let l = String.length f in + l >= 3 && String.sub f (l-3) 2 = ".v") + then load f + else load (f^".v")) files; if List.length files >=1 then activate_input 1 ;; diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 99c06cf67..c42c01fe2 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -275,6 +275,9 @@ let run_command f c = (Unix.close_process_full (cin,cout,cerr), Buffer.contents result) let underscore = Glib.Utf8.to_unichar "_" (ref 0) + +let arobase = Glib.Utf8.to_unichar "@" (ref 0) +let prime = Glib.Utf8.to_unichar "'" (ref 0) let bn = Glib.Utf8.to_unichar "\n" (ref 0) let space = Glib.Utf8.to_unichar " " (ref 0) let tab = Glib.Utf8.to_unichar "\t" (ref 0) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 6c2124a37..bf1915978 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -48,7 +48,10 @@ val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit val run_command : (string -> unit) -> string -> Unix.process_status*string + +val prime : Glib.unichar val underscore : Glib.unichar +val arobase : Glib.unichar val bn : Glib.unichar val space : Glib.unichar val tab : Glib.unichar diff --git a/ide/preferences.ml b/ide/preferences.ml index 5d127f5a0..454333141 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -92,6 +92,7 @@ type pref = mutable window_height :int; mutable use_utf8_notation : bool; + mutable auto_complete : bool; } let (current:pref ref) = @@ -139,6 +140,7 @@ let (current:pref ref) = window_width = 800; window_height = 600; use_utf8_notation = true; + auto_complete = true } @@ -146,6 +148,8 @@ let change_font = ref (fun f -> ()) let show_toolbar = ref (fun x -> ()) +let auto_complete = ref (fun x -> ()) + let contextual_menus_on_goal = ref (fun x -> ()) let resize_window = ref (fun () -> ()) @@ -195,6 +199,7 @@ let save_pref () = [string_of_bool p.contextual_menus_on_goal] ++ add "window_height" [string_of_int p.window_height] ++ add "window_width" [string_of_int p.window_width] ++ + add "auto_complete" [string_of_bool p.auto_complete] ++ Config_lexer.print_file pref_file with _ -> prerr_endline "Could not save preferences." @@ -249,7 +254,7 @@ let load_pref () = (fun v -> np.contextual_menus_on_goal <- v); set_int "window_width" (fun v -> np.window_width <- v); set_int "window_height" (fun v -> np.window_height <- v); - + set_bool "auto_complete" (fun v -> np.auto_complete <- v); current := np with e -> prerr_endline ("Could not load preferences ("^ @@ -309,6 +314,13 @@ let configure () = "Window width" (string_of_int !current.window_width) in + let auto_complete = + bool + ~f:(fun s -> + !current.auto_complete <- s; + !auto_complete s) + "Auto Complete" !current.auto_complete + in (* let use_utf8_notation = bool @@ -445,7 +457,7 @@ let configure () = "Contextual menus on goal" !current.contextual_menus_on_goal in - let misc = [contextual_menus_on_goal] in + let misc = [contextual_menus_on_goal;auto_complete] in let cmds = [Section("Fonts", @@ -457,7 +469,7 @@ let configure () = Section("Files", [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) - encodings + encodings; ]); Section("Browser", [cmd_browse;doc_url;library_url]); diff --git a/ide/preferences.mli b/ide/preferences.mli index d46ad050c..ba5d693e9 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -46,6 +46,7 @@ type pref = mutable window_width : int; mutable window_height : int; mutable use_utf8_notation : bool; + mutable auto_complete : bool; } val save_pref : unit -> unit @@ -57,4 +58,5 @@ val configure : unit -> unit val change_font : ( Pango.font_description -> unit) ref val show_toolbar : (bool -> unit) ref +val auto_complete : (bool -> unit) ref val resize_window : (unit -> unit) ref |