aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
authorGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-05-07 16:57:39 +0000
committerGravatar monate <monate@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-05-07 16:57:39 +0000
commitee280ef0957206a0cae7d510806a8667f87a510c (patch)
treedbcebf3d3d2016553cd5b13101e939f3f494ca58 /ide
parentdd53f04b22a4ba3b539fb25ba23d7757e5af2349 (diff)
coqide: toolbar/autosave
Hugo: Suppression du type dans les notations == et <> entre Suppression du type dans les notations == et <> entre volution second traducteur selon discussion TYPES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3993 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
-rw-r--r--ide/.coqide-gtk2rc11
-rw-r--r--ide/FAQ39
-rw-r--r--ide/command_windows.ml10
-rw-r--r--ide/config_lexer.mll10
-rw-r--r--ide/config_parser.mly9
-rw-r--r--ide/coq.ml47
-rw-r--r--ide/coq.mli16
-rw-r--r--ide/coq_commands.ml10
-rw-r--r--ide/coq_tactics.ml13
-rw-r--r--ide/coqide.ml1197
-rw-r--r--ide/extract_index.mll9
-rw-r--r--ide/find_phrase.mll10
-rw-r--r--ide/highlight.mll15
-rw-r--r--ide/ideutils.ml28
-rw-r--r--ide/preferences.ml205
-rw-r--r--ide/undo.ml10
-rw-r--r--ide/undo.mli10
-rw-r--r--ide/utils/configwin_ihm.ml10
-rw-r--r--ide/utils/editable_cells.ml102
19 files changed, 1181 insertions, 580 deletions
diff --git a/ide/.coqide-gtk2rc b/ide/.coqide-gtk2rc
index 11099742e..7a74a469d 100644
--- a/ide/.coqide-gtk2rc
+++ b/ide/.coqide-gtk2rc
@@ -6,9 +6,12 @@
gtk-key-theme-name = "Emacs"
+#pixmap_path "/home/"
+
binding "text" {
bind "<ctrl>k" { "set-anchor" ()
"move-cursor" (display-line-ends,1,0)
+ "move-cursor" (visual-positions,1,0)
"cut-clipboard" ()
}
bind "<ctrl>w" { "cut-clipboard" () }
@@ -22,6 +25,7 @@ class "GtkTextView" binding "text"
style "views" {
base[NORMAL] = "CornSilk"
+# bg_pixmap[NORMAL] = "background.jpg"
}
class "GtkTextView" style "views"
@@ -36,3 +40,10 @@ font_name = "Monospace 10"
}
widget "*location*" style "location"
+
+gtk-can-change-accels = 1
+
+style "men" {
+#
+}
+widget "GtkMenu" style "men"
diff --git a/ide/FAQ b/ide/FAQ
index e00131f7b..ba97211e5 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -1,36 +1,38 @@
+ CoqIde FAQ
+
+Q0) What is CoqIde?
+R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more informations
+
Q1) How to enable Emacs keybindings?
R1: Insert
gtk-key-theme-name = "Emacs"
in your ".coqide-gtk2rc" file. It may be in the current dir
or in $HOME dir. This is done by default.
-
Q2) How to enable antialiased fonts?
R2) Set the GDK_USE_XFT variable to 1. This is by default with Gtk >= 2.2.
- If some of your fonts seem not to be available, set to 0.
+ If some of your fonts are not available, set GDK_USE_XFT to 0.
-Q4) How can use Forall and Exists pretty symbols ?
+Q4) How to use those Forall and Exists pretty symbols?
R4) Thanks to the Notation features in Coq, you just need to insert these
lines in your Coq Buffer :
======================================================================
Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10).
Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
======================================================================
-Copy/Paste from this file will not work.
+Copy/Paste of these lines from this file will not work outside of CoqIde.
You need to load a file containing these lines or to enter the "∀"
-using an input method. As a convenience, you may put these lines in
+using an input method (see Q5). As a convenience, you may put these lines in
a utf8.v file and start coqide with :
coqide -l utf8.v
-In the ide subdir of Coq sources, you will find a sample utf8.v with some
-notations
-
+In the ide subdir of Coq library, you will find a sample utf8.v with some
+pretty notations.
-
-Input Methods:
--First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script widow.
+Q5) How to define an input method for non ASCII symbols?
+R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script widow.
2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀"
in UTF-8.
- 2203 is for exists. See http://www.unicode.org for more.
+ 2203 is for exists. See http://www.unicode.org for more codes.
-Second solution : rebind "<AltGr>a" to forall and "<AltGr>e" to exists.
Under X11, you need to use something like
xmodmap -e "keycode 24 = a A F13 F13"
@@ -40,7 +42,16 @@ Input Methods:
bind "F14" {"insert-at-cursor" ("∃")}
to your "binding "text"" section in .coqiderc-gtk2rc.
The strange ("∀") argument is the UTF-8 encoding for
- 0x2200. It is computed by lablgtk2 by
+ 0x2200.
+ You can compute these encodings using the lablgtk2 toplevel with
Glib.Utf8.from_unichar 0x2200;;
- Further symbols can be bound on higher Fxx key symbols.
+ Further symbols can be bound on higher Fxx keys or on even on other keys you
+ do not need .
+
+Q6) How to build a custom CoqIde with user ml code?
+R6) Use
+ coqmktop -ide -byte m1.cmo...mi.cmo
+ or
+ coqmktop -ide -opt m1.cmx...mi.cmx
+
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 7a08d209c..6c0048ca3 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
let decompose_tab w =
let vbox = new GPack.box ((Gobject.try_cast w "GtkBox"):Gtk.box Gtk.obj) in
let l = vbox#children in
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 480f04e24..778a9c7e7 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
{
open Lexing
diff --git a/ide/config_parser.mly b/ide/config_parser.mly
index fe9071964..19da4887c 100644
--- a/ide/config_parser.mly
+++ b/ide/config_parser.mly
@@ -1,3 +1,12 @@
+/***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************/
+
+/* $Id$ */
%{
diff --git a/ide/coq.ml b/ide/coq.ml
index c31306131..01a1c4c13 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
open Vernac
open Vernacexpr
open Pfedit
@@ -310,3 +320,40 @@ let concl_menu (_,_,concl,_) =
"Right", "Right.";
]
+
+
+let id_of_name = function
+ | Names.Anonymous -> id_of_string "x"
+ | Names.Name x -> x
+
+let make_cases s =
+ let qualified_name = Libnames.qualid_of_string s in
+ let glob_ref = Nametab.locate qualified_name in
+ match glob_ref with
+ | Libnames.IndRef i ->
+ let _,
+ {
+ Declarations.mind_nparams = np ;
+ Declarations.mind_consnames = carr ;
+ Declarations.mind_nf_lc = tarr }
+ = Global.lookup_inductive i
+ in
+ Util.array_fold_right2
+ (fun n t l ->
+ let (al,_) = Term.decompose_prod t in
+ let al,_ = Util.list_chop (List.length al - np) al in
+ let rec rename avoid = function
+ | [] -> []
+ | (n,_)::l ->
+ let n' = Tactics.next_global_ident_away
+ (id_of_name n)
+ avoid
+ in (string_of_id n')::(rename (n'::avoid) l)
+ in
+ let al' = rename [] (List.rev al) in
+ (string_of_id n :: al') :: l
+ )
+ carr
+ tarr
+ []
+ | _ -> raise Not_found
diff --git a/ide/coq.mli b/ide/coq.mli
index b2881a70d..7769a037b 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
open Names
open Term
open Environ
@@ -24,10 +34,6 @@ val print_no_goal : unit -> string
val process_exn : exn -> string*((int*int) option)
-type word_class = Normal | Kwd | Reserved
-
-val word_class : string -> word_class
-
type reset_info = NoReset | Reset of Names.identifier * bool ref
val compute_reset_info : Vernacexpr.vernac_expr -> reset_info
@@ -40,3 +46,5 @@ val concl_menu : concl -> (string * string) list
val is_in_coq_lib : string -> bool
+val make_cases : string -> string list list
+
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index a2db621fd..9cd851820 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
let commands = [
["Abort";
"Add Abstract Ring";
diff --git a/ide/coq_tactics.ml b/ide/coq_tactics.ml
index 7cac14da4..1d6783b6d 100644
--- a/ide/coq_tactics.ml
+++ b/ide/coq_tactics.ml
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
let tactics = [
"Abstract";
"Absurd";
@@ -119,6 +129,3 @@ let tactics = [
"Unfold";
"Unfold ... in";
]
-
-
-
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 2708fb825..0a258c741 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,9 +1,21 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
open Preferences
open Vernacexpr
open Coq
open Ideutils
+open Format
-let out_some s = match s with | None -> failwith "toto" | Some f -> f
+let out_some s = match s with
+ | None -> failwith "Internal error in out_some." | Some f -> f
let cb_ = ref None
let cb () = out_some !cb_
@@ -17,22 +29,18 @@ let warning_icon = `DIALOG_WARNING
let dialog_size = `DIALOG
let small_size = `SMALL_TOOLBAR
-let window_width = 800
-let window_height = 600
-
let initial_cwd = Sys.getcwd ()
let status = ref None
let push_info = ref (function s -> failwith "not ready")
let pop_info = ref (function s -> failwith "not ready")
-let flash_info = ref (function s -> failwith "not ready")
+let flash_info = ref (fun ?delay s -> failwith "not ready")
let set_location = ref (function s -> failwith "not ready")
let pulse = ref (function () -> failwith "not ready")
-let (font_selector:GWindow.font_selection_dialog option ref) = ref None
let (message_view:GText.view option ref) = ref None
let (proof_view:GText.view option ref) = ref None
@@ -129,12 +137,18 @@ object('self)
val mutable read_only : bool
val mutable filename : string option
val mutable stats : Unix.stats option
+ val mutable detached_views : GWindow.window list
+ method kill_detached_views : unit -> unit
+ 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
method update_stats : unit
method revert : unit
+ method auto_save : unit
method save : string -> bool
method save_as : string -> bool
method read_only : bool
@@ -191,7 +205,7 @@ let crash_save i =
(let filename = match av#filename with
| None ->
incr count;
- "Unamed_coqscript_"^(string_of_int !count)^".crashcoqide"
+ "Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
| Some f -> f^".crashcoqide"
in
try
@@ -281,6 +295,9 @@ 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
@@ -342,6 +359,9 @@ let rec complete_forward w (it:GText.iter) =
(* Reset this to None on page change ! *)
let (last_completion:(string*int*int*bool) option ref) = ref None
+let () = to_do_on_page_switch :=
+ (fun i -> last_completion := None)::!to_do_on_page_switch
+
let complete input_buffer w (offset:int) =
match !last_completion with
| Some (lw,loffset,lpos,backward)
@@ -392,6 +412,8 @@ let get_current_word () =
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 ->
prerr_endline "Some selected";
@@ -511,75 +533,117 @@ object(self)
val mutable read_only = false
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 = []
+
+ method add_detached_view (w:GWindow.window) =
+ detached_views <- w::detached_views
+ 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 () =
+ List.iter (fun w -> w#destroy ()) detached_views;
+ detached_views <- []
+
method view = input_view
method filename = filename
method stats = stats
method set_filename f =
filename <- f;
match f with
- | Some f -> stats <- my_stat f
- | None -> ()
+ | Some f -> stats <- my_stat f
+ | None -> ()
method update_stats =
match filename with
- | Some f -> stats <- my_stat f
- | _ -> ()
+ | Some f -> stats <- my_stat f
+ | _ -> ()
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 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:(let img = GMisc.image ()
- in img#set_stock warning_icon ~size:dialog_size;
- img#coerce)
- "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 ()
+ | 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 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
- | None -> ()
-
+ 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 warning_icon)
+ "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 =
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
else false
-
+ 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 =
+ input_buffer#modified &&
+ 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 !flash_info "Autosave failed"
+ with _ -> !flash_info "Autosave error"
+ end
+
method save_as f =
if Sys.file_exists f then
match (GToolbox.question_box ~title:"File exists on disk"
@@ -593,7 +657,7 @@ object(self)
("File "^f^"already exists")
)
with 1 -> self#save f
- | _ -> false
+ | _ -> false
else self#save f
method set_read_only b = read_only<-b
@@ -617,12 +681,12 @@ object(self)
method recenter_insert =
(* BUG : to investigate further:
FIXED : Never call GMain.* in thread !
- PLUS : GTK BUG ??? Cannot be called from a thread...*)
+ PLUS : GTK BUG ??? Cannot be called from a thread...*)
try
ignore (GtkThread.sync (input_view#scroll_to_mark
- ~use_align:false
- ~yalign:0.75
- ~within_margin:0.25)
+ ~use_align:false
+ ~yalign:0.75
+ ~within_margin:0.25)
`INSERT)
with _ -> prerr_endline "Could not recenter ERROR ignored"
@@ -631,22 +695,125 @@ object(self)
proof_view#buffer#set_text "";
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)
+ with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
+
+
+ method show_goals_full =
+ begin
+ try
+ proof_view#buffer#set_text "";
+ let s = Coq.get_current_goals () in
+ let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"]
+ 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"));
+ 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 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
+ (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";
+ ()
+ | _ -> ())
+ );
+ tag
+ in
List.iter
(fun ((_,_,_,(s,_)) as hyp) ->
- proof_buffer#insert (s^"\n"))
+ 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")
+ 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 sconcl;
+ proof_buffer#insert ~tags:[tag] sconcl;
proof_buffer#insert "\n";
let my_mark = `NAME "end_of_conclusion" in
proof_buffer#move_mark
@@ -656,117 +823,17 @@ object(self)
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
+ (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)
- with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
-
-
- method show_goals_full =
- begin
- try
- proof_view#buffer#set_text "";
- let s = Coq.get_current_goals () in
- let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"]
- 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"));
- 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 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
- (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";
- ()
- | _ -> ())
- );
- 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) ;
+ ignore (proof_view#scroll_to_mark my_mark) ;
with e -> prerr_endline (Printexc.to_string e)
end
@@ -785,17 +852,18 @@ object(self)
message_view#misc#draw None;
if localize then
(match 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
+ | 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;
));
None
@@ -852,14 +920,14 @@ object(self)
in
prerr_endline ("Completion of prefix : " ^ w);
match complete input_buffer w offset with
- | None -> ()
- | Some (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 `INSERT (it());
- ()
-
+ | None -> ()
+ | Some (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 `INSERT (it());
+ ()
+
method process_next_phrase display_goals do_highlight =
begin
try self#clear_message;
@@ -868,51 +936,51 @@ object(self)
!push_info "Coq is computing";
input_view#set_editable false;
end;
- begin match (self#find_phrase_starting_at self#get_start_of_input)
+ begin 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; false
- | Some(start,stop) ->
- prerr_endline "process_next_phrase : to_process highlight";
- let b = input_buffer in
- if do_highlight then begin
- input_buffer#apply_tag_by_name ~start ~stop "to_process";
- prerr_endline "process_next_phrase : to_process applied";
- process_pending ()
- end;
- prerr_endline "process_next_phrase : getting phrase";
- let phrase = start#get_slice ~stop in
- let r =
- match self#send_to_coq phrase true true true with
- | Some ast ->
+ | None ->
+ if do_highlight then begin
+ input_view#set_editable true;
+ !pop_info ();
+ end; false
+ | Some(start,stop) ->
+ prerr_endline "process_next_phrase : to_process highlight";
+ let b = input_buffer in
+ if do_highlight then begin
+ input_buffer#apply_tag_by_name ~start ~stop "to_process";
+ prerr_endline "process_next_phrase : to_process applied";
+ process_pending ()
+ end;
+ prerr_endline "process_next_phrase : getting phrase";
+ let phrase = start#get_slice ~stop in
+ let r =
+ match self#send_to_coq phrase true true true with
+ | Some ast ->
+ begin
+ b#move_mark ~where:stop (`NAME "start_of_input");
+ b#apply_tag_by_name "processed" ~start ~stop;
+ if (self#get_insert#compare) stop <= 0 then
begin
- b#move_mark ~where:stop (`NAME "start_of_input");
- b#apply_tag_by_name "processed" ~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
- start_of_phrase_mark
- end_of_phrase_mark ast;
- if display_goals then self#show_goals;
- true
- end
- | None -> false
- in
- if do_highlight then begin
- b#remove_tag_by_name ~start ~stop "to_process" ;
- input_view#set_editable true;
- !pop_info ();
- end;
- r;
+ 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
+ start_of_phrase_mark
+ end_of_phrase_mark ast;
+ if display_goals then self#show_goals;
+ true
+ end
+ | None -> false
+ in
+ if do_highlight then begin
+ b#remove_tag_by_name ~start ~stop "to_process" ;
+ input_view#set_editable true;
+ !pop_info ();
+ end;
+ r;
end
with e -> raise e
end
@@ -920,48 +988,49 @@ object(self)
method insert_this_phrase_on_success
show_output show_msg localize coqphrase insertphrase =
match self#send_to_coq coqphrase show_output show_msg localize with
- | Some ast ->
- begin
+ | Some ast ->
+ begin
+ 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 "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 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 insertphrase
- else input_buffer#insert ~iter:stop ("\n"^insertphrase);
+ 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;
+ 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 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 start_of_phrase_mark end_of_phrase_mark ast
- end
- | None -> ())
- | _ -> ())
- with _ -> ()*)
- true
- end
- | None -> self#insert_message ("Unsuccesfully tried: "^coqphrase);
- false
+ push_phrase start_of_phrase_mark end_of_phrase_mark ast
+ end
+ | None -> ())
+ | _ -> ())
+ with _ -> ()*)
+ true
+ end
+ | None -> self#insert_message ("Unsuccesfully tried: "^coqphrase);
+ false
method process_until_iter_or_error stop =
let start = self#get_start_of_input#copy in
@@ -1016,14 +1085,14 @@ object(self)
else begin
let t = pop () in
begin match t.reset_info with
- | Reset (id, ({contents=true} as v)) -> v:=false;
- (match snd t.ast with
- | VernacBeginSection _ | VernacDefineModule _
- | VernacDeclareModule _ | VernacDeclareModuleType _
- | VernacEndSegment _
- -> reset_to_mod id
- | _ -> reset_to id)
- | _ -> synchro ()
+ | Reset (id, ({contents=true} as v)) -> v:=false;
+ (match snd t.ast with
+ | VernacBeginSection _ | VernacDefineModule _
+ | VernacDeclareModule _ | VernacDeclareModuleType _
+ | VernacEndSegment _
+ -> reset_to_mod id
+ | _ -> reset_to id)
+ | _ -> synchro ()
end;
interp_last t.ast;
repush_phrase t
@@ -1050,8 +1119,8 @@ object(self)
begin
try
(match undos with
- | None -> synchro ()
- | Some n -> try Pfedit.undo n with _ -> synchro ());
+ | None -> synchro ()
+ | Some n -> try Pfedit.undo n with _ -> synchro ());
let start = if is_empty () then input_buffer#start_iter
else input_buffer#get_iter_at_mark (top ()).stop
in
@@ -1074,7 +1143,7 @@ Please restart and report NOW.";
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 backtrack_to_insert =
@@ -1103,37 +1172,37 @@ Please restart and report NOW.";
self#clear_message
in
begin match last_command with
- | {ast=_,VernacSolve _} ->
- begin
- try Pfedit.undo 1; ignore (pop ()); update_input ()
- with _ -> self#backtrack_to_no_lock start
- end
- | {ast=_,t;reset_info=Reset (id, {contents=true})} ->
- ignore (pop ());
- (match t with
- | VernacBeginSection _ | VernacDefineModule _
- | VernacDeclareModule _ | VernacDeclareModuleType _
- | VernacEndSegment _
- -> reset_to_mod id
- | _ -> reset_to id);
- update_input ()
- | { ast = _, ( VernacStartTheoremProof _
- | VernacDefinition (_,_,ProveBody _,_,_));
- reset_info=Reset(id,{contents=false})} ->
- ignore (pop ());
- (try
- Pfedit.delete_current_proof ()
- with e ->
- begin
- prerr_endline "WARNING : found a closed environment";
- raise e
- end);
- update_input ()
- | _ ->
- self#backtrack_to_no_lock start
+ | {ast=_,VernacSolve _} ->
+ begin
+ try Pfedit.undo 1; ignore (pop ()); update_input ()
+ with _ -> self#backtrack_to_no_lock start
+ end
+ | {ast=_,t;reset_info=Reset (id, {contents=true})} ->
+ ignore (pop ());
+ (match t with
+ | VernacBeginSection _ | VernacDefineModule _
+ | VernacDeclareModule _ | VernacDeclareModuleType _
+ | VernacEndSegment _
+ -> reset_to_mod id
+ | _ -> reset_to id);
+ update_input ()
+ | { ast = _, ( VernacStartTheoremProof _
+ | VernacDefinition (_,_,ProveBody _,_,_));
+ reset_info=Reset(id,{contents=false})} ->
+ ignore (pop ());
+ (try
+ Pfedit.delete_current_proof ()
+ with e ->
+ begin
+ prerr_endline "WARNING : found a closed environment";
+ raise e
+ end);
+ update_input ()
+ | _ ->
+ self#backtrack_to_no_lock start
end;
with
- | Size 0 -> (* !flash_info "Nothing to Undo"*)()
+ | Size 0 -> (* !flash_info "Nothing to Undo"*)()
);
!pop_info ();
Mutex.unlock coq_may_stop)
@@ -1146,40 +1215,41 @@ Please restart and report NOW.";
self#clear_message;
ignore (List.exists
(fun (cp,ip) ->
- self#insert_this_phrase_on_success true false false cp ip) l)
+ self#insert_this_phrase_on_success true false false
+ (cp^"\n") (ip^"\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";
- input_buffer#place_cursor i;
- self#process_until_insert_or_error
- end);
- true
- | l when List.mem `CONTROL l ->
- let k = GdkEvent.Key.keyval k in
- if GdkKeysyms._m=k
- then break ();
- false
- | l -> false
- end
- method disconnected_keypress_handler k =
- match GdkEvent.Key.state k 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";
+ input_buffer#place_cursor i;
+ self#process_until_insert_or_error
+ end);
+ true
| l when List.mem `CONTROL l ->
let k = GdkEvent.Key.keyval k in
- if GdkKeysyms._c=k
+ if GdkKeysyms._m=k
then break ();
false
| l -> false
-
+ end
+ 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 -> false
+
val mutable deact_id = None
val mutable act_id = None
@@ -1187,11 +1257,11 @@ Please restart and report NOW.";
method deactivate () =
is_active <- false;
(match act_id with None -> ()
- | Some id ->
- reset_initial ();
- input_view#misc#disconnect id;
- prerr_endline "DISCONNECTED old active : ";
- print_id id;
+ | 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);
@@ -1201,9 +1271,9 @@ Please restart and report NOW.";
method activate () =
is_active <- true;
(match deact_id with None -> ()
- | Some id -> input_view#misc#disconnect id;
- prerr_endline "DISCONNECTED old inactive : ";
- print_id id
+ | 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);
@@ -1213,8 +1283,8 @@ Please restart and report NOW.";
(out_some ((Vector.get input_views index).analyzed_view))
#filename
with
- | None -> initial_cwd
- | Some f -> Filename.dirname f
+ | None -> initial_cwd
+ | Some f -> Filename.dirname f
)
in
if not (is_in_coq_lib dir) then
@@ -1251,25 +1321,25 @@ Please restart and report NOW.";
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 ()
- | _ -> ())
+ | ')' ->
+ 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 () = browse_keyword (get_current_word ())
@@ -1304,13 +1374,14 @@ Please restart and report NOW.";
if input_buffer#modified then
set_tab_image index
(match (out_some (current_all.analyzed_view))#filename with
- | None -> saveas_icon
- | Some _ -> save_icon
+ | None -> saveas_icon
+ | Some _ -> save_icon
)
else set_tab_image index yes_icon;
));
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
@@ -1335,22 +1406,22 @@ Please restart and report NOW.";
"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 -> () )
+ | 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 -> () )
);
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 =
@@ -1417,17 +1488,38 @@ let create_input_tab filename =
let main files =
(* Statup preferences *)
- load_pref current;
+ load_pref ();
(* Main window *)
let w = GWindow.window
~allow_grow:true ~allow_shrink:true
- ~width:window_width ~height:window_height
+ ~width:!current.window_width ~height:!current.window_height
~title:"CoqIde" ()
in
- (* let accel_group = GtkData.AccelGroup.create () in *)
let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
+
+
+ (* Menu bar *)
let menubar = GMenu.menu_bar ~packing:vbox#pack () in
+
+ (* Tearable Toolbar *)
+ let handle = GBin.handle_box
+ ~show:!current.show_toolbar
+ ~handle_position:`LEFT
+ ~snap_edge:`LEFT
+ ~packing:vbox#pack
+ ()
+ in
+ let toolbar = GButton.toolbar
+ ~orientation:`HORIZONTAL
+ ~style:`BOTH
+ ~tooltips:true
+ ~packing:handle#add
+ ()
+ in
+ show_toolbar :=
+ (fun b -> if b then handle#misc#show () else handle#misc#hide ());
+
let factory = new GMenu.factory menubar in
let accel_group = factory#accel_group in
@@ -1480,7 +1572,7 @@ let main files =
| None -> ()
| (Some f) as fn -> load f
in
- ignore (load_m#connect#activate (do_if_not_computing load_f));
+ ignore (load_m#connect#activate (load_f));
(* File/Save Menu *)
let save_m = file_factory#add_item "_Save" ~key:GdkKeysyms._S in
@@ -1716,14 +1808,14 @@ let main files =
GtkText.View.Signals.paste_clipboard
with _ -> prerr_endline "EMIT PASTE FAILED")));
ignore (edit_f#add_separator ());
- let read_only_i = edit_f#add_check_item "_Read only" ~active:false
+ let read_only_i = edit_f#add_check_item "Expert" ~active:false
+ ~key:GdkKeysyms._Z
~callback:(fun b ->
- let v = get_current_view () in
- v.view#set_editable (not b);
- (out_some v.analyzed_view)#set_read_only b
+ GtkData.AccelGroup.save "tutu.l"
)
in
read_only_i#misc#set_state `INSENSITIVE;
+
let search_if = edit_f#add_item "Search _forward"
~key:GdkKeysyms._greater
in
@@ -1735,8 +1827,8 @@ let main files =
~callback:
(do_if_not_computing
(fun b ->
- let v =out_some (get_current_view ()).analyzed_view in
- v#complete_at_offset (v#get_insert#offset)
+ let v =out_some (get_current_view ()).analyzed_view
+ in v#complete_at_offset (v#get_insert#offset)
))
in
@@ -1760,37 +1852,64 @@ let main files =
if analyzed_view#is_active then
ignore (f analyzed_view)
else
- activate_input (notebook ())#current_page
+ begin
+ !flash_info "New proof started";
+ activate_input (notebook ())#current_page
+ end
in
let do_or_activate f = do_if_not_computing (do_or_activate f) in
- ignore (navigation_factory#add_item "_Break computations"
- ~key:GdkKeysyms._Break
- ~callback:(fun () -> break ()));
- ignore (navigation_factory#add_item "_Forward"
- ~key:GdkKeysyms._Down
- ~callback:(do_or_activate (fun a ->
- a#process_next_phrase true true)));
- ignore (navigation_factory#add_item "_Backward"
- ~key:GdkKeysyms._Up
- ~callback:(do_or_activate (fun a -> a#undo_last_step)));
- ignore (navigation_factory#add_item "_Forward to"
- ~key:GdkKeysyms._Right
- ~callback:(do_or_activate (fun a -> a#process_until_insert_or_error))
- );
- ignore (navigation_factory#add_item "_Backward to"
- ~key:GdkKeysyms._Left
- ~callback:(do_or_activate (fun a-> a#backtrack_to_insert))
- );
- ignore (navigation_factory#add_item "_Start"
- ~key:GdkKeysyms._Home
- ~callback:(do_or_activate (fun a -> a#reset_initial))
- );
- ignore (navigation_factory#add_item "_End"
- ~key:GdkKeysyms._End
- ~callback:(do_or_activate (fun a -> a#process_until_end_or_error))
- );
+ let add_to_menu_toolbar text ~tooltip ~key ~callback icon =
+ ignore (navigation_factory#add_item text ~key ~callback);
+ ignore (toolbar#insert_button
+ ~tooltip
+ ~text:tooltip
+ ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR icon)
+ ~callback
+ ())
+ in
+ add_to_menu_toolbar "_Interrupt computations"
+ ~tooltip:"Interrupt computations"
+ ~key:GdkKeysyms._Break
+ ~callback:break
+ `STOP
+ ;
+ add_to_menu_toolbar
+ "_Forward"
+ ~tooltip:"Forward"
+ ~key:GdkKeysyms._Down
+ ~callback:(do_or_activate (fun a -> a#process_next_phrase true true))
+ `GO_DOWN;
+ add_to_menu_toolbar "_Backward"
+ ~tooltip:"Backward"
+ ~key:GdkKeysyms._Up
+ ~callback:(do_or_activate (fun a -> a#undo_last_step))
+ `GO_UP;
+ add_to_menu_toolbar
+ "_Forward to"
+ ~tooltip:"Forward to"
+ ~key:GdkKeysyms._Right
+ ~callback:(do_or_activate (fun a -> a#process_until_insert_or_error))
+ `GOTO_LAST;
+ add_to_menu_toolbar
+ "_Backward to"
+ ~tooltip:"Backward to"
+ ~key:GdkKeysyms._Left
+ ~callback:(do_or_activate (fun a-> a#backtrack_to_insert))
+ `GOTO_FIRST;
+ add_to_menu_toolbar
+ "_Start"
+ ~tooltip:"Start"
+ ~key:GdkKeysyms._Home
+ ~callback:(do_or_activate (fun a -> a#reset_initial))
+ `GOTO_TOP;
+ add_to_menu_toolbar
+ "_End"
+ ~tooltip:"End"
+ ~key:GdkKeysyms._End
+ ~callback:(do_or_activate (fun a -> a#process_until_end_or_error))
+ `GOTO_BOTTOM;
(* Tactics Menu *)
let tactics_menu = factory#add_submenu "_Try Tactics" in
@@ -1846,6 +1965,17 @@ let main files =
~key:GdkKeysyms._v
~callback:(do_if_active( fun a -> a#insert_command "Progress Trivial.\n" "Trivial.\n" ))
);
+
+
+ ignore (toolbar#insert_button
+ ~tooltip:"Proof Wizzard"
+ ~text:"Wizzard"
+ ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_INFO)
+ ~callback:(do_if_active (fun a -> a#insert_commands
+ !current.automatic_tactics
+ ))
+ ());
+
ignore (tactics_factory#add_item "<Proof _Wizzard>"
~key:GdkKeysyms._dollar
~callback:(do_if_active (fun a -> a#insert_commands
@@ -1887,6 +2017,47 @@ let main files =
add_complex_template
("_Inductive __", "Inductive ident : :=\n | : .\n",
14, 5, Some GdkKeysyms._I);
+ add_complex_template("_Scheme __",
+"Scheme new_scheme := Induction for _ Sort _
+with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
+
+(* Template for Cases *)
+ let callback = (fun () ->
+ let w = get_current_word () in
+ try
+ let cases = Coq.make_cases w
+ in
+ let print c = function
+ | [x] -> fprintf c " | %s => _@\n" x
+ | x::l -> fprintf c " | (%s%a) => _@\n" x
+ (print_list (fun c s -> fprintf c " %s" s)) l
+ | [] -> assert false
+ in
+ let b = Buffer.create 1024 in
+ let fmt = formatter_of_buffer b in
+ fprintf fmt "@[Cases var of@\n%aend@]@."
+ (print_list print) cases;
+ let s = Buffer.contents b in
+ prerr_endline s;
+ let {view = view } = get_current_view () in
+ ignore (view#buffer#delete_selection ());
+ let m = view#buffer#create_mark
+ (view#buffer#get_iter `INSERT)
+ in
+ 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"
+ )
+ in
+ ignore (templates_factory#add_item "Cases ..."
+ ~key:GdkKeysyms._C
+ ~callback
+ );
+
let add_simple_template (factory: GMenu.menu GMenu.factory)
(menu_text, text) =
ignore (factory#add_item menu_text
@@ -2006,7 +2177,6 @@ let main files =
in
let _ = externals_factory#add_item "_Make Makefile" ~callback:coq_makefile_f
in
-
(* Configuration Menu *)
let reset_revert_timer () =
disconnect_revert_timer ();
@@ -2019,6 +2189,29 @@ let main files =
true))
in reset_revert_timer (); (* to enable statup preferences timer *)
+ let auto_save_f () =
+ Vector.iter
+ (function
+ {view = view ; analyzed_view = Some av} as full ->
+ (try
+ av#auto_save
+ with _ -> ())
+ | _ -> ()
+ )
+ input_views
+ in
+
+ let reset_auto_save_timer () =
+ disconnect_auto_save_timer ();
+ if !current.auto_save then
+ auto_save_timer := Some
+ (GMain.Timeout.add ~ms:!current.auto_save_delay
+ ~callback:
+ (fun () ->
+ do_if_not_computing (fun () -> auto_save_f ()) ();
+ true))
+ in reset_auto_save_timer (); (* to enable statup preferences timer *)
+
let configuration_menu = factory#add_submenu "Confi_guration" in
let configuration_factory = new GMenu.factory configuration_menu ~accel_group
in
@@ -2028,28 +2221,15 @@ let main files =
in
let save_prefs_m =
configuration_factory#add_item "_Save preferences"
- ~callback:(fun () -> save_pref !current)
- in
- font_selector :=
- Some (GWindow.font_selection_dialog
- ~title:"Select font..."
- ~modal:true ());
- let font_selector = out_some !font_selector in
- font_selector#selection#set_font_name (Pango.Font.to_string !current.text_font);
- font_selector#selection#set_preview_text
- "Lemma Truth: ∀ p:Prover, `p < Coq`. Proof. Auto with *. Save.";
- let customize_fonts_m =
- configuration_factory#add_item "Customize _fonts"
- ~callback:(fun () -> font_selector#present ())
+ ~callback:(fun () -> save_pref ())
in
-
let detach_menu = configuration_factory#add_item
"_Detach Scripting Window"
~callback:
(do_if_not_computing
(fun () ->
let nb = notebook () in
- if nb#misc#toplevel#get_oid=w#coerce#get_oid then
+ if nb#misc#toplevel#get_oid=w#coerce#get_oid then
begin
let nw = GWindow.window ~show:true () in
let parent = out_some nb#misc#parent in
@@ -2061,6 +2241,35 @@ let main files =
end
))
in
+ let detach_current_view = configuration_factory#add_item
+ "De_tach View"
+ ~callback:
+ (do_if_not_computing
+ (fun () ->
+ match get_current_view () with
+ | {view=v;analyzed_view=Some av} ->
+ let w = GWindow.window ~show:true
+ ~title:(match av#filename with
+ | None -> "*Unnamed*"
+ | Some f -> f)
+ ()
+ in
+ let sb = GBin.scrolled_window
+ ~packing:w#add ()
+ in
+ let nv = GText.view
+ ~buffer:v#buffer
+ ~packing:sb#add
+ ()
+ in
+ 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
@@ -2078,10 +2287,12 @@ let main files =
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
- (* Window layout *)
+ (* End of menu *)
+ (* The vertical Separator between Scripts and Goals *)
let hb = GPack.paned `HORIZONTAL ~border_width:3 ~packing:vbox#add () in
_notebook := Some (GPack.notebook ~scrollable:true
~packing:hb#add1
@@ -2101,13 +2312,13 @@ let main files =
let status_bar = GMisc.statusbar ~packing:(lower_hbox#pack ~expand:true) ()
in
let search_lbl = GMisc.label ~text:"Search:"
- ~show:true
+ ~show:false
~packing:(lower_hbox#pack ~expand:false) ()
in
let search_history = ref [] in
let search_input = GEdit.combo ~popdown_strings:!search_history
~use_arrows:`DEFAULT
- ~show:true
+ ~show:false
~packing:(lower_hbox#pack ~expand:false) ()
in
search_input#disable_activate ();
@@ -2128,16 +2339,21 @@ let main files =
let v = (get_current_view ()).view 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_input#entry#set_text "";
+ search_lbl#misc#hide ();
+ search_input#misc#hide ()
in
ignore (search_input#entry#connect#activate ~callback:end_search);
-
to_do_on_page_switch :=
(fun i ->
start_of_search := None;
ready_to_wrap_search:=false)::!to_do_on_page_switch;
+
let rec search_f () =
+ search_lbl#misc#show ();
+ search_input#misc#show ();
+
prerr_endline "search_f called";
if !start_of_search = None then
start_of_search :=
@@ -2147,8 +2363,9 @@ let main files =
let v = (get_current_view ()).view in
let iit = v#buffer#get_iter_at_mark `SEL_BOUND in
prerr_endline ("SELBOUND="^(string_of_int iit#offset));
- prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
-
+ prerr_endline ("INSERT="^(string_of_int
+ (v#buffer#get_iter_at_mark `INSERT)#offset));
+
(match
if !search_forward then iit#forward_search txt
else let npi = iit#forward_chars (Glib.Utf8.length txt) in
@@ -2164,33 +2381,33 @@ let main files =
| _,false ->
(iit#backward_search txt)
- with
- | None ->
- if !ready_to_wrap_search then begin
- ready_to_wrap_search := false;
- !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";
- ready_to_wrap_search := true
- end
- | 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));
-
- v#buffer#move_mark `SEL_BOUND start;
- v#buffer#move_mark `INSERT stop;
- prerr_endline "search: after 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));
- v#scroll_to_mark `SEL_BOUND
- )
- in
+ with
+ | None ->
+ if !ready_to_wrap_search then begin
+ ready_to_wrap_search := false;
+ !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";
+ ready_to_wrap_search := true
+ end
+ | 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));
+
+ v#buffer#move_mark `SEL_BOUND start;
+ v#buffer#move_mark `INSERT stop;
+ prerr_endline "search: after 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));
+ v#scroll_to_mark `SEL_BOUND
+ )
+ in
ignore (search_input#entry#event#connect#key_release
~callback:
(fun ev ->
@@ -2198,10 +2415,10 @@ let main files =
let v = (get_current_view ()).view in
(match !start_of_search with
| None ->
- prerr_endline "search_key_rel: Placing sel_bound";
+ prerr_endline "search_key_rel: Placing sel_bound";
v#buffer#move_mark
- `SEL_BOUND
- (v#buffer#get_iter_at_mark `INSERT)
+ `SEL_BOUND
+ (v#buffer#get_iter_at_mark `INSERT)
| Some mk -> let it = v#buffer#get_iter_at_mark
(`MARK mk) in
prerr_endline "search_key_rel: Placing cursor";
@@ -2212,9 +2429,9 @@ let main files =
v#coerce#misc#grab_focus ();
end;
false
- )) ;
+ ));
ignore (search_input#entry#connect#changed search_f);
-
+
ignore (search_if#connect#activate
~callback:(fun b ->
search_forward:= true;
@@ -2241,7 +2458,7 @@ let main files =
status := Some status_bar;
push_info := (fun s -> ignore (status_context#push s));
pop_info := (fun () -> status_context#pop ());
- flash_info := (fun s -> flash_context#flash ~delay:5000 s);
+ flash_info := (fun ?(delay=5000) s -> flash_context#flash ~delay s);
(* Location display *)
let l = GMisc.label
@@ -2249,7 +2466,7 @@ let main files =
~packing:lower_hbox#pack () in
l#coerce#misc#set_name "location";
set_location := l#set_text;
- load_pref current;
+
(* Progress Bar *)
pulse :=
(GRange.progress_bar ~text:"CoqIde started" ~pulse_step:0.2 ~packing:lower_hbox#pack ())#pulse;
@@ -2292,23 +2509,14 @@ let main files =
false)) e;
false)
in
- ignore (font_selector#cancel_button#connect#released
- ~callback:font_selector#misc#hide);
- ignore (font_selector#ok_button#connect#released
- ~callback:(fun () ->
- (match font_selector#selection#font_name with
- | None -> ()
- | Some n ->
- let pango_font = Pango.Font.from_string n in
- tv2#misc#modify_font pango_font;
- tv3#misc#modify_font pango_font;
- Vector.iter
- (fun {view=view} -> view#misc#modify_font pango_font)
- input_views;
- !current.text_font <- pango_font
- );
- font_selector#misc#hide ()));
-
+ 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;
+ );
(try
let image = Filename.concat lib_ide "coq.png" in
let startup_image = GdkPixbuf.from_file image in
@@ -2335,7 +2543,7 @@ let main files =
w#show ();
message_view := Some tv3;
proof_view := Some tv2;
- let view = create_input_tab "*Unamed Buffer*" in
+ let view = create_input_tab "*Unnamed Buffer*" in
let index = add_input_view {view = view;
analyzed_view = None;
}
@@ -2348,6 +2556,15 @@ let main files =
tv3#misc#modify_font !current.text_font;
ignore (about_m#connect#activate
~callback:(fun () -> tv3#buffer#set_text "by Benjamin Monate"));
+ ignore (faq_m#connect#activate
+ ~callback:(fun () ->
+ load (Filename.concat lib_ide "FAQ")));
+
+ 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
@@ -2357,7 +2574,9 @@ let main files =
old_h := h;
old_w := w;
hb#set_position (w/2);
- hb2#set_position (h*4/5)
+ hb2#set_position (h*4/5);
+ !current.window_height <- h;
+ !current.window_width <- w;
end
));
ignore(nb#connect#switch_page
@@ -2374,7 +2593,7 @@ let main files =
false));
List.iter load files;
if List.length files >=1 then activate_input 1
-
+;;
let start () =
let files = Coq.init () in
diff --git a/ide/extract_index.mll b/ide/extract_index.mll
index 1eb2c13d6..f3fbe0752 100644
--- a/ide/extract_index.mll
+++ b/ide/extract_index.mll
@@ -1,3 +1,12 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
{
open Lexing
diff --git a/ide/find_phrase.mll b/ide/find_phrase.mll
index 16d1cd83e..ed124461f 100644
--- a/ide/find_phrase.mll
+++ b/ide/find_phrase.mll
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
{
exception Lex_error of string
let length = ref 0
diff --git a/ide/highlight.mll b/ide/highlight.mll
index c751ff3f2..cdfc51f98 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
{
open Lexing
@@ -33,14 +43,14 @@ let keyword =
"Section" | "Show" | "Syntactic" | "Syntax" | "Tactic" |
"Unset" |
("Set" space+ "Implicit" space+ "Arguments") |
- ("Implicit" space+ "Arguments" space+ ("On" | "Off"))
+ ("Implicit" space+ "Arguments" space+ ("On" | "Off")) | "Cases"
let declaration =
"Lemma" | "Axiom" | "CoFixpoint" | "Definition" |
("Tactic" space+ "Definition") |
"Fixpoint" | "Hypothesis" |
"Inductive" | "Parameter" | "Remark" | "Theorem" |
- "Variable" | "Variables"
+ "Variable" | "Variables"
rule next_order = parse
| "(*" { comment_start := lexeme_start lexbuf; comment lexbuf }
@@ -73,7 +83,6 @@ and comment = parse
let lb = Lexing.from_string s in
try
while true do
- (* process_pending (); This is VERY DANGEROUS *)
let b,e,o=next_order lb in
let b,e = convert_pos b,convert_pos e in
let start = input_buffer#get_iter_at_char (offset + b) in
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index f0f54650e..671b12410 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -1,9 +1,18 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
open Preferences
exception Forbidden
-
let debug = Options.debug
let prerr_endline s =
@@ -116,8 +125,7 @@ let url_for_keyword =
let browse_keyword text =
- try
- let u = url_for_keyword text in browse (!current.doc_url ^ u)
+ try let u = url_for_keyword text in browse (!current.doc_url ^ u)
with _ -> ()
let my_stat f = try Some (Unix.stat f) with _ -> None
@@ -127,6 +135,11 @@ let disconnect_revert_timer () = match !revert_timer with
| None -> ()
| Some id -> GMain.Timeout.remove id; revert_timer := None
+let auto_save_timer = ref None
+let disconnect_auto_save_timer () = match !auto_save_timer with
+ | None -> ()
+ | Some id -> GMain.Timeout.remove id; auto_save_timer := None
+
let highlight_timer = ref None
let set_highlight_timer f =
match !highlight_timer with
@@ -202,3 +215,12 @@ let async =
if Sys.os_type <> "Unix" then GtkThread.async else (fun x -> x)
+let stock_to_widget ?(size=`DIALOG) s =
+ let img = GMisc.image ()
+ in img#set_stock ~size s ;
+ img#coerce
+
+let rec print_list print fmt = function
+ | [] -> ()
+ | [x] -> print fmt x
+ | x :: r -> print fmt x; print_list print fmt r
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 10071161b..c6a1aabdd 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
open Configwin
open Printf
open Util
@@ -67,9 +77,63 @@ type pref =
mutable doc_url : string;
mutable library_url : string;
+
+ mutable show_toolbar : bool;
+ mutable window_width : int;
+ mutable window_height :int;
+
}
-let save_pref p =
+let (current:pref ref) =
+ ref {
+ cmd_coqc = "coqc";
+ cmd_make = "make";
+ cmd_coqmakefile = "coq_makefile -o Makefile *.v";
+ cmd_coqdoc = "coqdoc -q -g";
+ cmd_print = "lpr";
+
+ global_auto_revert = false;
+ global_auto_revert_delay = 10000;
+
+ auto_save = false;
+ auto_save_delay = 10000;
+ auto_save_name = "#","#";
+
+ automatic_tactics = ["Progress Trivial.","Trivial.";
+ "Progress Auto.","Auto.";
+ "Tauto.","Tauto.";
+ "Omega.","Omega.";
+ "Progress Auto with *.","Auto with *.";
+ "Progress Intuition.","Intuition.";
+ ];
+
+ modifier_for_navigation = [`CONTROL; `MOD1];
+ modifier_for_templates = [`MOD4];
+ modifier_for_tactics = [`CONTROL; `MOD1];
+ modifiers_valid = [`SHIFT; `CONTROL; `MOD1; `MOD4];
+
+
+ cmd_browse = "netscape -remote \"OpenURL(", ")\"";
+
+ text_font = Pango.Font.from_string "Monospace 12";
+
+ doc_url = "http://coq.inria.fr/doc/";
+ library_url = "http://coq.inria.fr/library/";
+
+ show_toolbar = true;
+ window_width = 800;
+ window_height = 600;
+ }
+
+
+let change_font = ref (fun f -> ())
+
+let show_toolbar = ref (fun x -> ())
+
+let resize_window = ref (fun () -> ())
+
+let save_pref () =
+ let p = !current in
try
let add = Stringmap.add in
let (++) x f = f x in
@@ -101,51 +165,18 @@ let save_pref p =
add "doc_url" [p.doc_url] ++
add "library_url" [p.library_url] ++
+ add "show_toolbar" [string_of_bool p.show_toolbar] ++
+ add "window_height" [string_of_int p.window_height] ++
+ add "window_width" [string_of_int p.window_width] ++
Config_lexer.print_file pref_file
with _ -> prerr_endline "Could not save preferences."
-let (current:pref ref) =
- ref {
- cmd_coqc = "coqc";
- cmd_make = "make";
- cmd_coqmakefile = "coq_makefile -o Makefile *.v";
- cmd_coqdoc = "coqdoc -q -g";
- cmd_print = "lpr";
-
- global_auto_revert = false;
- global_auto_revert_delay = 10000;
-
- auto_save = false;
- auto_save_delay = 10000;
- auto_save_name = "#","#";
-
- automatic_tactics = ["Progress Trivial.\n","Trivial.\n";
- "Progress Auto.\n","Auto.\n";
- "Tauto.\n","Tauto.\n";
- "Omega.\n","Omega.\n";
- "Progress Auto with *.\n","Auto with *.\n";
- "Progress Intuition.\n","Intuition.\n";
- ];
-
- modifier_for_navigation = [`CONTROL; `MOD1];
- modifier_for_templates = [`MOD4];
- modifier_for_tactics = [`CONTROL; `MOD1];
- modifiers_valid = [`SHIFT; `CONTROL; `MOD1; `MOD4];
-
-
- cmd_browse = "netscape -remote \"OpenURL(", ")\"";
-
- text_font = Pango.Font.from_string "Monospace 12";
-
- doc_url = "http://coq.inria.fr/doc/";
- library_url = "http://coq.inria.fr/library/";
- }
-
-let load_pref p =
+let load_pref () =
+ let p = !current in
try
let m = Config_lexer.load_file pref_file in
- let np = { !p with cmd_coqc = !p.cmd_coqc } in
+ let np = { p with cmd_coqc = p.cmd_coqc } in
let set k f = try let v = Stringmap.find k m in f v with _ -> () in
let set_hd k f = set k (fun v -> f (List.hd v)) in
let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
@@ -181,10 +212,15 @@ let load_pref p =
set_hd "text_font" (fun v -> np.text_font <- Pango.Font.from_string v);
set_hd "doc_url" (fun v -> np.doc_url <- v);
set_hd "library_url" (fun v -> np.library_url <- v);
+ set_bool "show_toolbar" (fun v -> np.show_toolbar <- v);
+ set_int "window_width" (fun v -> np.window_width <- v);
+ set_int "window_height" (fun v -> np.window_height <- v);
+
current := np
with e ->
prerr_endline ("Could not load preferences ("^
(Printexc.to_string e)^").")
+
let configure () =
let cmd_coqc =
@@ -198,6 +234,48 @@ let configure () =
let cmd_print = string ~f:(fun s -> !current.cmd_print <- s)
"Print ps" !current.cmd_print in
+ let config_font =
+ let box = GPack.hbox () in
+ let w = GMisc.font_selection () in
+ w#set_preview_text
+ "Lemma Truth: ∀ p:Prover, `p < Coq`. Proof. Auto with *. Save.";
+ box#pack w#coerce;
+ ignore (w#misc#connect#realize
+ ~callback:(fun () -> w#set_font_name
+ (Pango.Font.to_string !current.text_font)));
+ custom
+ ~label:"Fonts for text"
+ box
+ (fun () -> match w#font_name with
+ | None -> ()
+ | Some fd -> !current.text_font <- (Pango.Font.from_string fd) ; !change_font !current.text_font)
+ true
+ in
+ let show_toolbar =
+ bool
+ ~f:(fun s ->
+ !current.show_toolbar <- s;
+ !show_toolbar s)
+ "Show toolbar" !current.show_toolbar
+ in
+ let window_height =
+ string
+ ~f:(fun s -> !current.window_height <- (try int_of_string s with _ -> 600);
+ !resize_window ();
+ )
+ "Window height"
+ (string_of_int !current.window_height)
+ in
+ let window_width =
+ string
+ ~f:(fun s -> !current.window_width <-
+ (try int_of_string s with _ -> 800))
+ "Window width"
+ (string_of_int !current.window_width)
+ in
+
+ let config_appearance = [show_toolbar; window_width; window_height] in
+
let global_auto_revert =
bool
~f:(fun s -> !current.global_auto_revert <- s)
@@ -211,6 +289,19 @@ let configure () =
(string_of_int !current.global_auto_revert_delay)
in
+ let auto_save =
+ bool
+ ~f:(fun s -> !current.auto_save <- s)
+ "Enable auto save" !current.auto_save
+ in
+ let auto_save_delay =
+ string
+ ~f:(fun s -> !current.auto_save_delay <-
+ (try int_of_string s with _ -> 10000))
+ "Auto save delay (ms)"
+ (string_of_int !current.auto_save_delay)
+ in
+
let modifier_for_tactics =
modifiers
~allow:!current.modifiers_valid
@@ -238,6 +329,12 @@ let configure () =
"Allowed modifiers"
!current.modifiers_valid
in
+ let mod_msg =
+ string
+ "Needs restart to apply!"
+ ~editable:false
+ ""
+ in
let cmd_browse =
string
@@ -265,27 +362,35 @@ let configure () =
let automatic_tactics =
let box = GPack.hbox () in
- let w = Editable_cells.create !current.automatic_tactics in
- box#pack w#coerce;
+ let (w,get_data) = Editable_cells.create !current.automatic_tactics in
+ box#add w#coerce;
custom
- ~label:"Wizzard tactics to try in order (WORK IN PROGRESS)"
+ ~label:"Wizzard tactics to try in order"
box
- (fun () -> ())
+ (fun () -> let d = get_data () in !current.automatic_tactics <- d)
true
in
let cmds =
- [Section("Commands",
+ [Section("Fonts",
+ [config_font]);
+ Section("Appearance",
+ config_appearance);
+ Section("Commands",
[cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print]);
Section("Files",
- [global_auto_revert;global_auto_revert_delay]);
+ [global_auto_revert;global_auto_revert_delay;
+ auto_save; auto_save_delay; (* auto_save_name*)
+ ]);
Section("Browser",
[cmd_browse;doc_url;library_url]);
Section("Tactics Wizzard",
[automatic_tactics]);
- Section("Shortcuts(need restart)",
- [modifiers_valid; modifier_for_tactics;modifier_for_templates; modifier_for_navigation])]
+ Section("Shortcuts",
+ [modifiers_valid; modifier_for_tactics;
+ modifier_for_templates; modifier_for_navigation;mod_msg])]
in
- match edit "Customizations" cmds
- with | Return_apply | Return_ok -> save_pref !current
+ match edit ~width:500 "Customizations" cmds
+ with
+ | Return_apply | Return_ok -> save_pref ()
| Return_cancel -> ()
diff --git a/ide/undo.ml b/ide/undo.ml
index e8fc305c7..10d5e0ab5 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
open GText
open Ideutils
type action =
diff --git a/ide/undo.mli b/ide/undo.mli
index 0aae49e79..64812a53e 100644
--- a/ide/undo.mli
+++ b/ide/undo.mli
@@ -1,3 +1,13 @@
+(***********************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+(* \VV/ *************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(***********************************************************************)
+
+(* $Id$ *)
+
(* An undoable view class *)
class undoable_view : Gtk.textview Gtk.obj ->
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 04d7c05ed..d01b83003 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1059,16 +1059,19 @@ let edit ?(with_apply=true)
let hbox_buttons = GPack.hbox ~packing: (vbox#pack ~expand: false ~padding: 4) () in
let bApply = GButton.button
- ~label: Configwin_messages.mApply
- ()
+ ~stock:`APPLY
+ ~label: Configwin_messages.mApply
+ ()
in
if with_apply then hbox_buttons#pack ~expand: true ~padding: 3 bApply#coerce;
let bOk = GButton.button
+ ~stock:`OK
~label: Configwin_messages.mOk
~packing: (hbox_buttons#pack ~expand: true ~padding: 3)
()
in
let bCancel = GButton.button
+ ~stock:`CANCEL
~label: Configwin_messages.mCancel
~packing: (hbox_buttons#pack ~expand: true ~padding: 3)
()
@@ -1091,6 +1094,9 @@ let edit ?(with_apply=true)
let f_cancel () = window#destroy () in
let _ = bCancel#connect#clicked f_cancel in
+ let _ = window#event#connect#key_press ~callback:
+ (fun k -> if GdkEvent.Key.keyval k = GdkKeysyms._Escape then f_cancel ();false)
+ in
let _ = window#show () in
GMain.Main.main () ;
!return
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index 1fd15f77a..20111bf84 100644
--- a/ide/utils/editable_cells.ml
+++ b/ide/utils/editable_cells.ml
@@ -3,11 +3,17 @@ open Gobject
let create l =
let hbox = GPack.hbox () in
+ let scw = GBin.scrolled_window
+ ~hpolicy:`AUTOMATIC
+ ~vpolicy:`AUTOMATIC
+ ~packing:(hbox#pack ~expand:true) () in
+
let columns = new GTree.column_list in
let command_col = columns#add Data.string in
let coq_col = columns#add Data.string in
let store = GTree.list_store columns
in
+
(* populate the store *)
let _ = List.iter (fun (x,y) ->
let row = store#append () in
@@ -15,25 +21,97 @@ let create l =
store#set ~row ~column:coq_col y)
l
in
- let view = GTree.view ~model:store ~packing:hbox#pack () in
-
- let renderer = GTree.cell_renderer_text () in
- GtkText.Tag.set_property renderer (`EDITABLE true);
+ let view = GTree.view ~model:store ~packing:scw#add_with_viewport () in
+
+ (* Alternate colors for the rows *)
+ view#set_rules_hint true;
+
+ let renderer_comm = GTree.cell_renderer_text () in
+ ignore (GtkSignal.connect renderer_comm
+ ~sgn:GtkTree.CellRendererText.Signals.edited
+ ~callback:(fun (path:Gtk.tree_path) (s:string) ->
+ store#set
+ ~row:(store#get_iter path)
+ ~column:command_col s));
+ GtkText.Tag.set_property renderer_comm (`EDITABLE true);
let first =
GTree.view_column ~title:"Coq Command to try"
- ~renderer:(renderer,["text",command_col])
+ ~renderer:(renderer_comm,["text",command_col])
()
in ignore (view#append_column first);
+
+ let renderer_coq = GTree.cell_renderer_text () in
+ ignore (GtkSignal.connect renderer_coq ~sgn:GtkTree.CellRendererText.Signals.edited
+ ~callback:(fun (path:Gtk.tree_path) (s:string) ->
+ store#set
+ ~row:(store#get_iter path)
+ ~column:coq_col s));
+ GtkText.Tag.set_property renderer_coq (`EDITABLE true);
let second =
GTree.view_column ~title:"Coq Command to insert"
- ~renderer:(renderer,["text",coq_col])
+ ~renderer:(renderer_coq,["text",coq_col])
()
in ignore (view#append_column second);
- let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack () in
- let up = GButton.button ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in
- let down = GButton.button ~label:"Down" ~packing:(vbox#pack ~expand:true ~fill:false) () in
- let add = GButton.button ~label:"Add" ~packing:(vbox#pack ~expand:true ~fill:false) () in
- let remove = GButton.button ~label:"Remove" ~packing:(vbox#pack ~expand:true ~fill:false) () in
- hbox
+ let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD ()
+ in
+ let up = GButton.button ~stock:`GO_UP ~label:"Up" ~packing:(vbox#pack ~expand:true ~fill:false) () in
+ let down = GButton.button
+ ~stock:`GO_DOWN
+ ~label:"Down"
+ ~packing:(vbox#pack ~expand:true ~fill:false) ()
+ in
+ let add = GButton.button ~stock:`ADD
+ ~label:"Add"
+ ~packing:(vbox#pack ~expand:true ~fill:false)
+ ()
+ in
+ let remove = GButton.button ~stock:`REMOVE
+ ~label:"Remove"
+ ~packing:(vbox#pack ~expand:true ~fill:false) ()
+ in
+
+ ignore (add#connect#clicked
+ ~callback:(fun b ->
+ let n = store#append () in
+ view#selection#select_iter n));
+ ignore (remove#connect#clicked
+ ~callback:(fun b -> match view#selection#get_selected_rows with
+ | [] -> ()
+ | path::_ ->
+ let iter = store#get_iter path in
+ ignore (store#remove iter);
+ ));
+ ignore (up#connect#clicked
+ ~callback:(fun b ->
+ match view#selection#get_selected_rows with
+ | [] -> ()
+ | path::_ ->
+ let iter = store#get_iter path in
+ GtkTree.TreePath.prev path;
+ let upiter = store#get_iter path in
+ ignore (store#swap iter upiter);
+ ));
+ ignore (down#connect#clicked
+ ~callback:(fun b ->
+ match view#selection#get_selected_rows with
+ | [] -> ()
+ | path::_ ->
+ let iter = store#get_iter path in
+ GtkTree.TreePath.next path;
+ try let upiter = store#get_iter path in
+ ignore (store#swap iter upiter)
+ with _ -> ()
+ ));
+ let get_data () =
+ let start_path = GtkTree.TreePath.from_string "0" in
+ let start_iter = store#get_iter start_path in
+ let rec all acc =
+ let new_acc = (store#get ~row:start_iter ~column:command_col,
+ store#get ~row:start_iter ~column:coq_col)::acc
+ in
+ if store#iter_next start_iter then all new_acc else List.rev new_acc
+ in all []
+ in
+ (hbox,get_data)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 21:40:33 +0000