diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-13 02:51:30 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-13 02:51:30 +0000 |
| commit | 2ca3e39dbcdd07d6bc777f1514999109827a2410 (patch) | |
| tree | 578670e90619a9a1cd8f4d3e6b82fbfdb917d1f6 /ide/wg_ScriptView.mli | |
| parent | 0296f82e4cd1a13fa5567373a03a66aad9e0987a (diff) | |
Added semantic completion in CoqIDE. (Should also add an option for that...)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15317 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_ScriptView.mli')
| -rw-r--r-- | ide/wg_ScriptView.mli | 50 |
1 files changed, 25 insertions, 25 deletions
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli index a2024eeec..b229eacfe 100644 --- a/ide/wg_ScriptView.mli +++ b/ide/wg_ScriptView.mli @@ -10,7 +10,7 @@ type source_view = [ Gtk.text_view | `sourceview ] Gtk.obj -class script_view : source_view -> +class script_view : source_view -> Coq.coqtop -> object inherit GSourceView2.source_view method undo : unit -> bool @@ -20,27 +20,27 @@ object method set_auto_complete : bool -> 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 +val script_view : Coq.coqtop -> + ?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 |