From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- ide/coqide.ml | 4012 ++++++++++++++++++++++++++------------------------------- 1 file changed, 1803 insertions(+), 2209 deletions(-) (limited to 'ide/coqide.ml') diff --git a/ide/coqide.ml b/ide/coqide.ml index cc147d5e..201fbe47 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -7,123 +7,23 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 12104 2009-04-24 18:10:10Z notin $ *) +(* $Id$ *) open Preferences open Vernacexpr open Coq +open Gtk_parsing open Ideutils - -let cb_ = ref None -let cb () = ((Option.get !cb_):GData.clipboard) -let last_cb_content = ref "" -let (message_view:GText.view option ref) = ref None -let (proof_view:GText.view option ref) = ref None - -let (_notebook:GPack.notebook option ref) = ref None -let notebook () = Option.get !_notebook +type ide_info = { + start : GText.mark; + stop : GText.mark; +} -let update_notebook_pos () = - let pos = - match !current.vertical_tabs, !current.opposite_tabs with - | false, false -> `TOP - | false, true -> `BOTTOM - | true , false -> `LEFT - | true , true -> `RIGHT - in - (notebook ())#set_tab_pos pos - -(* Tabs contain the name of the edited file and 2 status informations: - Saved state + Focused proof buffer *) -let decompose_tab w = - let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in - let l = vbox#children in - match l with - | [img;lbl] -> - let img = new GMisc.image - ((Gobject.try_cast img#as_widget "GtkImage"): - Gtk.image Gtk.obj) - in - let lbl = GMisc.label_cast lbl in - vbox,img,lbl - | _ -> assert false - -let set_tab_label i n = - let nb = notebook () in - 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 - - -let set_tab_image ~icon i = - let nb = notebook () in - let _,img,_ = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget - in - img#set_icon_size `SMALL_TOOLBAR; - img#set_stock icon - -let set_current_tab_image ~icon = set_tab_image ~icon (notebook())#current_page - -let set_current_tab_label n = set_tab_label (notebook())#current_page n - -let get_tab_label i = - let nb = notebook () in - let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget - in - lbl#text - -let get_full_tab_label i = - let nb = notebook () in - let _,_,lbl = decompose_tab (nb#get_tab_label(nb#get_nth_page i))#as_widget - in - lbl - -let get_current_tab_label () = get_tab_label (notebook())#current_page - -let get_current_page () = - let i = (notebook())#current_page in - (notebook())#get_nth_page i - -(* This function must remove "focused proof" decoration *) -let reset_tab_label i = - set_tab_label i (get_tab_label i) - -let to_do_on_page_switch = ref [] - -module Vector = struct - exception Found of int - type 'a t = ('a option) array ref - let create () = ref [||] - let length t = Array.length !t - let get t i = Option.get (Array.get !t i) - let set t i v = Array.set !t i (Some v) - let remove t i = Array.set !t i None - let append t e = t := Array.append !t [|Some e|]; (Array.length !t)-1 - let iter f t = Array.iter (function | None -> () | Some x -> f x) !t - let find_or_fail f t = - let test i = function | None -> () | Some e -> if f e then raise (Found i) in - Array.iteri test t - - let exists f t = - let l = Array.length !t in - let rec test i = - (i < l) && (((!t.(i) <> None) && f (Option.get !t.(i))) || test (i+1)) - in - test 0 -end -type 'a viewable_script = - {view : Undo.undoable_view; - mutable analyzed_view : 'a option; - } - - -class type analyzed_views= +class type analyzed_views= object('self) val mutable act_id : GtkSignal.id option - val current_all : 'self viewable_script val mutable deact_id : GtkSignal.id option val input_buffer : GText.buffer val input_view : Undo.undoable_view @@ -133,6 +33,7 @@ object('self) val message_view : GText.view val proof_buffer : GText.buffer val proof_view : GText.view + val cmd_stack : (ide_info * Coq.reset_info) Stack.t val mutable is_active : bool val mutable read_only : bool val mutable filename : string option @@ -145,7 +46,6 @@ object('self) method add_detached_view : GWindow.window -> unit method remove_detached_view : GWindow.window -> unit - method view : Undo.undoable_view method filename : string option method stats : Unix.stats option method set_filename : string option -> unit @@ -184,7 +84,7 @@ object('self) method send_to_coq : bool -> bool -> string -> bool -> bool -> bool -> - (bool*(reset_info*(Util.loc * Vernacexpr.vernac_expr))) option + (bool*reset_info) option method set_message : string -> unit method show_pm_goal : unit method show_goals : unit @@ -192,37 +92,132 @@ object('self) method undo_last_step : unit method help_for_keyword : unit -> unit method complete_at_offset : int -> bool - - method blaster : unit -> unit end -let (input_views:analyzed_views viewable_script Vector.t) = Vector.create () + +type viewable_script = + {script : Undo.undoable_view; + tab_label : GMisc.label; + mutable filename : string; + mutable encoding : string; + proof_view : GText.view; + message_view : GText.view; + analyzed_view : analyzed_views; + command_stack : (ide_info * Coq.reset_info) Stack.t; + } + + +let notebook_page_of_session {script=script;tab_label=bname;proof_view=proof;message_view=message} = + let session_paned = + GPack.paned `HORIZONTAL ~border_width:5 () in + let script_frame = + GBin.frame ~shadow_type:`IN ~packing:session_paned#add1 () in + let script_scroll = + GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:script_frame#add () in + let state_paned = + GPack.paned `VERTICAL ~packing:session_paned#add2 () in + let proof_frame = + GBin.frame ~shadow_type:`IN ~packing:state_paned#add1 () in + let proof_scroll = + GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:proof_frame#add () in + let message_frame = + GBin.frame ~shadow_type:`IN ~packing:state_paned#add2 () in + let message_scroll = + GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC ~packing:message_frame#add () in + let session_tab = + GPack.hbox ~homogeneous:false () in + let img = + GMisc.image ~packing:session_tab#pack ~icon_size:`SMALL_TOOLBAR () in + let _ = + script#buffer#connect#modified_changed + ~callback:(fun () -> if script#buffer#modified + then img#set_stock `SAVE + else img#set_stock `YES) in + let _ = + session_paned#misc#connect#size_allocate + (let old_paned_width = ref 2 in + let old_paned_height = ref 2 in + (fun {Gtk.width=paned_width;Gtk.height=paned_height} -> + if !old_paned_width <> paned_width || !old_paned_height <> paned_height then ( + session_paned#set_position (session_paned#position * paned_width / !old_paned_width); + state_paned#set_position (state_paned#position * paned_height / !old_paned_height); + old_paned_width := paned_width; + old_paned_height := paned_height; + ))) in + script_scroll#add script#coerce; + proof_scroll#add proof#coerce; + message_scroll#add message#coerce; + session_tab#pack bname#coerce; + img#set_stock `YES; + session_paned#set_position 1; + state_paned#set_position 1; + (Some session_tab#coerce,None,session_paned#coerce) + +let session_notebook = + Typed_notebook.create notebook_page_of_session ~border_width:2 ~show_border:false ~scrollable:true () + +let active_view = ref (~-1) + +let on_active_view f = + if !active_view < 0 + then failwith "no active view !" + else f (session_notebook#get_nth_term !active_view) + +let cb = GData.clipboard Gdk.Atom.primary + + +let last_cb_content = ref "" -let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; - Sys.sigill; Sys.sigpipe; Sys.sigquit; +let update_notebook_pos () = + let pos = + match !current.vertical_tabs, !current.opposite_tabs with + | false, false -> `TOP + | false, true -> `BOTTOM + | true , false -> `LEFT + | true , true -> `RIGHT + in + session_notebook#set_tab_pos pos + + +let set_active_view i = + prerr_endline "entering set_active_view"; + (try on_active_view (fun {tab_label=lbl} -> lbl#set_text lbl#text) with _ -> ()); + session_notebook#goto_page i; + let s = session_notebook#current_term in + s.tab_label#set_use_markup true; + s.tab_label#set_label (""^s.tab_label#text^""); + active_view := i; + prerr_endline "exiting set_active_view" + + + +let to_do_on_page_switch = ref [] + + +let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup; + Sys.sigill; Sys.sigpipe; Sys.sigquit; (* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2] let crash_save i = (* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*) Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files"; - let count = ref 0 in - Vector.iter - (function {view=view; analyzed_view = Some av } -> - (let filename = match av#filename with - | None -> - incr count; + let count = ref 0 in + List.iter + (function {script=view; analyzed_view = av } -> + (let filename = match av#filename with + | None -> + incr count; "Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide" | Some f -> f^".crashcoqide" in - try + try if try_export filename (view#buffer#get_text ()) then Pervasives.prerr_endline ("Saved "^filename) else Pervasives.prerr_endline ("Could not save "^filename) with _ -> Pervasives.prerr_endline ("Could not save "^filename)) - | _ -> Pervasives.prerr_endline "Unanalyzed view found. Please report." ) - input_views; + session_notebook#pages; Pervasives.prerr_endline "Done. Please report."; if i <> 127 then exit i @@ -240,9 +235,9 @@ let coq_computing = Mutex.create () (* To prevent Coq from interrupting during undoing...*) let coq_may_stop = Mutex.create () -let break () = +let break () = prerr_endline "User break received:"; - if not (Mutex.try_lock coq_computing) then + if not (Mutex.try_lock coq_computing) then begin prerr_endline " trying to stop computation:"; if Mutex.try_lock coq_may_stop then begin @@ -256,225 +251,110 @@ let break () = prerr_endline " ignored (not computing)" end -let do_if_not_computing text f x = - let threaded_task () = - if Mutex.try_lock coq_computing - then - begin - 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 - prerr_endline ("Launching thread " ^ text); - ignore (Thread.create threaded_task ()) - -let add_input_view tv = - Vector.append input_views tv - -let get_input_view i = - if 0 <= i && i < Vector.length input_views - then - Vector.get input_views i - else raise Not_found - -let active_view = ref None - -let get_active_view () = Vector.get input_views (Option.get !active_view) - -let set_active_view i = - (match !active_view with None -> () | Some i -> - reset_tab_label i); - (notebook ())#goto_page i; - let txt = get_current_tab_label () in - set_current_tab_label (""^txt^""); - active_view := Some i - -let set_current_view i = (notebook ())#goto_page i - -let kill_input_view i = - let v = Vector.get input_views i in - (match v.analyzed_view with - | Some v -> v#kill_detached_views () - | None -> ()); - v.view#destroy (); - v.analyzed_view <- None; - Vector.remove input_views i - -let get_current_view_page () = (notebook ())#current_page -let get_current_view () = Vector.get input_views (notebook ())#current_page -let remove_current_view_page () = - let c = (notebook ())#current_page in - kill_input_view c; - ((notebook ())#get_nth_page c)#misc#hide () - -let is_word_char c = - (* TODO: avoid num and prime at the head of a word *) - Glib.Unichar.isalnum c || c = underscore || c = prime - -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 (is_word_char c) - ) - -let inside_word it = - let c = it#char in - not (starts_word it) && - not (ends_word it) && - is_word_char c - -let is_on_word_limit it = inside_word it || ends_word it - -let rec find_word_start it = - prerr_endline "Find word start"; - 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 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 - let stop = find_word_end it in - start,stop - - -let rec complete_backward w (it:GText.iter) = - prerr_endline "Complete backward..."; - match it#backward_search w with - | 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 - then complete_backward w start - else Some (start,stop,ne) - else complete_backward w start - -let rec complete_forward w (it:GText.iter) = - prerr_endline "Complete forward..."; - match it#forward_search w with - | None -> None - | Some (start,stop) -> - if starts_word start then - let ne = find_word_end stop in - if ne#compare stop = 0 then - complete_forward w stop - else Some (stop,stop,ne) - else complete_forward w stop +let do_if_not_computing text f x = + if Mutex.try_lock coq_computing then + let threaded_task () = + prerr_endline "Getting lock"; + try + f x; + prerr_endline "Releasing lock"; + Mutex.unlock coq_computing; + with e -> + prerr_endline "Releasing lock (on error)"; + Mutex.unlock coq_computing; + raise e + in + prerr_endline ("Launching thread " ^ text); + ignore (Glib.Timeout.add ~ms:300 ~callback: + (fun () -> if Mutex.try_lock coq_computing + then (Mutex.unlock coq_computing; false) + else (pbar#pulse (); true))); + ignore (Thread.create threaded_task ()) + else + prerr_endline + "Discarded order (computations are ongoing)" + +(* XXX - 1 appel *) +let kill_input_view i = + let v = session_notebook#get_nth_term i in + v.analyzed_view#kill_detached_views (); + v.script#destroy (); + v.tab_label#destroy (); + v.proof_view#destroy (); + v.message_view#destroy (); + session_notebook#remove_page i +(* +(* XXX - beaucoups d'appels, a garder *) +let get_current_view = + focused_session + *) +let remove_current_view_page () = + let c = session_notebook#current_page in + kill_input_view c + (* Reset this to None on page change ! *) let (last_completion:(string*int*int*bool) option ref) = ref None -let () = to_do_on_page_switch := +let () = to_do_on_page_switch := (fun i -> last_completion := None)::!to_do_on_page_switch let rec complete input_buffer w (offset:int) = - match !last_completion with + match !last_completion with | Some (lw,loffset,lpos,backward) when lw=w && loffset=offset -> begin let iter = input_buffer#get_iter (`OFFSET lpos) in - if backward then + if backward then match complete_backward w iter with - | None -> - last_completion := + | None -> + last_completion := Some (lw,loffset, - (find_word_end + (find_word_end (input_buffer#get_iter (`OFFSET loffset)))#offset , - false); + false); None - | Some (ss,start,stop) as result -> - last_completion := + | Some (ss,start,stop) as result -> + last_completion := Some (w,offset,ss#offset,true); result else match complete_forward w iter with - | None -> + | None -> last_completion := None; None - | Some (ss,start,stop) as result -> - last_completion := + | Some (ss,start,stop) as result -> + last_completion := Some (w,offset,ss#offset,false); result end | _ -> begin match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with - | None -> - last_completion := + | None -> + last_completion := 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 -> + | Some (ss,start,stop) as result -> last_completion := Some (w,offset,ss#offset,true); result end - + let get_current_word () = - let av = Option.get ((get_current_view ()).analyzed_view) in - match (cb ())#text with - | None -> + match session_notebook#current_term,cb#text with + | {script=script; analyzed_view=av;},None -> prerr_endline "None selected"; let it = av#get_insert in let start = find_word_start it in let stop = find_word_end start in - av#view#buffer#move_mark `SEL_BOUND start; - av#view#buffer#move_mark `INSERT stop; - av#view#buffer#get_text ~slice:true ~start ~stop () - | Some t -> + script#buffer#move_mark `SEL_BOUND start; + script#buffer#move_mark `INSERT stop; + script#buffer#get_text ~slice:true ~start ~stop () + | _,Some t -> prerr_endline "Some selected"; prerr_endline t; t - + let input_channel b ic = let buf = String.create 1024 and len = ref 0 in @@ -488,142 +368,6 @@ let with_file handler name ~f = try f ic; close_in ic with e -> close_in ic; raise e with Sys_error s -> handler s -type info = {start:GText.mark; - stop:GText.mark; - ast:Util.loc * Vernacexpr.vernac_expr; - reset_info:Coq.reset_info - } - -exception Size of int -let (processed_stack:info Stack.t) = Stack.create () -let push x = Stack.push x processed_stack -let pop () = try Stack.pop processed_stack with Stack.Empty -> raise (Size 0) -let top () = try Stack.top processed_stack with Stack.Empty -> raise (Size 0) -let is_empty () = Stack.is_empty processed_stack - -(* push a new Coq phrase *) - -let update_on_end_of_segment id = - let lookup_section = function - | { reset_info = ResetAtSegmentStart id',_,_ } when id = id' -> raise Exit - | { reset_info = _,_,r } -> r := false - in - try Stack.iter lookup_section processed_stack with Exit -> () - -let push_phrase reset_info start_of_phrase_mark end_of_phrase_mark ast = - let x = {start = start_of_phrase_mark; - stop = end_of_phrase_mark; - ast = ast; - reset_info = reset_info - } in - begin - match snd ast with - | VernacEndSegment (_,id) -> - prerr_endline "Updating on end of segment 1"; - update_on_end_of_segment id - | _ -> () - end; - push x - - -let repush_phrase reset_info x = - let x = { x with reset_info = reset_info } in - begin - match snd x.ast with - | VernacEndSegment (_,id) -> - prerr_endline "Updating on end of segment 2"; - update_on_end_of_segment id - | _ -> () - end; - push x - -type backtrack = -| BacktrackToNextActiveMark -| BacktrackToMark of reset_mark -| BacktrackToModSec of Names.identifier -| NoBacktrack - -let add_undo = function (n,a,b,p,l as x) -> if p = 0 then (n+1,a,b,p,l) else x -let add_abort = function - | (n,a,b,0,l) -> (0,a+1,b,0,l) - | (n,a,b,p,l) -> (n,a,b,p-1,l) -let add_qed q (n,a,b,p,l as x) = - if q = 0 then x else (n,a,BacktrackToNextActiveMark,p+q,l) -let add_backtrack (n,a,b,p,l) b' = (n,a,b',p,l) - -let update_proofs (n,a,b,p,cur_lems) prev_lems = - let ncommon = List.length (Util.list_intersect cur_lems prev_lems) in - let openproofs = List.length cur_lems - ncommon in - let closedproofs = List.length prev_lems - ncommon in - let undos = (n,a,b,p,prev_lems) in - add_qed closedproofs (Util.iterate add_abort openproofs undos) - -let pop_command undos t = - let (state_info,undo_info,section_info) = t.reset_info in - let undos = - if !section_info then - let undos = update_proofs undos undo_info in - match state_info with - | _ when is_vernac_tactic_command (snd t.ast) -> - (* A tactic, active if not below a Qed *) - add_undo undos - | ResetAtRegisteredObject mark -> - add_backtrack undos (BacktrackToMark mark) - | ResetAtSegmentStart id -> - add_backtrack undos (BacktrackToModSec id) - | _ when is_vernac_state_preserving_command (snd t.ast) -> - undos - | _ -> - add_backtrack undos BacktrackToNextActiveMark - else - begin - prerr_endline "In section"; - (* An object inside a closed section *) - add_backtrack undos BacktrackToNextActiveMark - end in - ignore (pop ()); - undos - -let apply_aborts a = - if a <> 0 then prerr_endline ("Applying "^string_of_int a^" aborts"); - try Util.repeat a Pfedit.delete_current_proof () - with e -> prerr_endline "WARNING : found a closed environment"; raise e - -exception UndoStackExhausted - -let apply_tactic_undo n = - if n<>0 then - (prerr_endline ("Applying "^string_of_int n^" undos"); - try Pfedit.undo n with _ -> raise UndoStackExhausted) - -let apply_reset = function - | BacktrackToMark mark -> reset_to mark - | BacktrackToModSec id -> reset_to_mod id - | NoBacktrack -> () - | BacktrackToNextActiveMark -> assert false - -let rec apply_undos (n,a,b,p,l as undos) = - if p = 0 & b <> BacktrackToNextActiveMark then - begin - apply_aborts a; - try - apply_tactic_undo n; - apply_reset b - with UndoStackExhausted -> - apply_undos (n,0,BacktrackToNextActiveMark,p,l) - end - else - (* re-synchronize Coq to the current state of the stack *) - if is_empty () then - Coq.reset_initial () - else - begin - let t = top () in - apply_undos (pop_command undos t); - let reset_info = Coq.compute_reset_info (snd t.ast) in - interp_last t.ast; - repush_phrase reset_info t - end (* For electric handlers *) exception Found @@ -631,19 +375,16 @@ exception Found (* For find_phrase_starting_at *) exception Stop of int -let activate_input i = - (match !active_view with - | None -> () - | Some n -> - let a_v = Option.get (Vector.get input_views n).analyzed_view in - a_v#deactivate (); - a_v#reset_initial - ); - let activate_function = (Option.get (Vector.get input_views i).analyzed_view)#activate in - activate_function (); - set_active_view i - -let warning msg = +(* XXX *) +let activate_input i = + prerr_endline "entering activate_input"; + (try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ()) + with _ -> ()); + (session_notebook#get_nth_term i).analyzed_view#activate (); + set_active_view i; + prerr_endline "exiting activate_input" + +let warning msg = GToolbox.message_box ~title:"Warning" ~icon:(let img = GMisc.image () in img#set_stock `DIALOG_WARNING; @@ -651,30 +392,142 @@ let warning msg = img#coerce) msg - -class analyzed_view index = - let {view = input_view_} as current_all_ = get_input_view index in - let proof_view_ = Option.get !proof_view in - let message_view_ = Option.get !message_view in +let apply_tag (buffer:GText.buffer) orig off_conv from upto sort = + let conv_and_apply start stop tag = + let start = orig#forward_chars (off_conv from) in + let stop = orig#forward_chars (off_conv upto) in + buffer#apply_tag ~start ~stop tag + in match sort with + | Coq_lex.Comment -> + conv_and_apply from upto Tags.Script.comment + | Coq_lex.Keyword -> + conv_and_apply from upto Tags.Script.kwd + | Coq_lex.Declaration -> + conv_and_apply from upto Tags.Script.decl + | Coq_lex.ProofDeclaration -> + conv_and_apply from upto Tags.Script.proof_decl + | Coq_lex.Qed -> + conv_and_apply from upto Tags.Script.qed + | Coq_lex.String -> () + +let remove_tags (buffer:GText.buffer) from upto = + List.iter (buffer#remove_tag ~start:from ~stop:upto) + [ Tags.Script.comment; Tags.Script.kwd; Tags.Script.decl; + Tags.Script.proof_decl; Tags.Script.qed ] + +let split_slice_lax (buffer:GText.buffer) from upto = + remove_tags buffer from upto; + buffer#remove_tag ~start:from ~stop:upto Tags.Script.lax_end; + let slice = buffer#get_text ~start:from ~stop:upto () in + let slice = slice ^ " " in + let rec split_substring str = + let off_conv = byte_offset_to_char_offset str in + let slice_len = String.length str in + let sentence_len = Coq_lex.find_end_offset (apply_tag buffer from off_conv) str in + + let stop = from#forward_chars (pred (off_conv sentence_len)) in + let start = stop#backward_char in + buffer#apply_tag ~start ~stop Tags.Script.lax_end; + + if 1 < slice_len - sentence_len then begin (* remember that we added a trailing space *) + ignore (from#nocopy#forward_chars (off_conv sentence_len)); + split_substring (String.sub str sentence_len (slice_len - sentence_len)) + end + in + split_substring slice + +let rec grab_safe_sentence_start (iter:GText.iter) soi = + let lax_back = iter#backward_char#has_tag Tags.Script.lax_end in + let on_space = List.mem iter#char [0x09;0x0A;0x20] in + let full_ending = iter#is_start || (lax_back & on_space) in + if full_ending then iter + else if iter#compare soi <= 0 then raise Not_found + else + let prev = iter#backward_to_tag_toggle (Some Tags.Script.lax_end) in + (if prev#has_tag Tags.Script.lax_end then + ignore (prev#nocopy#backward_to_tag_toggle (Some Tags.Script.lax_end))); + grab_safe_sentence_start prev soi + +let grab_sentence_end_from (start:GText.iter) = + let stop = start#forward_to_tag_toggle (Some Tags.Script.lax_end) in + stop#forward_char + +let get_sentence_bounds (iter:GText.iter) = + let start = iter#backward_to_tag_toggle (Some Tags.Script.lax_end) in + (if start#has_tag Tags.Script.lax_end then ignore ( + start#nocopy#backward_to_tag_toggle (Some Tags.Script.lax_end))); + let stop = start#forward_to_tag_toggle (Some Tags.Script.lax_end) in + let stop = stop#forward_char in + start,stop + +let end_tag_present end_iter = + end_iter#backward_char#has_tag Tags.Script.lax_end + +let tag_on_insert = + let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *) + fun buffer -> + try + let insert = buffer#get_iter_at_mark `INSERT in + let start = grab_safe_sentence_start insert + (buffer#get_iter_at_mark (`NAME "start_of_input")) in + let stop = grab_sentence_end_from insert in + let skip_curr = ref true in (* shall the callback be skipped ? by default yes*) + (!skip_last) := true; (* skip the previously created callback *) + skip_last := skip_curr; + try split_slice_lax buffer start stop + with Not_found -> + skip_curr := false; + ignore (Glib.Timeout.add ~ms:1500 + ~callback:(fun () -> if not !skip_curr then ( + try split_slice_lax buffer start buffer#end_iter with _ -> ()); false)) + with Not_found -> + let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in + buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char + +let force_retag buffer = + try split_slice_lax buffer buffer#start_iter buffer#end_iter with _ -> () + +let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = + (* move back twice if not into proof_decl, + * once if into proof_decl and back_char into_proof_decl, + * don't move if into proof_decl and back_char not into proof_decl *) + if not (cursor#has_tag Tags.Script.proof_decl) then + ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl)); + if cursor#backward_char#has_tag Tags.Script.proof_decl then + ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl)); + let decl_start = cursor in + let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in + let decl_end = grab_sentence_end_from decl_start in + let prf_end = grab_sentence_end_from prf_end in + let prf_end = prf_end#forward_char in + if decl_start#has_tag Tags.Script.folded then ( + buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; + buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) + else ( + buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded; + buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden) + +class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs = object(self) - val current_all = current_all_ - val input_view = current_all_.view - val proof_view = Option.get !proof_view - val message_view = Option.get !message_view - val input_buffer = input_view_#buffer - val proof_buffer = proof_view_#buffer - val message_buffer = message_view_#buffer + val input_view = _script + val input_buffer = _script#buffer + val proof_view = _pv + val proof_buffer = _pv#buffer + val message_view = _mv + val message_buffer = _mv#buffer + val cmd_stack = _cs val mutable is_active = false val mutable read_only = false - val mutable filename = None + val mutable filename = None val mutable stats = None val mutable last_modification_time = 0. val mutable last_auto_save_time = 0. val mutable detached_views = [] val mutable auto_complete_on = !current.auto_complete + val hidden_proofs = Hashtbl.create 32 - method private toggle_auto_complete = + method private toggle_auto_complete = auto_complete_on <- not auto_complete_on method set_auto_complete t = auto_complete_on <- t method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b = fun f x -> @@ -683,131 +536,130 @@ object(self) let y = f x in self#set_auto_complete old; y - method add_detached_view (w:GWindow.window) = + method add_detached_view (w:GWindow.window) = detached_views <- w::detached_views - method remove_detached_view (w:GWindow.window) = + method remove_detached_view (w:GWindow.window) = detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views - method kill_detached_views () = + method kill_detached_views () = List.iter (fun w -> w#destroy ()) detached_views; detached_views <- [] - method view = input_view method filename = filename method stats = stats - method set_filename f = + method set_filename f = filename <- f; - match f with + match f with | Some f -> stats <- my_stat f | None -> () - method update_stats = - match filename with - | Some f -> stats <- my_stat f + method update_stats = + match filename with + | Some f -> stats <- my_stat f | _ -> () - method revert = - match filename with + method revert = + match filename with | Some f -> begin - let do_revert () = begin - !push_info "Reverting buffer"; - try - if is_active then self#reset_initial; - let b = Buffer.create 1024 in - with_file !flash_info f ~f:(input_channel b); - let s = try_convert (Buffer.contents b) in - input_buffer#set_text s; - self#update_stats; - input_buffer#place_cursor input_buffer#start_iter; - input_buffer#set_modified false; - !pop_info (); - !flash_info "Buffer reverted"; - Highlight.highlight_all input_buffer; - with _ -> - !pop_info (); - !flash_info "Warning: could not revert buffer"; - end - in - if input_buffer#modified then - match (GToolbox.question_box - ~title:"Modified buffer changed on disk" - ~buttons:["Revert from File"; - "Overwrite File"; - "Disable Auto Revert"] - ~default:0 - ~icon:(stock_to_widget `DIALOG_WARNING) - "Some unsaved buffers changed on disk" - ) - with 1 -> do_revert () - | 2 -> if self#save f then !flash_info "Overwritten" else - !flash_info "Could not overwrite file" - | _ -> - prerr_endline "Auto revert set to false"; - !current.global_auto_revert <- false; - disconnect_revert_timer () - else do_revert () - end + let do_revert () = begin + push_info "Reverting buffer"; + try + if is_active then self#reset_initial; + let b = Buffer.create 1024 in + with_file flash_info f ~f:(input_channel b); + let s = try_convert (Buffer.contents b) in + input_buffer#set_text s; + self#update_stats; + input_buffer#place_cursor input_buffer#start_iter; + input_buffer#set_modified false; + pop_info (); + flash_info "Buffer reverted"; + force_retag input_buffer; + with _ -> + pop_info (); + flash_info "Warning: could not revert buffer"; + end + in + if input_buffer#modified then + match (GToolbox.question_box + ~title:"Modified buffer changed on disk" + ~buttons:["Revert from File"; + "Overwrite File"; + "Disable Auto Revert"] + ~default:0 + ~icon:(stock_to_widget `DIALOG_WARNING) + "Some unsaved buffers changed on disk" + ) + with 1 -> do_revert () + | 2 -> if self#save f then flash_info "Overwritten" else + flash_info "Could not overwrite file" + | _ -> + prerr_endline "Auto revert set to false"; + !current.global_auto_revert <- false; + disconnect_revert_timer () + else do_revert () + end | None -> () - - method save f = + + method save f = if try_export f (input_buffer#get_text ()) then begin - filename <- Some f; - input_buffer#set_modified false; - stats <- my_stat f; - (match self#auto_save_name with - | None -> () - | Some fn -> try Sys.remove fn with _ -> ()); - true - end + filename <- Some f; + input_buffer#set_modified false; + stats <- my_stat f; + (match self#auto_save_name with + | None -> () + | Some fn -> try Sys.remove fn with _ -> ()); + true + end else false - method private auto_save_name = - match filename with + method private auto_save_name = + match filename with | None -> None - | Some f -> - let dir = Filename.dirname f in - let base = (fst !current.auto_save_name) ^ - (Filename.basename f) ^ - (snd !current.auto_save_name) - in Some (Filename.concat dir base) - - method private need_auto_save = + | Some f -> + let dir = Filename.dirname f in + let base = (fst !current.auto_save_name) ^ + (Filename.basename f) ^ + (snd !current.auto_save_name) + in Some (Filename.concat dir base) + + method private need_auto_save = input_buffer#modified && - last_modification_time > last_auto_save_time - + last_modification_time > last_auto_save_time + method auto_save = if self#need_auto_save then begin - match self#auto_save_name with - | None -> () - | Some fn -> - try - last_auto_save_time <- Unix.time(); - prerr_endline ("Autosave time : "^(string_of_float (Unix.time()))); - if try_export fn (input_buffer#get_text ()) then begin - !flash_info ~delay:1000 "Autosaved" - end - else warning - ("Autosave failed (check if " ^ fn ^ " is writable)") - with _ -> - warning ("Autosave: unexpected error while writing "^fn) - end - + match self#auto_save_name with + | None -> () + | Some fn -> + try + last_auto_save_time <- Unix.time(); + prerr_endline ("Autosave time : "^(string_of_float (Unix.time()))); + if try_export fn (input_buffer#get_text ()) then begin + flash_info ~delay:1000 "Autosaved" + end + else warning + ("Autosave failed (check if " ^ fn ^ " is writable)") + with _ -> + warning ("Autosave: unexpected error while writing "^fn) + end + method save_as f = - if Sys.file_exists f then + if Sys.file_exists f then match (GToolbox.question_box ~title:"File exists on disk" - ~buttons:["Overwrite"; - "Cancel";] - ~default:1 - ~icon: - (let img = GMisc.image () in - img#set_stock `DIALOG_WARNING; - img#set_icon_size `DIALOG; - img#coerce) - ("File "^f^"already exists") - ) + ~buttons:["Overwrite"; + "Cancel";] + ~default:1 + ~icon: + (let img = GMisc.image () in + img#set_stock `DIALOG_WARNING; + img#set_icon_size `DIALOG; + img#coerce) + ("File "^f^"already exists") + ) with 1 -> self#save f - | _ -> false - else self#save f + | _ -> false + else self#save f method set_read_only b = read_only<-b method read_only = read_only @@ -823,585 +675,494 @@ object(self) method clear_message = message_buffer#set_text "" val mutable last_index = true val last_array = [|"";""|] - method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input") + method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input") method get_insert = get_insert input_buffer - method recenter_insert = - (* BUG : to investigate further: - FIXED : Never call GMain.* in thread ! - PLUS : GTK BUG ??? Cannot be called from a thread... - ADDITION: using sync instead of async causes deadlock...*) + method recenter_insert = + (* BUG : to investigate further: + FIXED : Never call GMain.* in thread ! + PLUS : GTK BUG ??? Cannot be called from a thread... + ADDITION: using sync instead of async causes deadlock...*) ignore (GtkThread.async ( - input_view#scroll_to_mark - ~use_align:false - ~yalign:0.75 - ~within_margin:0.25) - `INSERT) + input_view#scroll_to_mark + ~use_align:false + ~yalign:0.75 + ~within_margin:0.25) + `INSERT) - method indent_current_line = + method indent_current_line = let get_nb_space it = let it = it#copy in let nb_sep = ref 0 in let continue = ref true in - while !continue do - if it#char = space then begin - incr nb_sep; - if not it#nocopy#forward_char then continue := false; - end else continue := false - done; - !nb_sep + while !continue do + if it#char = space then begin + incr nb_sep; + if not it#nocopy#forward_char then continue := false; + end else continue := false + done; + !nb_sep in let previous_line = self#get_insert in if previous_line#nocopy#backward_line then begin - let previous_line_spaces = get_nb_space previous_line in - let current_line_start = self#get_insert#set_line_offset 0 in - let current_line_spaces = get_nb_space current_line_start in - if input_buffer#delete_interactive - ~start:current_line_start - ~stop:(current_line_start#forward_chars current_line_spaces) - () - then - let current_line_start = self#get_insert#set_line_offset 0 in - input_buffer#insert - ~iter:current_line_start - (String.make previous_line_spaces ' ') - end + let previous_line_spaces = get_nb_space previous_line in + let current_line_start = self#get_insert#set_line_offset 0 in + let current_line_spaces = get_nb_space current_line_start in + if input_buffer#delete_interactive + ~start:current_line_start + ~stop:(current_line_start#forward_chars current_line_spaces) + () + then + let current_line_start = self#get_insert#set_line_offset 0 in + input_buffer#insert + ~iter:current_line_start + (String.make previous_line_spaces ' ') + end - method show_pm_goal = - proof_buffer#insert - (Printf.sprintf " *** Declarative Mode ***\n"); - try - let (hyps,concl) = get_current_pm_goal () in - List.iter - (fun ((_,_,_,(s,_)) as _hyp) -> - proof_buffer#insert (s^"\n")) - hyps; - proof_buffer#insert - (String.make 38 '_' ^ "\n"); - let (_,_,_,s) = concl in - proof_buffer#insert ("thesis := \n "^s^"\n"); - let my_mark = `NAME "end_of_conclusion" in - proof_buffer#move_mark - ~where:((proof_buffer#get_iter_at_mark `INSERT)) - my_mark; - ignore (proof_view#scroll_to_mark my_mark) - with Not_found -> + method show_pm_goal = + proof_buffer#insert + (Printf.sprintf " *** Declarative Mode ***\n"); + try + let (hyps,concl) = get_current_pm_goal () in + List.iter + (fun ((_,_,_,(s,_)) as _hyp) -> + proof_buffer#insert (s^"\n")) + hyps; + proof_buffer#insert + (String.make 38 '_' ^ "\n"); + let (_,_,_,s) = concl in + proof_buffer#insert ("thesis := \n "^s^"\n"); + let my_mark = `NAME "end_of_conclusion" in + proof_buffer#move_mark + ~where:((proof_buffer#get_iter_at_mark `INSERT)) + my_mark; + ignore (proof_view#scroll_to_mark my_mark) + with Not_found -> match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with - Some endc -> - proof_buffer#insert - ("Subproof completed, now type "^endc^".") - | None -> - proof_buffer#insert "Proof completed." + Some endc -> + proof_buffer#insert + ("Subproof completed, now type "^endc^".") + | None -> + proof_buffer#insert "Proof completed." + - method show_goals = - try - proof_view#buffer#set_text ""; - match Decl_mode.get_current_mode () with - Decl_mode.Mode_none -> proof_buffer#insert (Coq.print_no_goal ()) - | Decl_mode.Mode_tactic -> - begin - let s = Coq.get_current_goals () in - match s with - | [] -> proof_buffer#insert (Coq.print_no_goal ()) - | (hyps,concl)::r -> - let goal_nb = List.length s in - proof_buffer#insert - (Printf.sprintf "%d subgoal%s\n" - goal_nb - (if goal_nb<=1 then "" else "s")); - List.iter - (fun ((_,_,_,(s,_)) as _hyp) -> - proof_buffer#insert (s^"\n")) - hyps; - proof_buffer#insert - (String.make 38 '_' ^ "(1/"^ - (string_of_int goal_nb)^ - ")\n") ; - let _,_,_,sconcl = concl in - proof_buffer#insert sconcl; - proof_buffer#insert "\n"; - let my_mark = `NAME "end_of_conclusion" in - proof_buffer#move_mark - ~where:((proof_buffer#get_iter_at_mark `INSERT)) - my_mark; - proof_buffer#insert "\n\n"; - let i = ref 1 in - List.iter - (function (_,(_,_,_,concl)) -> - incr i; - proof_buffer#insert - (String.make 38 '_' ^"("^ - (string_of_int !i)^ - "/"^ - (string_of_int goal_nb)^ - ")\n"); - proof_buffer#insert concl; - proof_buffer#insert "\n\n"; - ) - r; - ignore (proof_view#scroll_to_mark my_mark) - end - | Decl_mode.Mode_proof -> - self#show_pm_goal - with e -> - prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e) - - val mutable full_goal_done = true - method show_goals_full = + method show_goals_full = if not full_goal_done then begin - try - proof_view#buffer#set_text ""; - match Decl_mode.get_current_mode () with - Decl_mode.Mode_none -> - proof_buffer#insert (Coq.print_no_goal ()) - | Decl_mode.Mode_tactic -> - begin - match Coq.get_current_goals () with - [] -> Util.anomaly "show_goals_full" - | ((hyps,concl)::r) as s -> - let last_shown_area = - proof_buffer#create_tag [`BACKGROUND "light green"] - in - let goal_nb = List.length s in - proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" - goal_nb - (if goal_nb<=1 then "" else "s")); - let coq_menu commands = - let tag = proof_buffer#create_tag [] - in - ignore - (tag#connect#event ~callback: - (fun ~origin ev it -> - begin match GdkEvent.get_type ev with - | `BUTTON_PRESS -> - let ev = (GdkEvent.Button.cast ev) in - if (GdkEvent.Button.button ev) = 3 - then begin - let loc_menu = GMenu.menu () in - let factory = - new GMenu.factory loc_menu in - let add_coq_command (cp,ip) = - ignore - (factory#add_item cp - ~callback: - (fun () -> ignore - (self#insert_this_phrase_on_success - true - true - false - ("progress "^ip^"\n") - (ip^"\n")) - ) - ) - in - List.iter add_coq_command commands; - loc_menu#popup - ~button:3 - ~time:(GdkEvent.Button.time ev); - end - | `MOTION_NOTIFY -> - proof_buffer#remove_tag - ~start:proof_buffer#start_iter - ~stop:proof_buffer#end_iter - last_shown_area; - prerr_endline "Before find_tag_limits"; - - let s,e = find_tag_limits tag - (new GText.iter it) - in - prerr_endline "After find_tag_limits"; - proof_buffer#apply_tag - ~start:s - ~stop:e - last_shown_area; - - prerr_endline "Applied tag"; - () - | _ -> () - end;false - ) - ); - tag - in - List.iter - (fun ((_,_,_,(s,_)) as hyp) -> - let tag = coq_menu (hyp_menu hyp) in - proof_buffer#insert ~tags:[tag] (s^"\n")) - hyps; - proof_buffer#insert - (String.make 38 '_' ^"(1/"^ - (string_of_int goal_nb)^ - ")\n") - ; - let tag = coq_menu (concl_menu concl) in - let _,_,_,sconcl = concl in - proof_buffer#insert ~tags:[tag] sconcl; - proof_buffer#insert "\n"; - let my_mark = `NAME "end_of_conclusion" in - proof_buffer#move_mark - ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark; - proof_buffer#insert "\n\n"; - let i = ref 1 in - List.iter - (function (_,(_,_,_,concl)) -> - incr i; - proof_buffer#insert - (String.make 38 '_' ^"("^ - (string_of_int !i)^ - "/"^ - (string_of_int goal_nb)^ - ")\n"); - proof_buffer#insert concl; - proof_buffer#insert "\n\n"; - ) - r; - ignore (proof_view#scroll_to_mark my_mark) ; - full_goal_done <- true - end - | Decl_mode.Mode_proof -> - self#show_pm_goal - with e -> prerr_endline (Printexc.to_string e) + try + proof_buffer#set_text ""; + match Decl_mode.get_current_mode () with + Decl_mode.Mode_none -> () + | Decl_mode.Mode_tactic -> + begin + match Coq.get_current_goals () with + [] -> proof_buffer#insert (Coq.print_no_goal()) + | ((hyps,concl)::r) as s -> + let last_shown_area = Tags.Proof.highlight + in + let goal_nb = List.length s in + proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" + goal_nb + (if goal_nb<=1 then "" else "s")); + let coq_menu commands = + let tag = proof_buffer#create_tag [] + in + ignore + (tag#connect#event ~callback: + (fun ~origin ev it -> + match GdkEvent.get_type ev with + | `BUTTON_PRESS -> + let ev = (GdkEvent.Button.cast ev) in + if (GdkEvent.Button.button ev) = 3 + then ( + let loc_menu = GMenu.menu () in + let factory = + new GMenu.factory loc_menu in + let add_coq_command (cp,ip) = + ignore + (factory#add_item cp + ~callback: + (fun () -> ignore + (self#insert_this_phrase_on_success + true + true + false + ("progress "^ip^"\n") + (ip^"\n")) + ) + ) + in + List.iter add_coq_command commands; + loc_menu#popup + ~button:3 + ~time:(GdkEvent.Button.time ev); + true) + else false + | `MOTION_NOTIFY -> + proof_buffer#remove_tag + ~start:proof_buffer#start_iter + ~stop:proof_buffer#end_iter + last_shown_area; + prerr_endline "Before find_tag_limits"; + + let s,e = find_tag_limits tag + (new GText.iter it) + in + prerr_endline "After find_tag_limits"; + proof_buffer#apply_tag + ~start:s + ~stop:e + last_shown_area; + + prerr_endline "Applied tag"; + false + | _ -> + false + ) + ); + tag + in + List.iter + (fun ((_,_,_,(s,_)) as hyp) -> + let tag = coq_menu (hyp_menu hyp) in + proof_buffer#insert ~tags:[tag] (s^"\n")) + hyps; + proof_buffer#insert + (String.make 38 '_' ^"(1/"^ + (string_of_int goal_nb)^ + ")\n") + ; + let tag = coq_menu (concl_menu concl) in + let _,_,_,sconcl = concl in + proof_buffer#insert ~tags:[tag] sconcl; + proof_buffer#insert "\n"; + let my_mark = `NAME "end_of_conclusion" in + proof_buffer#move_mark + ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark; + proof_buffer#insert "\n\n"; + let i = ref 1 in + List.iter + (function (_,(_,_,_,concl)) -> + incr i; + proof_buffer#insert + (String.make 38 '_' ^"("^ + (string_of_int !i)^ + "/"^ + (string_of_int goal_nb)^ + ")\n"); + proof_buffer#insert concl; + proof_buffer#insert "\n\n"; + ) + r; + ignore (proof_view#scroll_to_mark my_mark) ; + full_goal_done <- true + end + | Decl_mode.Mode_proof -> + self#show_pm_goal + with e -> prerr_endline (Printexc.to_string e) end - + + method show_goals = self#show_goals_full + + method send_to_coq verbosely replace phrase show_output show_error localize = 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#insert_message s; - message_view#misc#draw None; - if localize then - (match Option.map Util.unloc loc with - | None -> () - | Some (start,stop) -> - let convert_pos = byte_offset_to_char_offset phrase in - let start = convert_pos start in - let stop = convert_pos stop in - let i = self#get_start_of_input in - let starti = i#forward_chars start in - let stopi = i#forward_chars stop in - input_buffer#apply_tag_by_name "error" - ~start:starti - ~stop:stopi; - input_buffer#place_cursor starti) in - try - full_goal_done <- false; - prerr_endline "Send_to_coq starting now"; - Decl_mode.clear_daimon_flag (); - if replace then begin - let r,info = Coq.interp_and_replace ("info " ^ phrase) in - let complete = not (Decl_mode.get_daimon_flag ()) in - let msg = read_stdout () in - sync display_output msg; - Some (complete,r) - end else begin - let r = Coq.interp verbosely phrase in - let complete = not (Decl_mode.get_daimon_flag ()) in - let msg = read_stdout () in - sync display_output msg; - Some (complete,r) - end - with e -> - if show_error then sync display_error e; - None - - method find_phrase_starting_at (start:GText.iter) = - prerr_endline "find_phrase_starting_at starting now"; - let trash_bytes = ref "" in - let end_iter = start#copy in - let lexbuf_function s count = - let i = ref 0 in - let n_trash = String.length !trash_bytes in - String.blit !trash_bytes 0 s 0 n_trash; - i := n_trash; - try - while !i <= count - 1 do - let c = end_iter#char in - if c = 0 then raise (Stop !i); - let c' = Glib.Utf8.from_unichar c in - let n = String.length c' in - if (n<=0) then exit (-2); - if n > count - !i then - begin - let ri = count - !i in - String.blit c' 0 s !i ri; - trash_bytes := String.sub c' ri (n-ri); - i := count ; - end else begin - String.blit c' 0 s !i n; - i:= !i + n - end; - if not end_iter#nocopy#forward_char then - raise (Stop !i) - done; - count - with Stop x -> - x - in + assert (Glib.Utf8.validate s); + self#insert_message s; + message_view#misc#draw None; + if localize then + (match Option.map Util.unloc loc with + | None -> () + | Some (start,stop) -> + let convert_pos = byte_offset_to_char_offset phrase in + let start = convert_pos start in + let stop = convert_pos stop in + let i = self#get_start_of_input in + let starti = i#forward_chars start in + let stopi = i#forward_chars stop in + input_buffer#apply_tag Tags.Script.error + ~start:starti + ~stop:stopi; + input_buffer#place_cursor starti) in try - trash_bytes := ""; - let _ = Find_phrase.get (Lexing.from_function lexbuf_function) - in - end_iter#nocopy#set_offset (start#offset + !Find_phrase.length); - Some (start,end_iter) - with - (* - | Find_phrase.EOF s -> - (* Phrase is at the end of the buffer*) - let si = start#offset in - let ei = si + !Find_phrase.length in - end_iter#nocopy#set_offset (ei - 1); - input_buffer#insert ~iter:end_iter "\n"; - Some (input_buffer#get_iter (`OFFSET si), - input_buffer#get_iter (`OFFSET ei)) - *) - | _ -> None - - method complete_at_offset (offset:int) = + full_goal_done <- false; + prerr_endline "Send_to_coq starting now"; + Decl_mode.clear_daimon_flag (); + if replace then begin + let r,info = Coq.interp_and_replace ("info " ^ phrase) in + let is_complete = not (Decl_mode.get_daimon_flag ()) in + let msg = read_stdout () in + sync display_output msg; + Some (is_complete,r) + end else begin + let r = Coq.interp verbosely phrase in + let is_complete = not (Decl_mode.get_daimon_flag ()) in + let msg = read_stdout () in + sync display_output msg; + Some (is_complete,r) + end + with e -> + if show_error then sync display_error e; + None + + method find_phrase_starting_at (start:GText.iter) = + try + let start = grab_safe_sentence_start start self#get_start_of_input in + let stop = grab_sentence_end_from start in + if stop#backward_char#has_tag Tags.Script.lax_end then + Some (start,stop) + else + None + with Not_found -> None + + method complete_at_offset (offset:int) = prerr_endline ("Completion at offset : " ^ string_of_int offset); let it () = input_buffer#get_iter (`OFFSET offset) in let iit = it () in let start = find_word_start iit in - if ends_word iit then - let w = input_buffer#get_text - ~start - ~stop:iit - () - in - 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) -> - let completion = input_buffer#get_text ~start ~stop () in - ignore (input_buffer#delete_selection ()); - 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 verbosely display_goals do_highlight = + if ends_word iit then + let w = input_buffer#get_text + ~start + ~stop:iit + () + in + 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) -> + let completion = input_buffer#get_text ~start ~stop () in + ignore (input_buffer#delete_selection ()); + 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 verbosely display_goals do_highlight = 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; + 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; None - | Some(start,stop) -> - prerr_endline "process_next_phrase : to_process highlight"; - 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"; + | Some(start,stop) -> + prerr_endline "process_next_phrase : to_process highlight"; + if do_highlight then begin + input_buffer#apply_tag Tags.Script.to_process ~start ~stop; + prerr_endline "process_next_phrase : to_process applied"; + end; + prerr_endline "process_next_phrase : getting phrase"; 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 reset_info complete (start,stop) ast = - let b = input_buffer in - b#move_mark ~where:stop (`NAME "start_of_input"); - b#apply_tag_by_name - (if complete then "processed" else "unjustified") ~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 - reset_info - 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) -> + input_buffer#remove_tag Tags.Script.to_process ~start ~stop; + input_view#set_editable true; + pop_info (); + end in + let mark_processed reset_info is_complete (start,stop) = + let b = input_buffer in + b#move_mark ~where:stop (`NAME "start_of_input"); + b#apply_tag + (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + begin + b#place_cursor stop; + self#recenter_insert + end; + let ide_payload = { start = `MARK (b#create_mark start); + stop = `MARK (b#create_mark stop); } in + push_phrase + cmd_stack + reset_info + ide_payload; + 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 (complete,(reset_info,ast)) -> - sync (mark_processed reset_info complete) loc ast; true - | None -> sync remove_tag loc; false) - end - - method insert_this_phrase_on_success - show_output show_msg localize coqphrase insertphrase = - let mark_processed reset_info complete ast = + | Some (is_complete,reset_info) -> + sync (mark_processed reset_info is_complete) loc; true + | None -> sync remove_tag loc; false) + end + + method insert_this_phrase_on_success + show_output show_msg localize coqphrase insertphrase = + let mark_processed reset_info is_complete = 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 - (if complete then "processed" else "unjustified") ~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 reset_info 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 - reset_info start_of_phrase_mark end_of_phrase_mark ast - end - | None -> ()) - | _ -> ()) - with _ -> ()*) in - match self#send_to_coq false false coqphrase show_output show_msg localize with - | Some (complete,(reset_info,ast)) -> - sync (mark_processed reset_info complete) ast; true - | None -> - sync - (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) - (); - false + 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 + (if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + input_buffer#place_cursor stop; + let ide_payload = { start = `MARK (input_buffer#create_mark start); + stop = `MARK (input_buffer#create_mark stop); } in + push_phrase cmd_stack reset_info ide_payload; + 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 + reset_info start_of_phrase_mark end_of_phrase_mark ast + end + | None -> ()) + | _ -> ()) + with _ -> ()*) in + match self#send_to_coq false false coqphrase show_output show_msg localize with + | Some (is_complete,reset_info) -> + sync (mark_processed reset_info) is_complete; 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 sync (fun _ -> - input_buffer#apply_tag_by_name ~start ~stop "to_process"; - input_view#set_editable false) (); - !push_info "Coq is computing"; + input_buffer#apply_tag Tags.Script.to_process ~start ~stop; + input_view#set_editable false) (); + push_info "Coq is computing"; let get_current () = - if !current.stop_before then + if !current.stop_before then match self#find_phrase_starting_at self#get_start_of_input with | None -> self#get_start_of_input | Some (_, stop2) -> stop2 - else begin - self#get_start_of_input - end - in - (try - while ((stop#compare (get_current())>=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"); - 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 = + else begin + self#get_start_of_input + end + in + (try + while ((stop#compare (get_current())>=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"); + 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 Tags.Script.to_process ~start ~stop; + 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 = 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#remove_tag_by_name "unjustified" ~start ~stop; - input_buffer#delete_mark inf.start; - input_buffer#delete_mark inf.stop; - ) - processed_stack; - Stack.clear processed_stack; - self#clear_message)(); + 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 Tags.Script.processed ~start ~stop; + input_buffer#remove_tag Tags.Script.unjustified ~start ~stop; + input_buffer#delete_mark inf.start; + input_buffer#delete_mark inf.stop; + ) + cmd_stack; + Stack.clear cmd_stack; + self#clear_message)(); Coq.reset_initial () (* backtrack Coq to the phrase preceding iterator [i] *) method backtrack_to_no_lock i = prerr_endline "Backtracking_to iter starts now."; (* pop Coq commands until we reach iterator [i] *) - let rec pop_commands done_smthg undos = - if is_empty () then - done_smthg, undos + let rec pop_cmds popped = + if Stack.is_empty cmd_stack then + popped else - let t = top () in - if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then + let (ide,coq) = Stack.pop cmd_stack in + if i#compare (input_buffer#get_iter_at_mark ide.stop) < 0 then begin - prerr_endline "Popped top command"; - pop_commands true (pop_command undos t) - end + prerr_endline "popped command"; + pop_cmds (coq::popped) + end else - done_smthg, undos + begin + Stack.push (ide,coq) cmd_stack; + popped + end in - let undos = (0,0,NoBacktrack,0,undo_info()) in - let done_smthg, undos = pop_commands false undos in + let seq = List.rev (pop_cmds []) in prerr_endline "Popped commands"; - if done_smthg then - begin - try - apply_undos undos; + if 0 < List.length seq then + begin + try + rewind seq cmd_stack; 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"; - input_buffer#remove_tag_by_name - ~start - ~stop:self#get_start_of_input - "unjustified"; - 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) + let start = + if Stack.is_empty cmd_stack then input_buffer#start_iter + else input_buffer#get_iter_at_mark (fst (Stack.top cmd_stack)).stop in + prerr_endline "Removing (long) processed tag..."; + input_buffer#remove_tag + Tags.Script.processed + ~start + ~stop:self#get_start_of_input; + input_buffer#remove_tag + Tags.Script.unjustified + ~start + ~stop:self#get_start_of_input; + prerr_endline "Moving (long) start_of_input..."; + input_buffer#move_mark ~where:start (`NAME "start_of_input"); + full_goal_done <- false; + 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."; - end - else prerr_endline "backtrack_to : discarded (...)" - - method backtrack_to i = - if Mutex.try_lock coq_may_stop then - (!push_info "Undoing..."; + with _ -> + push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. + Please restart and report NOW."; + end + else prerr_endline "backtrack_to : discarded (...)" + + method backtrack_to i = + if Mutex.try_lock coq_may_stop then + (push_info "Undoing..."; self#backtrack_to_no_lock i; Mutex.unlock coq_may_stop; - !pop_info ()) + pop_info ()) else prerr_endline "backtrack_to : discarded (lock is busy)" method go_to_insert = @@ -1411,405 +1172,278 @@ Please restart and report NOW."; else self#backtrack_to point method undo_last_step = - if Mutex.try_lock coq_may_stop then - (!push_info "Undoing last step..."; + if Mutex.try_lock coq_may_stop then + (push_info "Undoing last step..."; (try - let last_command = top () in - let start = input_buffer#get_iter_at_mark last_command.start in - let update_input () = - prerr_endline "Removing processed tag..."; - input_buffer#remove_tag_by_name - ~start - ~stop:(input_buffer#get_iter_at_mark last_command.stop) - "processed"; - input_buffer#remove_tag_by_name - ~start - ~stop:(input_buffer#get_iter_at_mark last_command.stop) - "unjustified"; - prerr_endline "Moving start_of_input"; - input_buffer#move_mark - ~where:start - (`NAME "start_of_input"); - input_buffer#place_cursor start; - self#recenter_insert; - self#show_goals; - self#clear_message - in - let undo = pop_command (0,0,NoBacktrack,0,undo_info()) last_command in - apply_undos undo; - sync update_input () - with - | Size 0 -> (* !flash_info "Nothing to Undo"*)() + let (ide_ri,_) = Stack.top cmd_stack in + let start = input_buffer#get_iter_at_mark ide_ri.start in + let update_input () = + prerr_endline "Removing processed tag..."; + input_buffer#remove_tag + Tags.Script.processed + ~start + ~stop:(input_buffer#get_iter_at_mark ide_ri.stop); + input_buffer#remove_tag + Tags.Script.unjustified + ~start + ~stop:(input_buffer#get_iter_at_mark ide_ri.stop); + prerr_endline "Moving start_of_input"; + input_buffer#move_mark + ~where:start + (`NAME "start_of_input"); + input_buffer#place_cursor start; + self#recenter_insert; + full_goal_done <- false; + self#show_goals; + self#clear_message + in + let _,coq = Stack.pop cmd_stack in + rewind [coq] cmd_stack; + sync update_input () + with + | Stack.Empty -> (* flash_info "Nothing to Undo"*)() ); - !pop_info (); + pop_info (); Mutex.unlock coq_may_stop) else prerr_endline "undo_last_step discarded" - - method blaster () = - - ignore (Thread.create - (fun () -> - prerr_endline "Blaster called"; - let c = Blaster_window.present_blaster_window () in - if Mutex.try_lock c#lock then begin - c#clear (); - Decl_mode.check_not_proof_mode "No blaster in Proof mode"; - let current_gls = try get_current_goals () with _ -> [] in - - let set_goal i (s,t) = - let gnb = string_of_int i in - let s = gnb ^":"^s in - let t' = gnb ^": progress "^t in - let t'' = gnb ^": "^t in - c#set - ("Goal "^gnb) - s - (fun () -> try_interptac 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)) - (sync(fun () -> self#insert_command t t)) - in - begin match current_gls with - | [] -> () - | (hyp_l,current_gl)::r -> - List.iter set_current_goal (concl_menu current_gl); - List.iter - (fun hyp -> - List.iter set_current_goal (hyp_menu hyp)) - hyp_l; - let i = ref 2 in - List.iter - (fun (hyp_l,gl) -> - List.iter (set_goal !i) (concl_menu gl); - incr i) - r - end; - let _ = c#blaster () in - Mutex.unlock c#lock - end else prerr_endline "Blaster discarded") - ()) - - method insert_command cp ip = + + method insert_command cp ip = async(fun _ -> self#clear_message)(); ignore (self#insert_this_phrase_on_success true false false cp ip) method tactic_wizard l = async(fun _ -> self#clear_message)(); - ignore - (List.exists - (fun p -> - self#insert_this_phrase_on_success true false false - ("progress "^p^".\n") (p^".\n")) l) - - method active_keypress_handler k = + ignore + (List.exists + (fun p -> + self#insert_this_phrase_on_success true false false + ("progress "^p^".\n") (p^".\n")) l) + + method active_keypress_handler k = let state = GdkEvent.Key.state k in begin - match state with - | l when List.mem `MOD1 l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._Return=k - then ignore( - if (input_buffer#insert_interactive "\n") then - begin - let i= self#get_insert#backward_word_start in - prerr_endline "active_kp_hf: Placing cursor"; - self#process_until_iter_or_error i - end); - true - | l when List.mem `CONTROL l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._Break=k - then break (); - false - | l -> - if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin - prerr_endline "active_kp_handler for Tab"; - self#indent_current_line; - true - end else false + match state with + | l when List.mem `MOD1 l -> + let k = GdkEvent.Key.keyval k in + if GdkKeysyms._Return=k + then ignore( + if (input_buffer#insert_interactive "\n") then + begin + let i= self#get_insert#backward_word_start in + prerr_endline "active_kp_hf: Placing cursor"; + self#process_until_iter_or_error i + end); + true + | l when List.mem `CONTROL l -> + let k = GdkEvent.Key.keyval k in + if GdkKeysyms._Break=k + then break (); + false + | l -> + if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin + prerr_endline "active_kp_handler for Tab"; + self#indent_current_line; + true + end else false end - method disconnected_keypress_handler k = + + + method disconnected_keypress_handler k = match GdkEvent.Key.state k with - | l when List.mem `CONTROL l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._c=k - then break (); - false + | l when List.mem `CONTROL l -> + let k = GdkEvent.Key.keyval k in + if GdkKeysyms._c=k + then break (); + false | l -> false - + val mutable deact_id = None val mutable act_id = None - method deactivate () = + method deactivate () = is_active <- false; - (match act_id with None -> () + (match act_id with None -> () | Some id -> - reset_initial (); - input_view#misc#disconnect id; - prerr_endline "DISCONNECTED old active : "; - print_id id; - ); - deact_id <- Some - (input_view#event#connect#key_press self#disconnected_keypress_handler); + reset_initial (); + input_view#misc#disconnect id; + prerr_endline "DISCONNECTED old active : "; + print_id id; + )(*; + deact_id <- Some + (input_view#event#connect#key_press self#disconnected_keypress_handler); prerr_endline "CONNECTED inactive : "; - print_id (Option.get deact_id) + print_id (Option.get deact_id)*) + (* XXX *) method activate () = - is_active <- true; - (match deact_id with None -> () + is_active <- true;(* + (match deact_id with None -> () | Some id -> input_view#misc#disconnect id; - prerr_endline "DISCONNECTED old inactive : "; - print_id id - ); - act_id <- Some - (input_view#event#connect#key_press self#active_keypress_handler); + prerr_endline "DISCONNECTED old inactive : "; + print_id id + );*) + act_id <- Some + (input_view#event#connect#key_press self#active_keypress_handler); prerr_endline "CONNECTED active : "; print_id (Option.get act_id); - match - (Option.get ((Vector.get input_views index).analyzed_view)) #filename + match + filename with | None -> () | Some f -> let dir = Filename.dirname f in - if not (is_in_loadpath dir) then - begin - ignore (Coq.interp false - (Printf.sprintf "Add LoadPath \"%s\". " dir)) - end - - method electric_handler = + if not (is_in_loadpath dir) then + begin + ignore (Coq.interp false + (Printf.sprintf "Add LoadPath \"%s\". " dir)) + end + + method electric_handler = input_buffer#connect#insert_text ~callback: - (fun it x -> - begin try - if last_index then begin - last_array.(0)<-x; - if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found - end else begin - last_array.(1)<-x; - if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found - end - with Found -> - begin - ignore (self#process_next_phrase false true true) - end; - end; - last_index <- not last_index;) + (fun it x -> + begin try + if last_index then begin + last_array.(0)<-x; + if (last_array.(1) ^ last_array.(0) = ".\n") then raise Found + end else begin + last_array.(1)<-x; + if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found + end + with Found -> + begin + ignore (self#process_next_phrase false true true) + end; + end; + last_index <- not last_index;) method private electric_paren tag = let oparen_code = Glib.Utf8.to_unichar "(" (ref 0) in let cparen_code = Glib.Utf8.to_unichar ")" (ref 0) in ignore (input_buffer#connect#insert_text ~callback: - (fun it x -> - input_buffer#remove_tag - ~start:input_buffer#start_iter - ~stop:input_buffer#end_iter - tag; - if x = "" then () else - match x.[String.length x - 1] with - | ')' -> - let hit = self#get_insert in - let count = ref 0 in - if hit#nocopy#backward_find_char - (fun c -> - if c = oparen_code && !count = 0 then true - else if c = cparen_code then - (incr count;false) - else if c = oparen_code then - (decr count;false) - else false - ) - then - begin - prerr_endline "Found matching parenthesis"; - input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char - end - else () - | _ -> ()) - ) + (fun it x -> + input_buffer#remove_tag + ~start:input_buffer#start_iter + ~stop:input_buffer#end_iter + tag; + if x = "" then () else + match x.[String.length x - 1] with + | ')' -> + let hit = self#get_insert in + let count = ref 0 in + if hit#nocopy#backward_find_char + (fun c -> + if c = oparen_code && !count = 0 then true + else if c = cparen_code then + (incr count;false) + else if c = oparen_code then + (decr count;false) + else false + ) + then + begin + prerr_endline "Found matching parenthesis"; + input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char + end + else () + | _ -> ()) + ) + + method help_for_keyword () = - method help_for_keyword () = - browse_keyword (self#insert_message) (get_current_word ()) - initializer + initializer ignore (message_buffer#connect#insert_text - ~callback:(fun it s -> ignore - (message_view#scroll_to_mark - ~use_align:false - ~within_margin:0.49 - `INSERT))); + ~callback:(fun it s -> ignore + (message_view#scroll_to_mark + ~use_align:false + ~within_margin:0.49 + `INSERT))); ignore (input_buffer#connect#insert_text - ~callback:(fun it s -> - if (it#compare self#get_start_of_input)<0 - then GtkSignal.stop_emit (); - if String.length s > 1 then - (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it))); + ~callback:(fun it s -> + if (it#compare self#get_start_of_input)<0 + then GtkSignal.stop_emit (); + if String.length s > 1 then + (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it))); ignore (input_buffer#connect#after#apply_tag - ~callback:(fun tag ~start ~stop -> - if (start#compare self#get_start_of_input)>=0 - then - begin - input_buffer#remove_tag_by_name - ~start - ~stop - "processed"; - input_buffer#remove_tag_by_name - ~start - ~stop - "unjustified" - end - ) - ); + ~callback:(fun tag ~start ~stop -> + if (start#compare self#get_start_of_input)>=0 + then + begin + input_buffer#remove_tag + Tags.Script.processed + ~start + ~stop; + input_buffer#remove_tag + Tags.Script.unjustified + ~start + ~stop + end + ) + ); ignore (input_buffer#connect#after#insert_text - ~callback:(fun it s -> - if auto_complete_on && - String.length s = 1 && s <> " " && s <> "\n" - then - let v = Option.get (get_current_view ()).analyzed_view - in - let has_completed = - v#complete_at_offset - ((v#view#buffer#get_iter `SEL_BOUND)#offset) - in - if has_completed then - input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char; - - - ) - ); - ignore (input_buffer#connect#modified_changed - ~callback: - (fun () -> - if input_buffer#modified then - set_tab_image index - ~icon:(match (Option.get (current_all.analyzed_view))#filename with - | None -> `SAVE_AS - | Some _ -> `SAVE - ) - else set_tab_image index ~icon:`YES; - )); + ~callback:(fun it s -> + if auto_complete_on && + String.length s = 1 && s <> " " && s <> "\n" + then + let v = session_notebook#current_term.analyzed_view + in + let has_completed = + v#complete_at_offset + ((input_view#buffer#get_iter `SEL_BOUND)#offset) + in + if has_completed then + input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char; + + + ) + ); ignore (input_buffer#connect#changed - ~callback:(fun () -> - last_modification_time <- Unix.time (); - let r = input_view#visible_rect in - let stop = - input_view#get_iter_at_location - ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r) - ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r) - in - input_buffer#remove_tag_by_name - ~start:self#get_start_of_input - ~stop - "error"; - Highlight.highlight_around_current_line - input_buffer - ) - ); - ignore (input_buffer#add_selection_clipboard (cb())); - let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"] in - self#electric_paren paren_highlight_tag; - ignore (input_buffer#connect#after#mark_set - ~callback:(fun it (m:Gtk.text_mark) -> - !set_location - (Printf.sprintf - "Line: %5d Char: %3d" (self#get_insert#line + 1) - (self#get_insert#line_offset + 1)); - match GtkText.Mark.get_name m with - | Some "insert" -> - input_buffer#remove_tag - ~start:input_buffer#start_iter - ~stop:input_buffer#end_iter - paren_highlight_tag; - | Some s -> - prerr_endline (s^" moved") - | None -> () ) - ); + ~callback:(fun () -> + last_modification_time <- Unix.time (); + let r = input_view#visible_rect in + let stop = + input_view#get_iter_at_location + ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r) + ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r) + in + input_buffer#remove_tag + Tags.Script.error + ~start:self#get_start_of_input + ~stop; + tag_on_insert input_buffer + ) + ); + ignore (input_buffer#add_selection_clipboard cb); + ignore (proof_buffer#add_selection_clipboard cb); + ignore (message_buffer#add_selection_clipboard cb); + self#electric_paren Tags.Script.paren; + ignore (input_buffer#connect#after#mark_set + ~callback:(fun it (m:Gtk.text_mark) -> + !set_location + (Printf.sprintf + "Line: %5d Char: %3d" (self#get_insert#line + 1) + (self#get_insert#line_offset + 1)); + match GtkText.Mark.get_name m with + | Some "insert" -> + input_buffer#remove_tag + ~start:input_buffer#start_iter + ~stop:input_buffer#end_iter + Tags.Script.paren; + | Some s -> + prerr_endline (s^" moved") + | None -> () ) + ); ignore (input_buffer#connect#insert_text - (fun it s -> - prerr_endline "Should recenter ?"; - if String.contains s '\n' then begin - prerr_endline "Should recenter : yes"; - self#recenter_insert - end)) + (fun it s -> + prerr_endline "Should recenter ?"; + if String.contains s '\n' then begin + prerr_endline "Should recenter : yes"; + self#recenter_insert + end)); end -let create_input_tab filename = - let b = GText.buffer () in - let _ = GMisc.label () in - let v_box = GPack.hbox ~homogeneous:false () in - let _ = GMisc.image ~packing:v_box#pack () in - let _ = GMisc.label ~text:filename ~packing:v_box#pack () in - let appendp x = ignore ((notebook ())#append_page - ~tab_label:v_box#coerce x) in - let fr1 = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:appendp () - in - let sw1 = GBin.scrolled_window - ~vpolicy:`AUTOMATIC - ~hpolicy:`AUTOMATIC - ~packing:fr1#add () - in - let tv1 = Undo.undoable_view ~buffer:b ~packing:(sw1#add) () in - prerr_endline ("Language: "^ b#start_iter#language); - tv1#misc#set_name "ScriptWindow"; - let _ = tv1#set_editable true in - let _ = tv1#set_wrap_mode `NONE in - b#place_cursor ~where:(b#start_iter); - ignore (tv1#event#connect#button_press ~callback: - (fun ev -> GdkEvent.Button.button ev = 3)); - (* ignore (tv1#event#connect#button_press ~callback: - (fun ev -> - if (GdkEvent.Button.button ev=2) then - (try - prerr_endline "Paste invoked"; - GtkSignal.emit_unit - (get_current_view()).view#as_view - GtkText.View.Signals.paste_clipboard; - true - with _ -> false) - else false - ));*) - tv1#misc#grab_focus (); - ignore (tv1#buffer#create_mark - ~name:"start_of_input" - tv1#buffer#start_iter); - ignore (tv1#buffer#create_tag - ~name:"kwd" - [`FOREGROUND "blue"]); - ignore (tv1#buffer#create_tag - ~name:"decl" - [`FOREGROUND "orange red"]); - ignore (tv1#buffer#create_tag - ~name:"comment" - [`FOREGROUND "brown"]); - ignore (tv1#buffer#create_tag - ~name:"reserved" - [`FOREGROUND "dark red"]); - ignore (tv1#buffer#create_tag - ~name:"error" - [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]); - ignore (tv1#buffer#create_tag - ~name:"to_process" - [`BACKGROUND "light blue" ;`EDITABLE false]); - ignore (tv1#buffer#create_tag - ~name:"processed" - [`BACKGROUND "light green" ;`EDITABLE false]); - ignore (tv1#buffer#create_tag (* Proof mode *) - ~name:"unjustified" - [`UNDERLINE `SINGLE ; `FOREGROUND "red"; - `BACKGROUND "gold" ;`EDITABLE false]); - ignore (tv1#buffer#create_tag - ~name:"found" - [`BACKGROUND "blue"; `FOREGROUND "white"]); - tv1 - - let last_make = ref "";; let last_make_index = ref 0;; let search_compile_error_regexp = @@ -1823,20 +1457,228 @@ let search_next_error () = and b = int_of_string (Str.matched_group 3 !last_make) and e = int_of_string (Str.matched_group 4 !last_make) and msg_index = Str.match_beginning () - in - last_make_index := Str.group_end 4; + in + last_make_index := Str.group_end 4; (f,l,b,e, String.sub !last_make msg_index (String.length !last_make - msg_index)) -let main files = + + +(**********************************************************************) +(* session creation and primitive handling *) +(**********************************************************************) + +let create_session () = + let script = + Undo.undoable_view + ~buffer:(GText.buffer ~tag_table:Tags.Script.table ()) + ~wrap_mode:`NONE () in + let proof = + GText.view + ~buffer:(GText.buffer ~tag_table:Tags.Proof.table ()) + ~editable:false ~wrap_mode:`CHAR () in + let message = + GText.view + ~buffer:(GText.buffer ~tag_table:Tags.Message.table ()) + ~editable:false ~wrap_mode:`WORD () in + let basename = + GMisc.label ~text:"*scratch*" () in + let stack = + Stack.create () in + let legacy_av = + new analyzed_view script proof message stack in + let _ = + script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in + let _ = + proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in + let _ = + GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in + let _ = + proof#event#connect#motion_notify ~callback: + (fun e -> + let win = match proof#get_window `WIDGET with + | None -> assert false + | Some w -> w in + let x,y = Gdk.Window.get_pointer_location win in + let b_x,b_y = proof#window_to_buffer_coords ~tag:`WIDGET ~x ~y in + let it = proof#get_iter_at_location ~x:b_x ~y:b_y in + let tags = it#tags in + List.iter + (fun t -> + ignore (GtkText.Tag.event t#as_tag proof#as_widget e it#as_iter)) + tags; + false) in + script#misc#set_name "ScriptWindow"; + script#buffer#place_cursor ~where:(script#buffer#start_iter); + proof#misc#set_can_focus true; + message#misc#set_can_focus true; + script#misc#modify_font !current.text_font; + proof#misc#modify_font !current.text_font; + message#misc#modify_font !current.text_font; + { tab_label=basename; + filename=""; + script=script; + proof_view=proof; + message_view=message; + analyzed_view=legacy_av; + command_stack=stack; + encoding="" + } + +(* XXX - to be used later +let load_session session filename encs = + session.encoding <- List.find (IdeIO.load filename session.script#buffer) encs; + session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename)); + session.filename <- filename; + session.script#buffer#set_modified false + + +let save_session session filename encs = + session.encoding <- List.find (IdeIO.save session.script#buffer filename) encs; + session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename)); + session.filename <- filename; + session.script#buffer#set_modified false + + +let init_session session = + session.script#buffer#set_modified false; + session.script#clear_undo; + session.script#buffer#place_cursor session.script#buffer#start_iter + *) + + + + +(*********************************************************************) +(* functions called by the user interface *) +(*********************************************************************) +(* XXX - to be used later +let do_open session filename = + try + load_session session filename ["UTF-8";"ISO-8859-1";"ISO-8859-15"]; + init_session session; + ignore (session_notebook#append_term session) + with _ -> () + + +let do_save session = + try + if session.script#buffer#modified then + save_session session session.filename [session.encoding] + with _ -> () + + +let choose_open = + let last_filename = ref "" in fun session -> + let open_dialog = GWindow.file_chooser_dialog ~action:`OPEN ~title:"Open file" ~modal:true () in + let enc_frame = GBin.frame ~label:"File encoding" ~packing:(open_dialog#vbox#pack ~fill:false) () in + let enc_entry = GEdit.entry ~text:(String.concat " " ["UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in + let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok + ~message:"Invalid encoding, please indicate the encoding to use." () in + let open_response = function + | `OPEN -> begin + match open_dialog#filename with + | Some fn -> begin + try + load_session session fn (Util.split_string_at ' ' enc_entry#text); + session.analyzed_view <- Some (new analyzed_view session); + init_session session; + session_notebook#goto_page (session_notebook#append_term session); + last_filename := fn + with + | Not_found -> open_dialog#misc#hide (); error_dialog#show () + | _ -> + error_dialog#set_markup "Unknown error while loading file, aborting."; + open_dialog#destroy (); error_dialog#destroy () + end + | None -> () + end + | `DELETE_EVENT -> open_dialog#destroy (); error_dialog#destroy () + in + let _ = open_dialog#connect#response open_response in + let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); open_dialog#show ()) in + let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in + let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in + open_dialog#add_select_button_stock `OPEN `OPEN; + open_dialog#add_button_stock `CANCEL `DELETE_EVENT; + open_dialog#add_filter filter_any; + open_dialog#add_filter filter_coq; + ignore(open_dialog#set_filename !last_filename); + open_dialog#show () + + +let choose_save session = + let save_dialog = GWindow.file_chooser_dialog ~action:`SAVE ~title:"Save file" ~modal:true () in + let enc_frame = GBin.frame ~label:"File encoding" ~packing:(save_dialog#vbox#pack ~fill:false) () in + let enc_entry = GEdit.entry ~text:(String.concat " " [session.encoding;"UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in + let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok + ~message:"Invalid encoding, please indicate the encoding to use." () in + let save_response = function + | `SAVE -> begin + match save_dialog#filename with + | Some fn -> begin + try + save_session session fn (Util.split_string_at ' ' enc_entry#text) + with + | Not_found -> save_dialog#misc#hide (); error_dialog#show () + | _ -> + error_dialog#set_markup "Unknown error while saving file, aborting."; + save_dialog#destroy (); error_dialog#destroy () + end + | None -> () + end + | `DELETE_EVENT -> save_dialog#destroy (); error_dialog#destroy () + in + let _ = save_dialog#connect#response save_response in + let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); save_dialog#show ()) in + let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in + let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in + save_dialog#add_select_button_stock `SAVE `SAVE; + save_dialog#add_button_stock `CANCEL `DELETE_EVENT; + save_dialog#add_filter filter_any; + save_dialog#add_filter filter_coq; + ignore(save_dialog#set_filename session.filename); + save_dialog#show () + *) + +let do_print session = + let av = session.analyzed_view in + if session.filename = "" + then flash_info "Cannot print: this buffer has no name" + else begin + let cmd = + "cd " ^ Filename.quote (Filename.dirname session.filename) ^ "; " ^ + !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename session.filename) ^ + " | " ^ !current.cmd_print + in + let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () in + let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in + let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in + let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in + let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in + let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in + let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in + let callback_print () = + let cmd = print_entry#text in + let s,_ = run_command av#insert_message cmd in + flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed"); + print_window#destroy () + in + ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ; + ignore (print_button#connect#clicked ~callback:callback_print); + print_window#misc#show () + end + + +let main files = (* Statup preferences *) load_pref (); (* Main window *) - let w = GWindow.window + let w = GWindow.window ~wm_class:"CoqIde" ~wm_name:"CoqIde" - ~allow_grow:true ~allow_shrink:true - ~width:!current.window_width ~height:!current.window_height + ~allow_grow:true ~allow_shrink:true + ~width:!current.window_width ~height:!current.window_height ~title:"CoqIde" () in (try @@ -1852,15 +1694,15 @@ let main files = let menubar = GMenu.menu_bar ~packing:vbox#pack () in (* Toolbar *) - let toolbar = GButton.toolbar - ~orientation:`HORIZONTAL + let toolbar = GButton.toolbar + ~orientation:`HORIZONTAL ~style:`ICONS - ~tooltips:true + ~tooltips:true ~packing:(* handle#add *) (vbox#pack ~expand:false ~fill:false) () in - show_toolbar := + show_toolbar := (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ()); let factory = new GMenu.factory ~accel_path:"/" menubar in @@ -1873,17 +1715,20 @@ let main files = (* File/Load Menu *) let load_file handler f = - let f = absolute_filename f in + let f = absolute_filename f in try prerr_endline "Loading file starts"; - Vector.find_or_fail - (function - | {analyzed_view=Some av} -> - (match av#filename with - | None -> false - | Some fn -> same_file f fn) - | _ -> false) - !input_views; + if not (Util.list_fold_left_i + (fun i found x -> if found then found else + let {analyzed_view=av} = x in + (match av#filename with + | None -> false + | Some fn -> + if same_file f fn + then (session_notebook#goto_page i; true) + else false)) + 0 false session_notebook#pages) + then begin prerr_endline "Loading: must open"; let b = Buffer.create 1024 in prerr_endline "Loading: get raw content"; @@ -1891,290 +1736,231 @@ let main files = 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; + let session = create_session () in + session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename f)); 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; + let index = session_notebook#append_term session in + let av = session.analyzed_view in prerr_endline "Loading: set filename"; av#set_filename (Some f); prerr_endline "Loading: stats"; av#update_stats; - let input_buffer = view#buffer in + let input_buffer = session.script#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; - set_tab_image index ~icon:`YES; + session_notebook#goto_page index; prerr_endline "Loading: highlight"; - Highlight.highlight_all input_buffer; input_buffer#set_modified false; prerr_endline "Loading: clear undo"; - av#view#clear_undo; + session.script#clear_undo; prerr_endline "Loading: success" - with - | Vector.Found i -> set_current_view i + end + with | e -> handler ("Load failed: "^(Printexc.to_string e)) in - let load f = load_file !flash_info f in - let load_m = file_factory#add_item "_New" + let load f = load_file flash_info f in + let load_m = file_factory#add_item "_New" ~key:GdkKeysyms._N in - let load_f () = - match select_file_for_save ~title:"Create file" () with + let load_f () = + match select_file_for_save ~title:"Create file" () with | None -> () | Some f -> load f in ignore (load_m#connect#activate (load_f)); - let load_m = file_factory#add_item "_Open" + let load_m = file_factory#add_item "_Open" ~key:GdkKeysyms._O in - let load_f () = - match select_file_for_open ~title:"Load file" () with + let load_f () = + match select_file_for_open ~title:"Load file" () with | None -> () | Some f -> load f in ignore (load_m#connect#activate (load_f)); (* File/Save Menu *) - let save_m = file_factory#add_item "_Save" + let save_m = file_factory#add_item "_Save" ~key:GdkKeysyms._S in - - - let save_f () = - let current = get_current_view () in + let save_f () = + let current = session_notebook#current_term in try - (match (Option.get current.analyzed_view)#filename with + (match current.analyzed_view#filename with | None -> begin match select_file_for_save ~title:"Save file" () with | None -> () - | Some f -> - if (Option.get current.analyzed_view)#save_as f then begin - set_current_tab_label (Filename.basename f); - !flash_info ("File " ^ f ^ " saved") + | Some f -> + if current.analyzed_view#save_as f then begin + current.tab_label#set_text (Filename.basename f); + flash_info ("File " ^ f ^ " saved") end else warning ("Save Failed (check if " ^ f ^ " is writable)") end - | Some f -> - if (Option.get current.analyzed_view)#save f then - !flash_info ("File " ^ f ^ " saved") + | Some f -> + if current.analyzed_view#save f then + flash_info ("File " ^ f ^ " saved") else warning ("Save Failed (check if " ^ f ^ " is writable)") - + ) - with + with | e -> warning "Save: unexpected error" - in + in ignore (save_m#connect#activate save_f); (* File/Save As Menu *) - let saveas_m = file_factory#add_item "S_ave as" + let saveas_m = file_factory#add_item "S_ave as" in - let saveas_f () = - let current = get_current_view () in - try (match (Option.get current.analyzed_view)#filename with - | None -> + let saveas_f () = + let current = session_notebook#current_term in + try (match current.analyzed_view#filename with + | None -> begin match select_file_for_save ~title:"Save file as" () with | None -> () - | Some f -> - if (Option.get current.analyzed_view)#save_as f then begin - set_current_tab_label (Filename.basename f); - !flash_info "Saved" + | Some f -> + if current.analyzed_view#save_as f then begin + current.tab_label#set_text (Filename.basename f); + flash_info "Saved" end - else !flash_info "Save Failed" + else flash_info "Save Failed" end - | Some f -> - begin match select_file_for_save - ~dir:(ref (Filename.dirname f)) + | Some f -> + begin match select_file_for_save + ~dir:(ref (Filename.dirname f)) ~filename:(Filename.basename f) ~title:"Save file as" () with | None -> () - | Some f -> - if (Option.get current.analyzed_view)#save_as f then begin - set_current_tab_label (Filename.basename f); - !flash_info "Saved" - end else !flash_info "Save Failed" + | Some f -> + if current.analyzed_view#save_as f then begin + current.tab_label#set_text (Filename.basename f); + flash_info "Saved" + end else flash_info "Save Failed" end); - with e -> !flash_info "Save Failed" - in + with e -> flash_info "Save Failed" + in ignore (saveas_m#connect#activate saveas_f); - + (* XXX *) (* File/Save All Menu *) let saveall_m = file_factory#add_item "Sa_ve all" in - let saveall_f () = - Vector.iter - (function - | {view = view ; analyzed_view = Some av} -> - begin match av#filename with + let saveall_f () = + List.iter + (function + | {script = view ; analyzed_view = av} -> + begin match av#filename with | None -> () | Some f -> ignore (av#save f) end - | _ -> () - ) input_views + ) session_notebook#pages in - let has_something_to_save () = - Vector.exists - (function - | {view=view} -> view#buffer#modified + (* XXX *) + let has_something_to_save () = + List.exists + (function + | {script=view} -> view#buffer#modified ) - input_views + session_notebook#pages in ignore (saveall_m#connect#activate saveall_f); - + (* XXX *) (* File/Revert Menu *) let revert_m = file_factory#add_item "_Revert all buffers" in - let revert_f () = - Vector.iter - (function - {view = view ; analyzed_view = Some av} -> - (try - match av#filename,av#stats with - | Some f,Some stats -> + let revert_f () = + List.iter + (function + {analyzed_view = av} -> + (try + match av#filename,av#stats with + | Some f,Some stats -> let new_stats = Unix.stat f in - if new_stats.Unix.st_mtime > stats.Unix.st_mtime + if new_stats.Unix.st_mtime > stats.Unix.st_mtime then av#revert | Some _, None -> av#revert | _ -> () with _ -> av#revert) - | _ -> () - ) input_views + ) session_notebook#pages in ignore (revert_m#connect#activate revert_f); - + (* File/Close Menu *) let close_m = file_factory#add_item "_Close buffer" ~key:GdkKeysyms._W in - let close_f () = - let v = Option.get !active_view in - let act = get_current_view_page () in - if v = act then !flash_info "Cannot close an active view" + let close_f () = + let v = !active_view in + let act = session_notebook#current_page in + if v = act then flash_info "Cannot close an active view" else remove_current_view_page () in ignore (close_m#connect#activate close_f); - + (* File/Print Menu *) - let print_f () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in - match av#filename with - | None -> - !flash_info "Cannot print: this buffer has no name" - | Some f -> - let cmd = - "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ - !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f) ^ - " | " ^ !current.cmd_print - in - let print_window = GWindow.window - ~title:"Print" - ~modal:true - ~position:`CENTER - ~wm_class:"CodIDE" - ~wm_name: "CodIDE" () in - let vbox_print = GPack.vbox - ~spacing:10 - ~border_width:10 - ~packing:print_window#add () in - let _ = GMisc.label - ~justify:`LEFT - ~text:"Print using the following command:" - ~packing:vbox_print#add () in - let print_entry = GEdit.entry - ~text:cmd - ~editable:true - ~width_chars:80 - ~packing:vbox_print#add () in - let hbox_print = GPack.hbox - ~spacing:10 - ~packing:vbox_print#add () in - let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in - let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in - let callback_print () = - let cmd = print_entry#text in - let s,_ = run_command av#insert_message cmd in - !flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed"); - print_window#destroy () - in - ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ; - ignore (print_button#connect#clicked ~callback:callback_print); - print_window#misc#show(); - in let _ = file_factory#add_item "_Print..." ~key:GdkKeysyms._P - ~callback:print_f in + ~callback:(fun () -> do_print session_notebook#current_term) in (* File/Export to Menu *) let export_f kind () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in match av#filename with - | None -> - !flash_info "Cannot print: this buffer has no name" + | None -> + flash_info "Cannot print: this buffer has no name" | Some f -> let basef = Filename.basename f in - let output = + let output = let basef_we = try Filename.chop_extension basef with _ -> basef in match kind with | "latex" -> basef_we ^ ".tex" | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind | _ -> assert false in - let cmd = + let cmd = "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef) in let s,_ = run_command av#insert_message cmd in - !flash_info (cmd ^ - if s = Unix.WEXITED 0 - then " succeeded" + flash_info (cmd ^ + if s = Unix.WEXITED 0 + then " succeeded" else " failed") in let file_export_m = file_factory#add_submenu "E_xport to" in let file_export_factory = new GMenu.factory ~accel_path:"/Export/" file_export_m ~accel_group in - let _ = - file_export_factory#add_item "_Html" ~callback:(export_f "html") + let _ = + file_export_factory#add_item "_Html" ~callback:(export_f "html") in - let _ = + let _ = file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex") in - let _ = - file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") + let _ = + file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi") in - let _ = - file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf") + let _ = + file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf") in - let _ = - file_export_factory#add_item "_Ps" ~callback:(export_f "ps") + let _ = + file_export_factory#add_item "_Ps" ~callback:(export_f "ps") in (* File/Rehighlight Menu *) let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in - ignore (rehighlight_m#connect#activate - (fun () -> - Highlight.highlight_all - (get_current_view()).view#buffer; - (Option.get (get_current_view()).analyzed_view)#recenter_insert)); + ignore (rehighlight_m#connect#activate + (fun () -> + force_retag + session_notebook#current_term.script#buffer; + session_notebook#current_term.analyzed_view#recenter_insert)); (* File/Quit Menu *) let quit_f () = save_pref(); - if has_something_to_save () then + if has_something_to_save () then match (GToolbox.question_box ~title:"Quit" ~buttons:["Save Named Buffers and Quit"; "Quit without Saving"; - "Don't Quit"] + "Don't Quit"] ~default:0 ~icon: (let img = GMisc.image () in @@ -2188,7 +1974,7 @@ let main files = | _ -> () else exit 0 in - let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q + let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q ~callback:quit_f in ignore (w#event#connect#delete (fun _ -> quit_f (); true)); @@ -2198,50 +1984,60 @@ let main files = let edit_f = new GMenu.factory ~accel_path:"/Edit/" edit_menu ~accel_group in ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback: (do_if_not_computing "undo" - (fun () -> - ignore ((Option.get ((get_current_view()).analyzed_view))# - without_auto_complete - (fun () -> (get_current_view()).view#undo) ())))); - ignore(edit_f#add_item "_Clear Undo Stack" + (fun () -> + ignore (session_notebook#current_term.analyzed_view# + without_auto_complete + (fun () -> session_notebook#current_term.script#undo) ())))); + ignore(edit_f#add_item "_Clear Undo Stack" (* ~key:GdkKeysyms._exclam *) ~callback: - (fun () -> - ignore (get_current_view()).view#clear_undo)); + (fun () -> + ignore session_notebook#current_term.script#clear_undo)); ignore(edit_f#add_separator ()); + let get_active_view_for_cp () = + let has_sel (i0,i1) = i0#compare i1 <> 0 in + let current = session_notebook#current_term in + if has_sel current.script#buffer#selection_bounds + then current.script#as_view + else if has_sel current.proof_view#buffer#selection_bounds + then current.proof_view#as_view + else current.message_view#as_view + in ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback: (fun () -> GtkSignal.emit_unit - (get_current_view()).view#as_view - GtkText.View.S.cut_clipboard)); + (get_active_view_for_cp ()) + 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 + (get_active_view_for_cp ()) GtkText.View.S.copy_clipboard)); ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback: - (fun () -> + (fun () -> try GtkSignal.emit_unit - (get_current_view()).view#as_view + session_notebook#current_term.script#as_view GtkText.View.S.paste_clipboard with _ -> prerr_endline "EMIT PASTE FAILED")); ignore (edit_f#add_separator ()); (* - let toggle_auto_complete_i = - edit_f#add_check_item "_Auto Completion" + let toggle_auto_complete_i = + edit_f#add_check_item "_Auto Completion" ~active:!current.auto_complete ~callback: in *) (* - auto_complete := - (fun b -> match (get_current_view()).analyzed_view with + auto_complete := + (fun b -> match session_notebook#current_term.analyzed_view with | Some av -> av#set_auto_complete b | None -> ()); *) let last_found = ref None in let search_backward = ref false in - let find_w = GWindow.window + let find_w = GWindow.window (* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *) (* ~allow_grow:true ~allow_shrink:true *) (* ~width:!current.window_width ~height:!current.window_height *) @@ -2252,38 +2048,38 @@ let main files = ~columns:3 ~rows:5 ~col_spacings:10 ~row_spacings:10 ~border_width:10 ~homogeneous:false ~packing:find_w#add () in - - let _ = + + let _ = GMisc.label ~text:"Find:" ~xalign:1.0 - ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) () + ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) () in let find_entry = GEdit.entry ~editable: true ~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X) () in - let _ = + let _ = GMisc.label ~text:"Replace with:" ~xalign:1.0 - ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) () + ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) () in let replace_entry = GEdit.entry ~editable: true ~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X) () in - (* let _ = + (* let _ = GButton.check_button ~label:"case sensitive" ~active:true ~packing: (find_box#attach ~left:1 ~top:2) () - + in *) (* - let find_backwards_check = + let find_backwards_check = GButton.check_button ~label:"search backwards" ~active:false @@ -2322,25 +2118,25 @@ let main files = () in let last_find () = - let v = (get_current_view()).view in + let v = session_notebook#current_term.script in let b = v#buffer in let start,stop = - match !last_found with + match !last_found with | None -> let i = b#get_iter_at_mark `INSERT in (i,i) | Some(start,stop) -> let start = b#get_iter_at_mark start and stop = b#get_iter_at_mark stop in - b#remove_tag_by_name ~start ~stop "found"; + b#remove_tag Tags.Script.found ~start ~stop; last_found:=None; start,stop in (v,b,start,stop) in let do_replace () = - let v = (get_current_view()).view in + let v = session_notebook#current_term.script in let b = v#buffer in - match !last_found with + match !last_found with | None -> () | Some(start,stop) -> let start = b#get_iter_at_mark start @@ -2358,7 +2154,7 @@ let main files = with | None -> () | Some(start,stop) -> - b#apply_tag_by_name "found" ~start ~stop; + b#apply_tag Tags.Script.found ~start ~stop; let start = `MARK (b#create_mark start) and stop = `MARK (b#create_mark stop) in @@ -2368,7 +2164,7 @@ let main files = in let do_find () = let (v,b,starti,_) = last_find () in - find_from v b starti find_entry#text + find_from v b starti find_entry#text in let do_replace_find () = do_replace(); @@ -2380,8 +2176,8 @@ let main files = find_w#misc#hide(); v#coerce#misc#grab_focus() in - to_do_on_page_switch := - (fun i -> if find_w#misc#visible then close_find()):: + to_do_on_page_switch := + (fun i -> if find_w#misc#visible then close_find()):: !to_do_on_page_switch; let find_again_forward () = search_backward := false; @@ -2403,12 +2199,12 @@ let main files = find_w#misc#hide(); v#coerce#misc#grab_focus(); true - end + end else if k = GdkKeysyms._Return then begin close_find(); true - end + end else if List.mem `CONTROL s && k = GdkKeysyms._f then begin find_again_forward (); @@ -2421,7 +2217,7 @@ let main files = end else false (* to let default callback execute *) in - let find_f ~backward () = + let find_f ~backward () = search_backward := backward; find_w#show (); find_w#present (); @@ -2455,30 +2251,30 @@ let main files = let complete_i = edit_f#add_item "_Complete" ~key:GdkKeysyms._comma ~callback: - (do_if_not_computing - (fun b -> - let v = Option.get (get_current_view ()).analyzed_view - - in v#complete_at_offset + (do_if_not_computing + (fun b -> + let v = session_notebook#current_term.analyzed_view + + in v#complete_at_offset ((v#view#buffer#get_iter `SEL_BOUND)#offset) )) in complete_i#misc#set_state `INSENSITIVE; *) - + ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback: - (fun () -> + (fun () -> ignore ( - let av = Option.get ((get_current_view()).analyzed_view) in + let av = session_notebook#current_term.analyzed_view in av#complete_at_offset (av#get_insert)#offset ))); ignore(edit_f#add_separator ()); (* external editor *) - let _ = + let _ = edit_f#add_item "External editor" ~callback: - (fun () -> - let av = Option.get ((get_current_view()).analyzed_view) in + (fun () -> + let av = session_notebook#current_term.analyzed_view in match av#filename with | None -> warning "Call to external editor available only on named files" | Some f -> @@ -2491,34 +2287,33 @@ let main files = (* Preferences *) let reset_revert_timer () = disconnect_revert_timer (); - if !current.global_auto_revert then + if !current.global_auto_revert then revert_timer := Some - (GMain.Timeout.add ~ms:!current.global_auto_revert_delay + (GMain.Timeout.add ~ms:!current.global_auto_revert_delay ~callback: - (fun () -> + (fun () -> do_if_not_computing "revert" (sync revert_f) (); true)) in reset_revert_timer (); (* to enable statup preferences timer *) - - let auto_save_f () = - Vector.iter - (function - {view = view ; analyzed_view = Some av} -> - (try + (* XXX *) + let auto_save_f () = + List.iter + (function + {script = view ; analyzed_view = av} -> + (try av#auto_save with _ -> ()) - | _ -> () - ) - input_views + ) + session_notebook#pages in let reset_auto_save_timer () = disconnect_auto_save_timer (); - if !current.auto_save then + if !current.auto_save then auto_save_timer := Some - (GMain.Timeout.add ~ms:!current.auto_save_delay + (GMain.Timeout.add ~ms:!current.auto_save_delay ~callback: - (fun () -> + (fun () -> do_if_not_computing "autosave" (sync auto_save_f) (); true)) in reset_auto_save_timer (); (* to enable statup preferences timer *) @@ -2536,34 +2331,40 @@ let main files = *) (* Navigation Menu *) let navigation_menu = factory#add_submenu "_Navigation" in - let navigation_factory = - new GMenu.factory navigation_menu + let navigation_factory = + new GMenu.factory navigation_menu ~accel_path:"/Navigation/" - ~accel_group - ~accel_modi:!current.modifier_for_navigation + ~accel_group + ~accel_modi:!current.modifier_for_navigation in - let do_or_activate f () = - let current = get_current_view () in - let analyzed_view = Option.get current.analyzed_view in - if analyzed_view#is_active then + let _do_or_activate f () = + let current = session_notebook#current_term in + let analyzed_view = current.analyzed_view in + if analyzed_view#is_active then begin + prerr_endline ("view "^current.tab_label#text^"already active"); ignore (f analyzed_view) - else + end else begin - !flash_info "New proof started"; - activate_input (notebook ())#current_page; + flash_info "New proof started"; + prerr_endline ("activating view "^current.tab_label#text); + activate_input session_notebook#current_page; ignore (f analyzed_view) end in - let do_or_activate f = + let do_or_activate f = do_if_not_computing "do_or_activate" - (do_or_activate - (fun av -> f av ; !pop_info();!push_info (Coq.current_status()))) + (_do_or_activate + (fun av -> f av; + pop_info (); + push_info (Coq.current_status()) + ) + ) in - let add_to_menu_toolbar text ~tooltip ?key ~callback icon = + let add_to_menu_toolbar text ~tooltip ?key ~callback icon = begin - match key with None -> () + match key with None -> () | Some key -> ignore (navigation_factory#add_item text ~key ~callback) end; ignore (toolbar#insert_button @@ -2573,107 +2374,106 @@ let main files = ~callback ()) in - add_to_menu_toolbar - "_Save" - ~tooltip:"Save current buffer" + add_to_menu_toolbar + "_Save" + ~tooltip:"Save current buffer" ~callback:save_f `SAVE; - add_to_menu_toolbar - "_Close" - ~tooltip:"Close current buffer" + add_to_menu_toolbar + "_Close" + ~tooltip:"Close current buffer" ~callback:close_f `CLOSE; - add_to_menu_toolbar - "_Forward" - ~tooltip:"Forward one command" - ~key:GdkKeysyms._Down - ~callback:(do_or_activate (fun a -> a#process_next_phrase true true true)) + add_to_menu_toolbar + "_Forward" + ~tooltip:"Forward one command" + ~key:GdkKeysyms._Down + ~callback:(do_or_activate (fun a -> a#process_next_phrase true true true )) + `GO_DOWN; add_to_menu_toolbar "_Backward" - ~tooltip:"Backward one command" + ~tooltip:"Backward one command" ~key:GdkKeysyms._Up ~callback:(do_or_activate (fun a -> a#undo_last_step)) `GO_UP; - add_to_menu_toolbar - "_Go to" - ~tooltip:"Go to cursor" + add_to_menu_toolbar + "_Go to" + ~tooltip:"Go to cursor" ~key:GdkKeysyms._Right ~callback:(do_or_activate (fun a-> a#go_to_insert)) `JUMP_TO; - add_to_menu_toolbar - "_Start" - ~tooltip:"Go to start" + add_to_menu_toolbar + "_Start" + ~tooltip:"Go to start" ~key:GdkKeysyms._Home ~callback:(do_or_activate (fun a -> a#reset_initial)) `GOTO_TOP; - add_to_menu_toolbar - "_End" - ~tooltip:"Go to end" + add_to_menu_toolbar + "_End" + ~tooltip:"Go to end" ~key:GdkKeysyms._End ~callback:(do_or_activate (fun a -> a#process_until_end_or_error)) `GOTO_BOTTOM; add_to_menu_toolbar "_Interrupt" - ~tooltip:"Interrupt computations" - ~key:GdkKeysyms._Break + ~tooltip:"Interrupt computations" + ~key:GdkKeysyms._Break ~callback:break `STOP; + add_to_menu_toolbar "_Hide" + ~tooltip:"Hide proof" + ~key:GdkKeysyms._h + ~callback:(fun x -> + let sess = session_notebook#current_term in + toggle_proof_visibility sess.script#buffer + sess.analyzed_view#get_insert) + `MISSING_IMAGE; (* Tactics Menu *) let tactics_menu = factory#add_submenu "_Try Tactics" in - let tactics_factory = - new GMenu.factory tactics_menu + let tactics_factory = + new GMenu.factory tactics_menu ~accel_path:"/Tactics/" - ~accel_group + ~accel_group ~accel_modi:!current.modifier_for_tactics in - let do_if_active_raw f () = - let current = get_current_view () in - let analyzed_view = Option.get current.analyzed_view in + let do_if_active_raw f () = + let current = session_notebook#current_term in + let analyzed_view = current.analyzed_view in if analyzed_view#is_active then ignore (f analyzed_view) in let do_if_active f = do_if_not_computing "do_if_active" (do_if_active_raw f) in - (* - let blaster_i = - tactics_factory#add_item "_Blaster" - ~key:GdkKeysyms._b - ~callback: (do_if_active_raw (fun a -> a#blaster ())) - (* Custom locking mechanism! *) - in - blaster_i#misc#set_state `INSENSITIVE; - *) - - ignore (tactics_factory#add_item "_auto" + ignore (tactics_factory#add_item "_auto" ~key:GdkKeysyms._a ~callback:(do_if_active (fun a -> a#insert_command "progress auto.\n" "auto.\n")) ); ignore (tactics_factory#add_item "_auto with *" ~key:GdkKeysyms._asterisk - ~callback:(do_if_active (fun a -> a#insert_command + ~callback:(do_if_active (fun a -> a#insert_command "progress auto with *.\n" "auto with *.\n"))); ignore (tactics_factory#add_item "_eauto" ~key:GdkKeysyms._e - ~callback:(do_if_active (fun a -> a#insert_command + ~callback:(do_if_active (fun a -> a#insert_command "progress eauto.\n" "eauto.\n")) ); ignore (tactics_factory#add_item "_eauto with *" ~key:GdkKeysyms._ampersand - ~callback:(do_if_active (fun a -> a#insert_command - "progress eauto with *.\n" + ~callback:(do_if_active (fun a -> a#insert_command + "progress eauto with *.\n" "eauto with *.\n")) ); ignore (tactics_factory#add_item "_intuition" ~key:GdkKeysyms._i - ~callback:(do_if_active (fun a -> a#insert_command - "progress intuition.\n" + ~callback:(do_if_active (fun a -> a#insert_command + "progress intuition.\n" "intuition.\n")) ); ignore (tactics_factory#add_item "_omega" ~key:GdkKeysyms._o - ~callback:(do_if_active (fun a -> a#insert_command + ~callback:(do_if_active (fun a -> a#insert_command "omega.\n" "omega.\n")) ); ignore (tactics_factory#add_item "_simpl" @@ -2703,15 +2503,15 @@ let main files = ignore (tactics_factory#add_item "" ~key:GdkKeysyms._dollar - ~callback:(do_if_active (fun a -> a#tactic_wizard + ~callback:(do_if_active (fun a -> a#tactic_wizard !current.automatic_tactics )) ); - + ignore (tactics_factory#add_separator ()); - let add_simple_template (factory: GMenu.menu GMenu.factory) + let add_simple_template (factory: GMenu.menu GMenu.factory) (menu_text, text) = - let text = + let text = let l = String.length text - 1 in if String.get text l = '.' then text ^"\n" @@ -2719,42 +2519,42 @@ let main files = in ignore (factory#add_item menu_text ~callback: - (fun () -> let {view = view } = get_current_view () in + (fun () -> let {script = view } = session_notebook#current_term in ignore (view#buffer#insert_interactive text))) in - List.iter - (fun l -> - match l with + List.iter + (fun l -> + match l with | [] -> () - | [s] -> add_simple_template tactics_factory ("_"^s, s) - | s::_ -> + | [s] -> add_simple_template tactics_factory ("_"^s, s) + | s::_ -> let a = "_@..." in a.[1] <- s.[0]; - let f = tactics_factory#add_submenu a in + let f = tactics_factory#add_submenu a in let ff = new GMenu.factory f ~accel_group in - List.iter - (fun x -> + List.iter + (fun x -> add_simple_template - ff + ff ((String.sub x 0 1)^ "_"^ (String.sub x 1 (String.length x - 1)), x)) l - ) + ) Coq_commands.tactics; - + (* Templates Menu *) let templates_menu = factory#add_submenu "Te_mplates" in - let templates_factory = new GMenu.factory templates_menu + let templates_factory = new GMenu.factory templates_menu ~accel_path:"/Templates/" - ~accel_group + ~accel_group ~accel_modi:!current.modifier_for_templates in let add_complex_template (menu_text, text, offset, len, key) = (* Templates/Lemma *) let callback () = - let {view = view } = get_current_view () in + let {script = view } = session_notebook#current_term in if view#buffer#insert_interactive text then begin let iter = view#buffer#get_iter_at_mark `INSERT in ignore (iter#nocopy#backward_chars offset); @@ -2764,19 +2564,19 @@ let main files = end in ignore (templates_factory#add_item menu_text ~callback ?key) in - add_complex_template - ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n", + add_complex_template + ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n", 19, 9, Some GdkKeysyms._L); - add_complex_template - ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n", + add_complex_template + ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n", 19, 11, Some GdkKeysyms._T); - add_complex_template + add_complex_template ("_Definition __", "Definition ident := .\n", 6, 5, Some GdkKeysyms._D); - add_complex_template + add_complex_template ("_Inductive __", "Inductive ident : :=\n | : .\n", 14, 5, Some GdkKeysyms._I); - add_complex_template + add_complex_template ("_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 29, 5, Some GdkKeysyms._F); add_complex_template("_Scheme __", @@ -2784,14 +2584,14 @@ let main files = with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Template for match *) - let callback () = + let callback () = let w = get_current_word () in - try + try let cases = Coq.make_cases w in let print c = function | [x] -> Format.fprintf c " | %s => _@\n" x - | x::l -> Format.fprintf c " | (%s%a) => _@\n" x + | x::l -> Format.fprintf c " | (%s%a) => _@\n" x (print_list (fun c s -> Format.fprintf c " %s" s)) l | [] -> assert false in @@ -2801,28 +2601,28 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (print_list print) cases; let s = Buffer.contents b in prerr_endline s; - let {view = view } = get_current_view () in + let {script = view } = session_notebook#current_term in ignore (view#buffer#delete_selection ()); - let m = view#buffer#create_mark + let m = view#buffer#create_mark (view#buffer#get_iter `INSERT) in - if view#buffer#insert_interactive s then + if view#buffer#insert_interactive s then let i = view#buffer#get_iter (`MARK m) in let _ = i#nocopy#forward_chars 9 in view#buffer#place_cursor i; view#buffer#move_mark ~where:(i#backward_chars 3) - `SEL_BOUND - with Not_found -> !flash_info "Not an inductive type" + `SEL_BOUND + with Not_found -> flash_info "Not an inductive type" in ignore (templates_factory#add_item "match ..." ~key:GdkKeysyms._C ~callback ); - + (* - let add_simple_template (factory: GMenu.menu GMenu.factory) + let add_simple_template (factory: GMenu.menu GMenu.factory) (menu_text, text) = - let text = + let text = let l = String.length text - 1 in if String.get text l = '.' then text ^"\n" @@ -2830,7 +2630,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in ignore (factory#add_item menu_text ~callback: - (fun () -> let {view = view } = get_current_view () in + (fun () -> let {view = view } = session_notebook#current_term in ignore (view#buffer#insert_interactive text))) in *) @@ -2849,92 +2649,100 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ]; ignore (templates_factory#add_separator ()); *) - List.iter - (fun l -> - match l with + List.iter + (fun l -> + match l with | [] -> () - | [s] -> add_simple_template templates_factory ("_"^s, s) - | s::_ -> + | [s] -> add_simple_template templates_factory ("_"^s, s) + | s::_ -> let a = "_@..." in a.[1] <- s.[0]; - let f = templates_factory#add_submenu a in + let f = templates_factory#add_submenu a in let ff = new GMenu.factory f ~accel_group in - List.iter - (fun x -> - add_simple_template - ff + List.iter + (fun x -> + add_simple_template + ff ((String.sub x 0 1)^ "_"^ (String.sub x 1 (String.length x - 1)), x)) l - ) + ) Coq_commands.commands; - + (* Queries Menu *) let queries_menu = factory#add_submenu "_Queries" in let queries_factory = new GMenu.factory queries_menu ~accel_group ~accel_path:"/Queries" ~accel_modi:[] in - + (* Command/Show commands *) - let _ = + let _ = queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"SearchAbout" - ~term + ~term ()) in - let _ = + let _ = queries_factory#add_item "_Check " ~key:GdkKeysyms._F3 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Check" - ~term + ~term ()) in - let _ = + let _ = queries_factory#add_item "_Print " ~key:GdkKeysyms._F4 ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Print" - ~term + ~term + ()) + in + let _ = + queries_factory#add_item "_About " ~key:GdkKeysyms._F5 + ~callback:(fun () -> let term = get_current_word () in + (Command_windows.command_window ())#new_command + ~command:"About" + ~term ()) in - let _ = - queries_factory#add_item "_Locate" + let _ = + queries_factory#add_item "_Locate" ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Locate" - ~term + ~term ()) in - let _ = - queries_factory#add_item "_Whelp Locate" + let _ = + queries_factory#add_item "_Whelp Locate" ~callback:(fun () -> let term = get_current_word () in (Command_windows.command_window ())#new_command ~command:"Whelp Locate" - ~term + ~term ()) in (* Display menu *) - + let display_menu = factory#add_submenu "_Display" in let view_factory = new GMenu.factory display_menu ~accel_path:"/Display/" - ~accel_group + ~accel_group ~accel_modi:!current.modifier_for_display in - let _ = ignore (view_factory#add_check_item - "Display _implicit arguments" + let _ = ignore (view_factory#add_check_item + "Display _implicit arguments" ~key:GdkKeysyms._i ~callback:(fun _ -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ())) in - let _ = ignore (view_factory#add_check_item + let _ = ignore (view_factory#add_check_item "Display _coercions" ~key:GdkKeysyms._c ~callback:(fun _ -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ())) in @@ -2944,104 +2752,77 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ~key:GdkKeysyms._m ~callback:(fun _ -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ())) in - let _ = ignore (view_factory#add_check_item + let _ = ignore (view_factory#add_check_item "Deactivate _notations display" ~key:GdkKeysyms._n ~callback:(fun _ -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ())) in - let _ = ignore (view_factory#add_check_item + let _ = ignore (view_factory#add_check_item "Display _all basic low-level contents" ~key:GdkKeysyms._a - ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in + ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in - let _ = ignore (view_factory#add_check_item + let _ = ignore (view_factory#add_check_item "Display _existential variable instances" ~key:GdkKeysyms._e ~callback:(fun _ -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ())) in - let _ = ignore (view_factory#add_check_item + let _ = ignore (view_factory#add_check_item "Display _universe levels" ~key:GdkKeysyms._u ~callback:(fun _ -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ())) in - let _ = ignore (view_factory#add_check_item + let _ = ignore (view_factory#add_check_item "Display all _low-level contents" ~key:GdkKeysyms._l - ~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) in + ~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) in + + - (* Unicode *) -(* - let unicode_menu = factory#add_submenu "_Unicode" in - let unicode_factory = new GMenu.factory unicode_menu - ~accel_path:"/Unicode/" - ~accel_group - ~accel_modi:[] - in - let logic_symbols_menu = unicode_factory#add_submenu "Math operators" in - let logic_factory = new GMenu.factory logic_symbols_menu - ~accel_path:"/Unicode/Math operators" - ~accel_group - ~accel_modi:[] - in - let new_unicode_item s = ignore ( - logic_factory#add_item s - ~callback:(fun () -> - let v = get_current_view () in - ignore (v.view#buffer#insert_interactive s))) - in - - for i = 0x2200 to 0x22FF do - List.iter new_unicode_item [Glib.Utf8.from_unichar i]; - - done; - -*) - - (* Externals *) let externals_menu = factory#add_submenu "_Compile" in - let externals_factory = new GMenu.factory externals_menu + let externals_factory = new GMenu.factory externals_menu ~accel_path:"/Compile/" - ~accel_group + ~accel_group ~accel_modi:[] in - + (* Command/Compile Menu *) let compile_f () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in save_f (); match av#filename with - | None -> - !flash_info "Active buffer has no name" + | None -> + flash_info "Active buffer has no name" | Some f -> - let cmd = !current.cmd_coqc ^ " -I " + let cmd = !current.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f)) ^ " " ^ (Filename.quote f) in let s,res = run_command av#insert_message cmd in if s = Unix.WEXITED 0 then - !flash_info (f ^ " successfully compiled") + flash_info (f ^ " successfully compiled") else begin - !flash_info (f ^ " failed to compile"); - activate_input (notebook ())#current_page; + flash_info (f ^ " failed to compile"); + activate_input session_notebook#current_page; av#process_until_end_or_error; av#insert_message "Compilation output:\n"; av#insert_message res end in - let _ = - externals_factory#add_item "_Compile Buffer" ~callback:compile_f + let _ = + externals_factory#add_item "_Compile Buffer" ~callback:compile_f in (* Command/Make Menu *) let make_f () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in match av#filename with - | None -> - !flash_info "Cannot make: this buffer has no name" + | None -> + flash_info "Cannot make: this buffer has no name" | Some f -> - let cmd = + let cmd = "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in (* @@ -3051,22 +2832,22 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let s,res = run_command av#insert_message cmd in last_make := res; last_make_index := 0; - !flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") + flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in - let _ = externals_factory#add_item "_Make" + let _ = externals_factory#add_item "_Make" ~key:GdkKeysyms._F6 - ~callback:make_f + ~callback:make_f in - + (* Compile/Next Error *) - let next_error () = + let next_error () = try let file,line,start,stop,error_msg = search_next_error () in - load file; - let v = get_current_view () in - let av = Option.get v.analyzed_view in - let input_buffer = v.view#buffer in + load file; + let v = session_notebook#current_term in + let av = v.analyzed_view in + let input_buffer = v.script#buffer in (* let init = input_buffer#start_iter in let i = init#forward_lines (line-1) in @@ -3082,215 +2863,143 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); *) let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in - input_buffer#apply_tag_by_name "error" + input_buffer#apply_tag Tags.Script.error ~start:starti ~stop:stopi; input_buffer#place_cursor starti; av#set_message error_msg; - v.view#misc#grab_focus () + v.script#misc#grab_focus () with Not_found -> last_make_index := 0; - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in av#set_message "No more errors.\n" in - let _ = - externals_factory#add_item "_Next error" + let _ = + externals_factory#add_item "_Next error" ~key:GdkKeysyms._F7 ~callback:next_error in - + (* Command/CoqMakefile Menu*) let coq_makefile_f () = - let v = get_current_view () in - let av = Option.get v.analyzed_view in + let v = session_notebook#current_term in + let av = v.analyzed_view in match av#filename with - | None -> - !flash_info "Cannot make makefile: this buffer has no name" + | None -> + flash_info "Cannot make makefile: this buffer has no name" | Some f -> - let cmd = + let cmd = "cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in let s,res = run_command av#insert_message cmd in - !flash_info + flash_info (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed") in - let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f + let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f in (* Windows Menu *) let configuration_menu = factory#add_submenu "_Windows" in - let configuration_factory = new GMenu.factory configuration_menu + let configuration_factory = new GMenu.factory configuration_menu ~accel_path:"/Windows" ~accel_modi:[] ~accel_group in let _ = - configuration_factory#add_item + configuration_factory#add_item "Show/Hide _Query Pane" ~key:GdkKeysyms._Escape - ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then + ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then (Command_windows.command_window ())#frame#misc#hide () else (Command_windows.command_window ())#frame#misc#show ()) - in - let _ = - configuration_factory#add_check_item - "Show/Hide _Toolbar" - ~callback:(fun _ -> - !current.show_toolbar <- not !current.show_toolbar; - !show_toolbar !current.show_toolbar) - in - let _ = configuration_factory#add_item - "Detach _Script Window" - ~callback: - (do_if_not_computing "detach script window" (sync - (fun () -> - let nb = notebook () in - if nb#misc#toplevel#get_oid=w#coerce#get_oid then - begin - let nw = GWindow.window - ~width:(!current.window_width*2/3) - ~height:(!current.window_height*2/3) - ~position:`CENTER - ~wm_name:"CoqIde" - ~wm_class:"CoqIde" - ~title:"Script" - ~show:true () in - let parent = Option.get nb#misc#parent in - ignore (nw#connect#destroy - ~callback: - (fun () -> nb#misc#reparent parent)); - nw#add_accel_group accel_group; - nb#misc#reparent nw#coerce - end - ))) in -(* let _ = configuration_factory#add_item - "Detach _Command Pane" - ~callback: - (do_if_not_computing "detach command pane" (sync - (fun () -> - let command_object = Command_windows.command_window() in - let queries_frame = command_object#frame in - if queries_frame#misc#toplevel#get_oid=w#coerce#get_oid then - begin - let nw = GWindow.window - ~width:(!current.window_width*2/3) - ~height:(!current.window_height*2/3) - ~wm_name:"CoqIde" - ~wm_class:"CoqIde" - ~position:`CENTER - ~title:"Queries" - ~show:true () in - let parent = Option.get queries_frame#misc#parent in - ignore (nw#connect#destroy - ~callback: - (fun () -> queries_frame#misc#reparent parent)); - queries_frame#misc#show(); - queries_frame#misc#reparent nw#coerce - end - ))) + let _ = + configuration_factory#add_check_item + "Show/Hide _Toolbar" + ~callback:(fun _ -> + !current.show_toolbar <- not !current.show_toolbar; + !show_toolbar !current.show_toolbar) in -*) - let _ = - configuration_factory#add_item + let _ = + configuration_factory#add_item "Detach _View" ~callback: (do_if_not_computing "detach view" - (fun () -> - match get_current_view () with - | {view=v;analyzed_view=Some av} -> - let w = GWindow.window ~show:true + (fun () -> + match session_notebook#current_term with + | {script=v;analyzed_view=av} -> + let w = GWindow.window ~show:true ~width:(!current.window_width*2/3) ~height:(!current.window_height*2/3) ~position:`CENTER ~title:(match av#filename with | None -> "*Unnamed*" - | Some f -> f) - () + | Some f -> f) + () in - let sb = GBin.scrolled_window - ~packing:w#add () + let sb = GBin.scrolled_window + ~packing:w#add () in - let nv = GText.view - ~buffer:v#buffer - ~packing:sb#add + let nv = GText.view + ~buffer:v#buffer + ~packing:sb#add () in - nv#misc#modify_font - !current.text_font; - ignore (w#connect#destroy + nv#misc#modify_font + !current.text_font; + ignore (w#connect#destroy ~callback: (fun () -> av#remove_detached_view w)); av#add_detached_view w - | _ -> () - + )) in (* Help Menu *) let help_menu = factory#add_submenu "_Help" in - let help_factory = new GMenu.factory help_menu + let help_factory = new GMenu.factory help_menu ~accel_path:"/Help/" ~accel_modi:[] ~accel_group in - let _ = help_factory#add_item "Browse Coq _Manual" + let _ = help_factory#add_item "Browse Coq _Manual" ~callback: - (fun () -> - let av = Option.get ((get_current_view ()).analyzed_view) in - browse av#insert_message (!current.doc_url)) in - let _ = help_factory#add_item "Browse Coq _Library" + (fun () -> + let av = session_notebook#current_term.analyzed_view in + browse av#insert_message (doc_url ())) in + let _ = help_factory#add_item "Browse Coq _Library" ~callback: - (fun () -> - let av = Option.get ((get_current_view ()).analyzed_view) in + (fun () -> + let av = session_notebook#current_term.analyzed_view in browse av#insert_message !current.library_url) in - let _ = + let _ = help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1 - ~callback:(fun () -> - let av = Option.get ((get_current_view ()).analyzed_view) in + ~callback:(fun () -> + let av = session_notebook#current_term.analyzed_view in av#help_for_keyword ()) in let _ = help_factory#add_separator () in - (* - let faq_m = help_factory#add_item "_FAQ" in - *) let about_m = help_factory#add_item "_About" in (* End of menu *) (* The vertical Separator between Scripts and Goals *) let queries_pane = GPack.paned `VERTICAL ~packing:(vbox#pack ~expand:true ) () in - let hb = GPack.paned `HORIZONTAL ~border_width:5 ~packing:(queries_pane#pack1 ~shrink:false ~resize:true) () in - let fr_notebook = GBin.frame ~shadow_type:`IN ~packing:hb#add1 () in - _notebook := Some (GPack.notebook ~border_width:2 ~show_border:false ~scrollable:true - ~packing:fr_notebook#add - ()); + queries_pane#pack1 ~shrink:false ~resize:true session_notebook#coerce; update_notebook_pos (); - let nb = notebook () in - let hb2 = GPack.paned `VERTICAL ~packing:hb#add2 () in - let fr_a = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in - let fr_b = GBin.frame ~shadow_type:`IN ~packing:hb2#add () in - let sw2 = GBin.scrolled_window - ~vpolicy:`AUTOMATIC - ~hpolicy:`AUTOMATIC - ~packing:(fr_a#add) () in - let sw3 = GBin.scrolled_window - ~vpolicy:`AUTOMATIC - ~hpolicy:`AUTOMATIC - ~packing:(fr_b#add) () in + let nb = session_notebook in let command_object = Command_windows.command_window() in let queries_frame = command_object#frame in queries_pane#pack2 ~shrink:false ~resize:false (queries_frame#coerce); let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in - let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) () - in + lower_hbox#pack ~expand:true status#coerce; let search_lbl = GMisc.label ~text:"Search:" ~show:false - ~packing:(lower_hbox#pack ~expand:false) () + ~packing:(lower_hbox#pack ~expand:false) () in let search_history = ref [] in let search_input = GEdit.combo ~popdown_strings:!search_history ~enable_arrow_keys:true ~show:false - ~packing:(lower_hbox#pack ~expand:false) () + ~packing:(lower_hbox#pack ~expand:false) () in search_input#disable_activate (); let ready_to_wrap_search = ref false in @@ -3301,108 +3010,99 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let search_forward = ref true in let matched_word = ref None in - let memo_search () = + let memo_search () = matched_word := Some search_input#entry#text - - (* if not (List.mem search_input#entry#text !search_history) then - (search_history := - search_input#entry#text::!search_history; - search_input#set_popdown_strings !search_history); - start_of_search := None; - ready_to_wrap_search := false - *) - in - let end_search () = + let end_search () = prerr_endline "End Search"; memo_search (); - let v = (get_current_view ()).view in + let v = session_notebook#current_term.script in v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT); v#coerce#misc#grab_focus (); search_input#entry#set_text ""; search_lbl#misc#hide (); search_input#misc#hide () in - let end_search_focus_out () = + let end_search_focus_out () = prerr_endline "End Search(focus out)"; memo_search (); - let v = (get_current_view ()).view in + let v = session_notebook#current_term.script in v#buffer#move_mark `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT); search_input#entry#set_text ""; search_lbl#misc#hide (); search_input#misc#hide () in ignore (search_input#entry#connect#activate ~callback:end_search); - ignore (search_input#entry#event#connect#key_press + ignore (search_input#entry#event#connect#key_press ~callback:(fun k -> let kv = GdkEvent.Key.keyval k in - if + if kv = GdkKeysyms._Right - || kv = GdkKeysyms._Up + || kv = GdkKeysyms._Up || kv = GdkKeysyms._Left - || (kv = GdkKeysyms._g + || (kv = GdkKeysyms._g && (List.mem `CONTROL (GdkEvent.Key.state k))) - then end_search (); + then end_search (); false)); ignore (search_input#entry#event#connect#focus_out ~callback:(fun _ -> end_search_focus_out (); false)); - to_do_on_page_switch := - (fun i -> + to_do_on_page_switch := + (fun i -> start_of_search := None; ready_to_wrap_search:=false)::!to_do_on_page_switch; (* TODO : make it work !!! *) - let rec search_f () = + let rec search_f () = search_lbl#misc#show (); search_input#misc#show (); prerr_endline "search_f called"; if !start_of_search = None then begin (* A full new search is starting *) - start_of_search := - Some ((get_current_view ()).view#buffer#create_mark - ((get_current_view ()).view#buffer#get_iter_at_mark `INSERT)); + start_of_search := + Some (session_notebook#current_term.script#buffer#create_mark + (session_notebook#current_term.script#buffer#get_iter_at_mark `INSERT)); start_of_found := !start_of_search; end_of_found := !start_of_search; matched_word := Some ""; end; - let txt = search_input#entry#text in - let v = (get_current_view ()).view in - let iit = v#buffer#get_iter_at_mark `SEL_BOUND + let txt = search_input#entry#text in + let v = session_notebook#current_term.script in + let iit = v#buffer#get_iter_at_mark `SEL_BOUND and insert_iter = v#buffer#get_iter_at_mark `INSERT in prerr_endline ("SELBOUND="^(string_of_int iit#offset)); prerr_endline ("INSERT="^(string_of_int insert_iter#offset)); - + (match - if !search_forward then iit#forward_search txt + if !search_forward then iit#forward_search txt else let npi = iit#forward_chars (Glib.Utf8.length txt) in - match + match (npi#offset = (v#buffer#get_iter_at_mark `INSERT)#offset), - (let t = iit#get_text ~stop:npi in - !flash_info (t^"\n"^txt); + (let t = iit#get_text ~stop:npi in + flash_info (t^"\n"^txt); t = txt) - with - | true,true -> - (!flash_info "T,T";iit#backward_search txt) - | false,true -> !flash_info "F,T";Some (iit,npi) + with + | true,true -> + (flash_info "T,T";iit#backward_search txt) + | false,true -> flash_info "F,T";Some (iit,npi) | _,false -> (iit#backward_search txt) - with - | None -> + with + | None -> if !ready_to_wrap_search then begin ready_to_wrap_search := false; - !flash_info "Search wrapped"; - v#buffer#place_cursor + flash_info "Search wrapped"; + v#buffer#place_cursor (if !search_forward then v#buffer#start_iter else v#buffer#end_iter); search_f () end else begin - if !search_forward then !flash_info "Search at end" - else !flash_info "Search at start"; + if !search_forward then flash_info "Search at end" + else flash_info "Search at start"; ready_to_wrap_search := true end - | Some (start,stop) -> + | Some (start,stop) -> prerr_endline "search: before moving marks"; prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset)); prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset)); @@ -3415,105 +3115,49 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); v#scroll_to_mark `SEL_BOUND ) in - ignore (search_input#entry#event#connect#key_release + ignore (search_input#entry#event#connect#key_release ~callback: (fun ev -> if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin - let v = (get_current_view ()).view in - (match !start_of_search with - | None -> + let v = session_notebook#current_term.script in + (match !start_of_search with + | None -> prerr_endline "search_key_rel: Placing sel_bound"; - v#buffer#move_mark - `SEL_BOUND + v#buffer#move_mark + `SEL_BOUND (v#buffer#get_iter_at_mark `INSERT) - | Some mk -> let it = v#buffer#get_iter_at_mark + | Some mk -> let it = v#buffer#get_iter_at_mark (`MARK mk) in prerr_endline "search_key_rel: Placing cursor"; v#buffer#place_cursor it; start_of_search := None ); - search_input#entry#set_text ""; + search_input#entry#set_text ""; v#coerce#misc#grab_focus (); - end; + end; false )); ignore (search_input#entry#connect#changed search_f); - - (* - ignore (search_if#connect#activate - ~callback:(fun b -> - search_forward:= true; - search_input#entry#coerce#misc#grab_focus (); - search_f (); - ) - ); - ignore (search_ib#connect#activate - ~callback:(fun b -> - search_forward:= false; - - (* Must restore the SEL_BOUND mark after - grab_focus ! *) - let v = (get_current_view ()).view in - let old_sel = v#buffer#get_iter_at_mark `SEL_BOUND - in - search_input#entry#coerce#misc#grab_focus (); - v#buffer#move_mark `SEL_BOUND old_sel; - search_f (); - )); - *) - let status_context = status_bar#new_context "Messages" in - let flash_context = status_bar#new_context "Flash" in - ignore (status_context#push "Ready"); - status := Some status_bar; - push_info := (fun s -> ignore (status_context#push s)); - pop_info := (fun () -> status_context#pop ()); - flash_info := (fun ?(delay=5000) s -> flash_context#flash ~delay s); - - (* Location display *) + push_info "Ready"; + (* Location display *) let l = GMisc.label - ~text:"Line: 1 Char: 1" - ~packing:lower_hbox#pack () in + ~text:"Line: 1 Char: 1" + ~packing:lower_hbox#pack () in l#coerce#misc#set_name "location"; set_location := l#set_text; - (* Progress Bar *) - pulse := - (let pb = GRange.progress_bar ~pulse_step:0.2 ~packing:lower_hbox#pack () - in pb#set_text "CoqIde started";pb)#pulse; - let tv2 = GText.view ~packing:(sw2#add) () in - tv2#misc#set_name "GoalWindow"; - let _ = tv2#set_editable false in - let _ = tv2#buffer in - let tv3 = GText.view ~packing:(sw3#add) () in - tv2#misc#set_name "MessageWindow"; - let _ = tv2#set_wrap_mode `CHAR in - let _ = tv3#set_wrap_mode `WORD in - let _ = tv3#set_editable false in - let _ = GtkBase.Widget.add_events tv2#as_widget - [`ENTER_NOTIFY;`POINTER_MOTION] in - let _ = - tv2#event#connect#motion_notify - ~callback: - (fun e -> - let win = match tv2#get_window `WIDGET with - | None -> assert false - | Some w -> w in - let x,y = Gdk.Window.get_pointer_location win in - let b_x,b_y = tv2#window_to_buffer_coords ~tag:`WIDGET ~x ~y in - let it = tv2#get_iter_at_location ~x:b_x ~y:b_y in - let tags = it#tags in - List.iter - (fun t -> - ignore(GtkText.Tag.event t#as_tag tv2#as_widget e it#as_iter)) - tags; - false) in - change_font := - (fun fd -> - tv2#misc#modify_font fd; - tv3#misc#modify_font fd; - Vector.iter - (fun {view=view} -> view#misc#modify_font fd) - input_views; + lower_hbox#pack pbar#coerce; + pbar#set_text "CoqIde started"; + (* XXX *) + change_font := + (fun fd -> + List.iter + (fun {script=view; proof_view=prf_v; message_view=msg_v} -> + view#misc#modify_font fd; + prf_v#misc#modify_font fd; + msg_v#misc#modify_font fd + ) + session_notebook#pages; ); let about_full_string = "\nCoq is developed by the Coq Development Team\ @@ -3539,7 +3183,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); b#insert ~iter:b#start_iter "\n\n"; if Glib.Utf8.validate ("You are running " ^ coq_version) then b#insert ~iter:b#start_iter ("You are running " ^ coq_version); if Glib.Utf8.validate initial_string then b#insert ~iter:b#start_iter initial_string; - (try + (try let image = lib_ide_file "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; @@ -3549,7 +3193,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); in let about (b:GText.buffer) = - (try + (try let image = lib_ide_file "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; @@ -3563,77 +3207,30 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); then b#insert coq_version in - initial_about tv2#buffer; w#add_accel_group accel_group; (* Remove default pango menu for textviews *) - ignore (tv2#event#connect#button_press ~callback: - (fun ev -> GdkEvent.Button.button ev = 3)); - ignore (tv3#event#connect#button_press ~callback: - (fun ev -> GdkEvent.Button.button ev = 3)); - tv2#misc#set_can_focus true; - tv3#misc#set_can_focus true; - ignore (tv2#buffer#create_mark - ~name:"end_of_conclusion" - tv2#buffer#start_iter); - ignore (tv3#buffer#create_tag - ~name:"error" - [`FOREGROUND "red"]); w#show (); - message_view := Some tv3; - proof_view := Some tv2; - tv2#misc#modify_font !current.text_font; - tv3#misc#modify_font !current.text_font; - ignore (about_m#connect#activate - ~callback:(fun () -> tv2#buffer#set_text ""; about tv2#buffer)); + ignore (about_m#connect#activate + ~callback:(fun () -> let prf_v = session_notebook#current_term.proof_view in + prf_v#buffer#set_text ""; about prf_v#buffer)); (* - ignore (faq_m#connect#activate - ~callback:(fun () -> - load (lib_ide_file "FAQ"))); - + *) - resize_window := (fun () -> - w#resize + resize_window := (fun () -> + w#resize ~width:!current.window_width ~height:!current.window_height); - - ignore (w#misc#connect#size_allocate - (let old_w = ref 0 - and old_h = ref 0 in - fun {Gtk.width=w;Gtk.height=h} -> - if !old_w <> w or !old_h <> h then - begin - old_h := h; - old_w := w; - hb#set_position (w/2); - hb2#set_position (h/2); - !current.window_height <- h; - !current.window_width <- w; - end - )); - ignore(nb#connect#switch_page + ignore(nb#connect#switch_page ~callback: - (fun i -> + (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 _ -> - if !current.contextual_menus_on_goal then - begin - let w = (Option.get (get_active_view ()).analyzed_view) in - !push_info "Computing advanced goal's menus"; - prerr_endline "Entering Goal Window. Computing Menus...."; - w#show_goals_full; - prerr_endline "....Done with Goal menu"; - !pop_info(); - end; - false; - )); - if List.length files >=1 then + if List.length files >=1 then begin - List.iter (fun f -> - if Sys.file_exists f then load f else + List.iter (fun f -> + if Sys.file_exists f then load f else let f = if Filename.check_suffix f ".v" then f else f^".v" in load_file (fun s -> print_endline s; exit 1) f) files; @@ -3641,69 +3238,66 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); end else begin - let view = create_input_tab "*Unnamed Buffer*" in - let index = add_input_view {view = view; - analyzed_view = None; - } - in - (get_input_view index).analyzed_view <- Some (new analyzed_view index); + let session = create_session () in + let index = session_notebook#append_term session in activate_input index; - set_tab_image index ~icon:`YES; - view#misc#modify_font !current.text_font end; + initial_about session_notebook#current_term.proof_view#buffer; + !show_toolbar !current.show_toolbar; + session_notebook#current_term.script#misc#grab_focus () ;; -(* This function check every half of second if GeoProof has send +(* This function check every half of second if GeoProof has send something on his private clipboard *) -let rec check_for_geoproof_input () = +let rec check_for_geoproof_input () = let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in while true do Thread.delay 0.1; let s = cb_Dr#text in - (match s with - Some s -> + (match s with + Some s -> if s <> "Ack" then - (get_current_view()).view#buffer#insert (s^"\n"); + session_notebook#current_term.script#buffer#insert (s^"\n"); cb_Dr#set_text "Ack" | None -> () ); (* cb_Dr#clear does not work so i use : *) - (* cb_Dr#set_text "Ack" *) + (* cb_Dr#set_text "Ack" *) done - - -let start () = + + +let start () = let files = Coq.init () in ignore_break (); GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc"); - (try + (try GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc"); with Not_found -> ()); ignore (GtkMain.Main.init ()); - GtkData.AccelGroup.set_default_mod_mask + GtkData.AccelGroup.set_default_mod_mask (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]); - cb_ := Some (GData.clipboard Gdk.Atom.primary); ignore ( Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL; `WARNING;`CRITICAL] - (fun ~level msg -> + (fun ~level msg -> if level land Glib.Message.log_level `WARNING <> 0 then Pp.warning msg else failwith ("Coqide internal error: " ^ msg))); Command_windows.main (); - Blaster_window.main 9; init_stdout (); main files; - if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); - while true do - try - GtkThread.main () + if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ()); + while true do + try + GtkThread.main () with | Sys.Break -> prerr_endline "Interrupted." ; flush stderr - | e -> + | e -> Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e)); flush stderr; crash_save 127 done + + -- cgit v1.2.3