diff options
Diffstat (limited to 'ide/wg_ScriptView.ml')
| -rw-r--r-- | ide/wg_ScriptView.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index 6d7dc6bcc..8796d3581 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -278,7 +278,7 @@ class script_view (tv : source_view) (ct : Coq.coqtop) = let view = new GSourceView2.source_view (Gobject.unsafe_cast tv) in let completion = new Wg_Completion.complete_model ct view#buffer in -let _ = new Wg_Completion.complete_popup completion (view :> GText.view) in +let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in object (self) inherit GSourceView2.source_view (Gobject.unsafe_cast tv) as super @@ -397,6 +397,8 @@ object (self) self#buffer#delete_mark (`MARK stop_mark) | _ -> () + method complete_popup = popup + method undo = undo_manager#undo method redo = undo_manager#redo method clear_undo = undo_manager#clear_undo |