From aba5307d448d60e46d469d81d253b96f9d3e35f6 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Sat, 5 May 2012 23:51:09 +0000 Subject: Renamed Undo to conform to CoqIDE widget naming convention. In addition, made various hack to handle GtkSourceView built-in undo/redo and made method types and names more compliant with the one of Gtk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15280 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqide.ml | 14 ++-- ide/coqide_ui.ml | 2 +- ide/ide.mllib | 2 +- ide/undo.ml | 178 ------------------------------------------------ ide/undo.mli | 44 ------------ ide/wg_ScriptView.ml | 185 ++++++++++++++++++++++++++++++++++++++++++++++++++ ide/wg_ScriptView.mli | 44 ++++++++++++ 7 files changed, 238 insertions(+), 231 deletions(-) delete mode 100644 ide/undo.ml delete mode 100644 ide/undo.mli create mode 100644 ide/wg_ScriptView.ml create mode 100644 ide/wg_ScriptView.mli diff --git a/ide/coqide.ml b/ide/coqide.ml index c47b301ff4..b5181b0f16 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -63,7 +63,7 @@ end type viewable_script = - {script : Undo.undoable_view; + {script : Wg_ScriptView.script_view; tab_label : GMisc.label; proof_view : GText.view; message_view : GText.view; @@ -515,7 +515,7 @@ let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) = let custom_project_files = ref [] let sup_args = ref [] -class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct _fn = +class analyzed_view (_script:Wg_ScriptView.script_view) (_pv:GText.view) (_mv:GText.view) _cs _ct _fn = object(self) val input_view = _script val input_buffer = _script#buffer @@ -1369,7 +1369,7 @@ let create_session file = () in let script = - Undo.undoable_view + Wg_ScriptView.script_view ~source_buffer:script_buffer ~show_line_numbers:true ~wrap_mode:`NONE () in @@ -1638,7 +1638,7 @@ let load_file handler f = prerr_endline "Loading: highlight"; input_buffer#set_modified false; prerr_endline "Loading: clear undo"; - session.script#clear_undo; + session.script#clear_undo (); prerr_endline "Loading: success" end with @@ -2116,10 +2116,10 @@ let main files = ~callback:(fun _ -> do_if_not_computing "undo" (fun sess -> ignore (sess.analyzed_view#without_auto_complete - (fun () -> session_notebook#current_term.script#undo) ())) + session_notebook#current_term.script#undo ())) [session_notebook#current_term]) ~stock:`UNDO; - GAction.add_action "Clear Undo Stack" ~label:"_Clear Undo Stack" - ~callback:(fun _ -> ignore session_notebook#current_term.script#clear_undo); + GAction.add_action "Redo" ~stock:`REDO + ~callback:(fun _ -> ignore (session_notebook#current_term.script#redo ())); GAction.add_action "Cut" ~callback:(fun _ -> GtkSignal.emit_unit (get_active_view_for_cp ()) ~sgn:GtkText.View.S.cut_clipboard diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index adfd9e6686..4ba378b7be 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -43,7 +43,7 @@ let init () = - + diff --git a/ide/ide.mllib b/ide/ide.mllib index 5a9a6a8743..c2df9bf47f 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -17,9 +17,9 @@ Preferences Project_file Ideutils Ideproof +Wg_ScriptView Coq_lex Gtk_parsing -Undo Coq Coq_commands Wg_Command diff --git a/ide/undo.ml b/ide/undo.ml deleted file mode 100644 index 9b33c11e5e..0000000000 --- a/ide/undo.ml +++ /dev/null @@ -1,178 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Delete (s,i,l) - | Delete (s,i,l) -> Insert (s,i,l) - -type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj - -class undoable_view (tv : source_view) = - let undo_lock = ref true in -object(self) - inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super - val history = (Stack.create () : action Stack.t) - val redo = (Queue.create () : action Queue.t) - val nredo = (Stack.create () : action Stack.t) - - method private dump_debug = - if false (* !debug *) then begin - prerr_endline "==========Stack top============="; - Stack.iter - (fun e -> match e with - | Insert(s,p,l) -> - Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l - | Delete(s,p,l) -> - Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l) - history; - Printf.eprintf "Stack size %d\n" (Stack.length history); - prerr_endline "==========Stack Bottom=========="; - prerr_endline "==========Queue start============="; - Queue.iter - (fun e -> match e with - | Insert(s,p,l) -> - Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l - | Delete(s,p,l) -> - Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l) - redo; - Printf.eprintf "Stack size %d\n" (Queue.length redo); - prerr_endline "==========Queue End==========" - - end - - method clear_undo = Stack.clear history; Stack.clear nredo; Queue.clear redo - - method undo = if !undo_lock then begin - undo_lock := false; - prerr_endline "UNDO"; - try begin - let r = - match Stack.pop history with - | Insert(s,p,l) as act -> - let start = self#buffer#get_iter_at_char p in - (self#buffer#delete_interactive - ~start - ~stop:(start#forward_chars l) - ()) or - (Stack.push act history; false) - | Delete(s,p,l) as act -> - let iter = self#buffer#get_iter_at_char p in - (self#buffer#insert_interactive ~iter s) or - (Stack.push act history; false) - in if r then begin - let act = Stack.pop history in - Queue.push act redo; - Stack.push act nredo - end; - undo_lock := true; - r - end - with Stack.Empty -> - undo_lock := true; - false - end else - (prerr_endline "UNDO DISCARDED"; true) - - method redo = prerr_endline "REDO"; true - initializer -(* INCORRECT: is called even while undoing... - ignore (self#buffer#connect#mark_set - ~callback: - (fun it tm -> if !undo_lock && not (Queue.is_empty redo) then begin - Stack.iter (fun e -> Stack.push (neg e) history) nredo; - Stack.clear nredo; - Queue.iter (fun e -> Stack.push e history) redo; - Queue.clear redo; - end) - ); -*) - ignore (self#buffer#connect#insert_text - ~callback: - (fun it s -> - if !undo_lock && not (Queue.is_empty redo) then begin - Stack.iter (fun e -> Stack.push (neg e) history) nredo; - Stack.clear nredo; - Queue.iter (fun e -> Stack.push e history) redo; - Queue.clear redo; - end; -(* let pos = it#offset in - if Stack.is_empty history or - s=" " or s="\t" or s="\n" or - (match Stack.top history with - | Insert(old,opos,olen) -> - opos + olen <> pos - | _ -> true) - then *) - Stack.push (Insert(s,it#offset,Glib.Utf8.length s)) history - (*else begin - match Stack.pop history with - | Insert(olds,offset,len) -> - Stack.push - (Insert(olds^s, - offset, - len+(Glib.Utf8.length s))) - history - | _ -> assert false - end*); - self#dump_debug - )); - ignore (self#buffer#connect#delete_range - ~callback: - (fun ~start ~stop -> - if !undo_lock && not (Queue.is_empty redo) then begin - Queue.iter (fun e -> Stack.push e history) redo; - Queue.clear redo; - end; - let start_offset = start#offset in - let stop_offset = stop#offset in - let s = self#buffer#get_text ~start ~stop () in -(* if Stack.is_empty history or (match Stack.top history with - | Delete(old,opos,olen) -> - olen=1 or opos <> start_offset - | _ -> true - ) - then -*) Stack.push - (Delete(s, - start_offset, - stop_offset - start_offset - )) - history - (* else begin - match Stack.pop history with - | Delete(olds,offset,len) -> - Stack.push - (Delete(olds^s, - offset, - len+(Glib.Utf8.length s))) - history - | _ -> assert false - - end*); - self#dump_debug - )) -end - -let undoable_view ?(source_buffer:GSourceView2.source_buffer option) ?draw_spaces = - GtkSourceView2.SourceView.make_params [] ~cont:( - GtkText.View.make_params ~cont:( - GContainer.pack_container ~create: - (fun pl -> let w = match source_buffer with - | None -> GtkSourceView2.SourceView.new_ () - | Some buf -> GtkSourceView2.SourceView.new_with_buffer - (Gobject.try_cast buf#as_buffer "GtkSourceBuffer") in - let w = Gobject.unsafe_cast w in - Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl; - Gaux.may (GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces; - ((new undoable_view w) : undoable_view)))) diff --git a/ide/undo.mli b/ide/undo.mli deleted file mode 100644 index b6a59ba756..0000000000 --- a/ide/undo.mli +++ /dev/null @@ -1,44 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* -object - inherit GSourceView2.source_view - method undo : bool - method redo : bool - method clear_undo : unit -end - -val undoable_view : - ?source_buffer:GSourceView2.source_buffer -> - ?draw_spaces:SourceView2Enums.source_draw_spaces_flags list -> - ?auto_indent:bool -> - ?highlight_current_line:bool -> - ?indent_on_tab:bool -> - ?indent_width:int -> - ?insert_spaces_instead_of_tabs:bool -> - ?right_margin_position:int -> - ?show_line_marks:bool -> - ?show_line_numbers:bool -> - ?show_right_margin:bool -> - ?smart_home_end:SourceView2Enums.source_smart_home_end_type -> - ?tab_width:int -> - ?editable:bool -> - ?cursor_visible:bool -> - ?justification:GtkEnums.justification -> - ?wrap_mode:GtkEnums.wrap_mode -> - ?accepts_tab:bool -> - ?border_width:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> unit -> undoable_view diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml new file mode 100644 index 0000000000..e2801f92ac --- /dev/null +++ b/ide/wg_ScriptView.ml @@ -0,0 +1,185 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Delete (s,i,l) + | Delete (s,i,l) -> Insert (s,i,l) + +type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj + +class script_view (tv : source_view) = + let undo_lock = ref true in +object(self) + inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super + val history = (Stack.create () : action Stack.t) + val redo = (Queue.create () : action Queue.t) + val nredo = (Stack.create () : action Stack.t) + + method private dump_debug = + if false (* !debug *) then begin + prerr_endline "==========Stack top============="; + Stack.iter + (fun e -> match e with + | Insert(s,p,l) -> + Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l + | Delete(s,p,l) -> + Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l) + history; + Printf.eprintf "Stack size %d\n" (Stack.length history); + prerr_endline "==========Stack Bottom=========="; + prerr_endline "==========Queue start============="; + Queue.iter + (fun e -> match e with + | Insert(s,p,l) -> + Printf.eprintf "Insert of '%s' at %d (length %d)\n" s p l + | Delete(s,p,l) -> + Printf.eprintf "Delete '%s' from %d (length %d)\n" s p l) + redo; + Printf.eprintf "Stack size %d\n" (Queue.length redo); + prerr_endline "==========Queue End==========" + + end + + method clear_undo () = + Stack.clear history; + Stack.clear nredo; + Queue.clear redo + + method undo () = if !undo_lock then begin + undo_lock := false; + prerr_endline "UNDO"; + try begin + let r = + match Stack.pop history with + | Insert(s,p,l) as act -> + let start = self#buffer#get_iter_at_char p in + (self#buffer#delete_interactive + ~start + ~stop:(start#forward_chars l) + ()) or + (Stack.push act history; false) + | Delete(s,p,l) as act -> + let iter = self#buffer#get_iter_at_char p in + (self#buffer#insert_interactive ~iter s) or + (Stack.push act history; false) + in if r then begin + let act = Stack.pop history in + Queue.push act redo; + Stack.push act nredo + end; + undo_lock := true; + r + end + with Stack.Empty -> + undo_lock := true; + false + end else + (prerr_endline "UNDO DISCARDED"; true) + + method redo () = prerr_endline "REDO"; true + initializer +(* INCORRECT: is called even while undoing... + ignore (self#buffer#connect#mark_set + ~callback: + (fun it tm -> if !undo_lock && not (Queue.is_empty redo) then begin + Stack.iter (fun e -> Stack.push (neg e) history) nredo; + Stack.clear nredo; + Queue.iter (fun e -> Stack.push e history) redo; + Queue.clear redo; + end) + ); +*) + ignore (self#buffer#connect#insert_text + ~callback: + (fun it s -> + if !undo_lock && not (Queue.is_empty redo) then begin + Stack.iter (fun e -> Stack.push (neg e) history) nredo; + Stack.clear nredo; + Queue.iter (fun e -> Stack.push e history) redo; + Queue.clear redo; + end; +(* let pos = it#offset in + if Stack.is_empty history or + s=" " or s="\t" or s="\n" or + (match Stack.top history with + | Insert(old,opos,olen) -> + opos + olen <> pos + | _ -> true) + then *) + Stack.push (Insert(s,it#offset,Glib.Utf8.length s)) history + (*else begin + match Stack.pop history with + | Insert(olds,offset,len) -> + Stack.push + (Insert(olds^s, + offset, + len+(Glib.Utf8.length s))) + history + | _ -> assert false + end*); + self#dump_debug + )); + ignore (self#buffer#connect#delete_range + ~callback: + (fun ~start ~stop -> + if !undo_lock && not (Queue.is_empty redo) then begin + Queue.iter (fun e -> Stack.push e history) redo; + Queue.clear redo; + end; + let start_offset = start#offset in + let stop_offset = stop#offset in + let s = self#buffer#get_text ~start ~stop () in +(* if Stack.is_empty history or (match Stack.top history with + | Delete(old,opos,olen) -> + olen=1 or opos <> start_offset + | _ -> true + ) + then +*) Stack.push + (Delete(s, + start_offset, + stop_offset - start_offset + )) + history + (* else begin + match Stack.pop history with + | Delete(olds,offset,len) -> + Stack.push + (Delete(olds^s, + offset, + len+(Glib.Utf8.length s))) + history + | _ -> assert false + + end*); + self#dump_debug + )); + (* Redirect the undo/redo signals of the underlying GtkSourceView *) + ignore (self#connect#undo (fun _ -> ignore (self#undo ()); GtkSignal.stop_emit())); + ignore (self#connect#redo (fun _ -> ignore (self#redo ()); GtkSignal.stop_emit())); + +end + +let script_view ?(source_buffer:GSourceView2.source_buffer option) ?draw_spaces = + GtkSourceView2.SourceView.make_params [] ~cont:( + GtkText.View.make_params ~cont:( + GContainer.pack_container ~create: + (fun pl -> let w = match source_buffer with + | None -> GtkSourceView2.SourceView.new_ () + | Some buf -> GtkSourceView2.SourceView.new_with_buffer + (Gobject.try_cast buf#as_buffer "GtkSourceBuffer") in + let w = Gobject.unsafe_cast w in + Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl; + Gaux.may (GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces; + ((new script_view w) : script_view)))) diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli new file mode 100644 index 0000000000..bc738257cc --- /dev/null +++ b/ide/wg_ScriptView.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* +object + inherit GSourceView2.source_view + method undo : unit -> bool + method redo : unit -> bool + method clear_undo : unit -> unit +end + +val script_view : + ?source_buffer:GSourceView2.source_buffer -> + ?draw_spaces:SourceView2Enums.source_draw_spaces_flags list -> + ?auto_indent:bool -> + ?highlight_current_line:bool -> + ?indent_on_tab:bool -> + ?indent_width:int -> + ?insert_spaces_instead_of_tabs:bool -> + ?right_margin_position:int -> + ?show_line_marks:bool -> + ?show_line_numbers:bool -> + ?show_right_margin:bool -> + ?smart_home_end:SourceView2Enums.source_smart_home_end_type -> + ?tab_width:int -> + ?editable:bool -> + ?cursor_visible:bool -> + ?justification:GtkEnums.justification -> + ?wrap_mode:GtkEnums.wrap_mode -> + ?accepts_tab:bool -> + ?border_width:int -> + ?width:int -> + ?height:int -> + ?packing:(GObj.widget -> unit) -> + ?show:bool -> unit -> script_view -- cgit v1.2.3