aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/command_windows.ml64
-rw-r--r--ide/config_lexer.mll8
-rw-r--r--ide/coq.ml124
-rw-r--r--ide/coq.mli8
-rw-r--r--ide/coq_commands.ml16
-rw-r--r--ide/coqide.ml1276
-rw-r--r--ide/coqide.mli2
-rw-r--r--ide/gtk_parsing.ml38
-rw-r--r--ide/highlight.mll54
-rw-r--r--ide/ideutils.ml122
-rw-r--r--ide/preferences.ml254
-rw-r--r--ide/tags.ml2
-rw-r--r--ide/typed_notebook.ml2
-rw-r--r--ide/undo.ml66
-rw-r--r--ide/undo_lablgtk_ge212.mli2
-rw-r--r--ide/undo_lablgtk_ge26.mli2
-rw-r--r--ide/undo_lablgtk_lt26.mli2
-rw-r--r--ide/utf8_convert.mll10
-rw-r--r--ide/utils/configwin.mli2
-rw-r--r--ide/utils/configwin_ihm.ml24
-rw-r--r--ide/utils/configwin_keys.ml50
-rw-r--r--ide/utils/configwin_types.ml6
-rw-r--r--ide/utils/editable_cells.ml92
-rw-r--r--ide/utils/okey.mli64
24 files changed, 1145 insertions, 1145 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index ab65fa143..ee07b3fb8 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -8,9 +8,9 @@
(* $Id$ *)
-class command_window () =
-(* let window = GWindow.window
- ~allow_grow:true ~allow_shrink:true
+class command_window () =
+(* let window = GWindow.window
+ ~allow_grow:true ~allow_shrink:true
~width:500 ~height:250
~position:`CENTER
~title:"CoqIde queries" ~show:false ()
@@ -19,23 +19,23 @@ class command_window () =
let _ = frame#misc#hide () in
let _ = GtkData.AccelGroup.create () in
let hbox = GPack.hbox ~homogeneous:false ~packing:frame#add () in
- let toolbar = GButton.toolbar
- ~orientation:`VERTICAL
+ let toolbar = GButton.toolbar
+ ~orientation:`VERTICAL
~style:`ICONS
- ~tooltips:true
- ~packing:(hbox#pack
+ ~tooltips:true
+ ~packing:(hbox#pack
~expand:false
~fill:false)
()
in
- let notebook = GPack.notebook ~scrollable:true
- ~packing:(hbox#pack
+ let notebook = GPack.notebook ~scrollable:true
+ ~packing:(hbox#pack
~expand:true
~fill:true
- )
+ )
()
in
- let _ =
+ let _ =
toolbar#insert_button
~tooltip:"Hide Commands Pane"
~text:"Hide Pane"
@@ -43,7 +43,7 @@ class command_window () =
~callback:frame#misc#hide
()
in
- let new_page_menu =
+ let new_page_menu =
toolbar#insert_button
~tooltip:"New Page"
~text:"New Page"
@@ -51,7 +51,7 @@ class command_window () =
()
in
- let _ =
+ let _ =
toolbar#insert_button
~tooltip:"Delete Page"
~text:"Delete Page"
@@ -65,10 +65,10 @@ object(self)
val new_page_menu = new_page_menu
val notebook = notebook
- method frame = frame
+ method frame = frame
method new_command ?command ?term () =
let appendp x = ignore (notebook#append_page x) in
- let frame = GBin.frame
+ let frame = GBin.frame
~shadow_type:`ETCHED_OUT
~packing:appendp
()
@@ -84,15 +84,15 @@ object(self)
()
in
combo#disable_activate ();
- let on_activate c () =
- if List.mem combo#entry#text Coq_commands.state_preserving then c ()
- else prerr_endline "Not a state preserving command"
+ let on_activate c () =
+ if List.mem combo#entry#text Coq_commands.state_preserving then c ()
+ else prerr_endline "Not a state preserving command"
in
let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in
entry#misc#set_can_default true;
let r_bin =
- GBin.scrolled_window
- ~vpolicy:`AUTOMATIC
+ GBin.scrolled_window
+ ~vpolicy:`AUTOMATIC
~hpolicy:`AUTOMATIC
~packing:(vbox#pack ~fill:true ~expand:true) () in
let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in
@@ -101,13 +101,13 @@ object(self)
result#set_editable false;
let callback () =
let com = combo#entry#text in
- let phrase =
+ let phrase =
if String.get com (String.length com - 1) = '.'
- then com ^ " " else com ^ " " ^ entry#text ^" . "
+ then com ^ " " else com ^ " " ^ entry#text ^" . "
in
try
ignore(Coq.interp false phrase);
- result#buffer#set_text
+ result#buffer#set_text
("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ())
with e ->
let (s,loc) = Coq.process_exn e in
@@ -117,16 +117,16 @@ object(self)
ignore (combo#entry#connect#activate ~callback:(on_activate callback));
ignore (ok_b#connect#clicked ~callback:(on_activate callback));
- begin match command,term with
+ begin match command,term with
| None,None -> ()
- | Some c, None ->
+ | Some c, None ->
combo#entry#set_text c;
-
- | Some c, Some t ->
+
+ | Some c, Some t ->
combo#entry#set_text c;
entry#set_text t
-
- | None , Some t ->
+
+ | None , Some t ->
entry#set_text t
end;
on_activate callback ();
@@ -134,9 +134,9 @@ object(self)
entry#misc#grab_default ();
ignore (entry#connect#activate ~callback);
ignore (combo#entry#connect#activate ~callback);
- self#frame#misc#show ()
+ self#frame#misc#show ()
- initializer
+ initializer
ignore (new_page_menu#connect#clicked self#new_command);
(* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*)
end
@@ -145,6 +145,6 @@ let command_window = ref None
let main () = command_window := Some (new command_window ())
-let command_window () = match !command_window with
+let command_window () = match !command_window with
| None -> failwith "No command window."
| Some c -> c
diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll
index 8e04331c1..97aeb2f5a 100644
--- a/ide/config_lexer.mll
+++ b/ide/config_lexer.mll
@@ -28,19 +28,19 @@ rule token = parse
| '#' [^ '\n']* { token lexbuf }
| ident { IDENT (lexeme lexbuf) }
| '=' { EQUAL }
- | '"' { Buffer.reset string_buffer;
+ | '"' { Buffer.reset string_buffer;
Buffer.add_char string_buffer '"';
string lexbuf;
let s = Buffer.contents string_buffer in
STRING (Scanf.sscanf s "%S" (fun s -> s)) }
| _ { let c = lexeme_start lexbuf in
- eprintf ".coqiderc: invalid character (%d)\n@." c;
+ eprintf ".coqiderc: invalid character (%d)\n@." c;
token lexbuf }
| eof { EOF }
and string = parse
| '"' { Buffer.add_char string_buffer '"' }
- | '\\' '"' | _
+ | '\\' '"' | _
{ Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf }
| eof { eprintf ".coqiderc: unterminated string\n@." }
@@ -60,7 +60,7 @@ and string = parse
| [] -> ()
| s :: sl -> fprintf fmt "%S@ %a" s print_list sl
in
- Stringmap.iter
+ Stringmap.iter
(fun k s -> fprintf fmt "@[<hov 2>%s = %a@]@\n" k print_list s) m;
fprintf fmt "@.";
close_out c
diff --git a/ide/coq.ml b/ide/coq.ml
index 4fd48a306..a567fb4f5 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -30,16 +30,16 @@ let prerr_endline s = if !debug then prerr_endline s else ()
let output = ref (Format.formatter_of_out_channel stdout)
-let msg m =
+let msg m =
let b = Buffer.create 103 in
Pp.msg_with (Format.formatter_of_buffer b) m;
Buffer.contents b
-let msgnl m =
+let msgnl m =
(msg m)^"\n"
-let init () =
- (* To hide goal in lower window.
+let init () =
+ (* To hide goal in lower window.
Problem: should not hide "xx is assumed"
messages *)
(**)
@@ -70,7 +70,7 @@ let short_version () =
let version () =
let (ver,date) = get_version_date () in
- Printf.sprintf
+ Printf.sprintf
"The Coq Proof Assistant, version %s (%s)\
\nArchitecture %s running %s operating system\
\nGtk version is %s\
@@ -79,14 +79,14 @@ let version () =
ver date
Coq_config.arch Sys.os_type
(let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
- (if Mltop.is_native then "native" else "bytecode")
- (if Coq_config.best="opt" then "native" else "bytecode")
+ (if Mltop.is_native then "native" else "bytecode")
+ (if Coq_config.best="opt" then "native" else "bytecode")
-let is_in_coq_lib dir =
+let is_in_coq_lib dir =
prerr_endline ("Is it a coq theory ? : "^dir);
let is_same_file = same_file dir in
- List.exists
- (fun s ->
+ List.exists
+ (fun s ->
let fdir =
Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in
prerr_endline (" Comparing to: "^fdir);
@@ -97,19 +97,19 @@ let is_in_coq_lib dir =
let is_in_loadpath dir =
Library.is_in_load_paths (System.physical_path_of_string dir)
-let is_in_coq_path f =
- try
+let is_in_coq_path f =
+ try
let base = Filename.chop_extension (Filename.basename f) in
let _ = Library.locate_qualified_library false
- (Libnames.make_qualid Names.empty_dirpath
+ (Libnames.make_qualid Names.empty_dirpath
(Names.id_of_string base)) in
prerr_endline (f ^ " is in coq path");
true
- with _ ->
+ with _ ->
prerr_endline (f ^ " is NOT in coq path");
- false
+ false
-let is_in_proof_mode () =
+let is_in_proof_mode () =
match Decl_mode.get_current_mode () with
Decl_mode.Mode_none -> false
| _ -> true
@@ -347,13 +347,13 @@ type reset_info = reset_mark * undo_info * bool ref
let compute_reset_info () =
(match Lib.has_top_frozen_state () with
- | Some st ->
+ | Some st ->
prerr_endline ("On top of state "^Libnames.string_of_path (fst st));
st
- | None ->
+ | None ->
failwith "FATAL ERROR: NO RESET"), undo_info(), ref true
-let reset_initial () =
+let reset_initial () =
prerr_endline "Reset initial called"; flush stderr;
Vernacentries.abort_refine Lib.reset_initial ()
@@ -361,14 +361,14 @@ let reset_to st =
prerr_endline ("Reset called with state "^(Libnames.string_of_path (fst st)));
Lib.reset_to_state st
-let reset_to_mod id =
- prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id));
+let reset_to_mod id =
+ prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id));
Lib.reset_mod (Util.dummy_loc,id)
let raw_interp s =
Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s))
-let interp_with_options verbosely options s =
+let interp_with_options verbosely options s =
prerr_endline "Starting interp...";
prerr_endline s;
let pa = Pcoq.Gram.parsable (Stream.of_string s) in
@@ -376,7 +376,7 @@ let interp_with_options verbosely options s =
(* Temporary hack to make coqide.byte work (WTF???) - now with less screen
* pollution *)
Pervasives.prerr_string " \r"; Pervasives.flush stderr;
- match pe with
+ match pe with
| None -> assert false
| Some((loc,vernac) as last) ->
if is_vernac_debug_command vernac then
@@ -385,7 +385,7 @@ let interp_with_options verbosely options s =
user_error_loc loc (str "Use CoqIDE navigation instead");
if is_vernac_known_option_command vernac then
user_error_loc loc (str "Use CoqIDE display menu instead");
- if is_vernac_query_command vernac then
+ if is_vernac_query_command vernac then
flash_info
"Warning: query commands should not be inserted in scripts";
if not (is_vernac_goal_printing_command vernac) then
@@ -402,12 +402,12 @@ let interp_with_options verbosely options s =
let interp verbosely phrase =
interp_with_options verbosely (make_option_commands ()) phrase
-let interp_and_replace s =
+let interp_and_replace s =
let result = interp false s in
let msg = read_stdout () in
result,msg
-type tried_tactic =
+type tried_tactic =
| Interrupted
| Success of int (* nb of goals after *)
| Failed
@@ -424,7 +424,7 @@ let print_toplevel_error exc =
match exc with
| DuringCommandInterp (loc,ie) ->
if loc = dummy_loc then (None,ie) else (Some loc, ie)
- | _ -> (None, exc)
+ | _ -> (None, exc)
in
let (loc,exc) =
match exc with
@@ -434,19 +434,19 @@ let print_toplevel_error exc =
in
match exc with
| End_of_input -> str "Please report: End of input",None
- | Vernacexpr.ProtectedLoop ->
+ | Vernacexpr.ProtectedLoop ->
str "ProtectedLoop not allowed by coqide!",None
| Vernacexpr.Drop -> str "Drop is not allowed by coqide!",None
| Vernacexpr.Quit -> str "Quit is not allowed by coqide! Use menus.",None
- | _ ->
- (try Cerrors.explain_exn exc with e ->
+ | _ ->
+ (try Cerrors.explain_exn exc with e ->
str "Failed to explain error. This is an internal Coq error. Please report.\n"
++ str (Printexc.to_string e)),
(if is_pervasive_exn exc then None else loc)
let process_exn e = let s,loc= print_toplevel_error e in (msgnl s,loc)
-let interp_last last =
+let interp_last last =
prerr_string "*";
try
vernac_com (States.with_heavy_rollback Vernacentries.interp) last;
@@ -457,7 +457,7 @@ let interp_last last =
type hyp = env * evar_map *
- ((identifier * string) * constr option * constr) *
+ ((identifier * string) * constr option * constr) *
(string * string)
type concl = env * evar_map * constr * string
type meta = env * evar_map * string
@@ -465,7 +465,7 @@ type goal = hyp list * concl
let prepare_hyp sigma env ((i,c,d) as a) =
env, sigma,
- ((i,string_of_id i),c,d),
+ ((i,string_of_id i),c,d),
(msg (pr_var_decl env a), msg (pr_ltype_env env d))
let prepare_hyps sigma env =
@@ -473,7 +473,7 @@ let prepare_hyps sigma env =
let hyps =
fold_named_context
(fun env d acc -> let hyp = prepare_hyp sigma env d in hyp :: acc)
- env ~init:[]
+ env ~init:[]
in
List.rev hyps
@@ -496,9 +496,9 @@ let get_current_pm_goal () =
let gl = sig_it gls in
prepare_goal sigma gl
-let get_current_goals () =
+let get_current_goals () =
let pfts = get_pftreestate () in
- let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
+ let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
let sigma = Tacmach.evc_of_pftreestate pfts in
List.map (prepare_goal sigma) gls
@@ -508,16 +508,16 @@ let print_no_goal () =
let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
[("clear "^ident),("clear "^ident^".");
-
+
("apply "^ident),
("apply "^ident^".");
-
+
("exact "^ident),
("exact "^ident^".");
("generalize "^ident),
("generalize "^ident^".");
-
+
("absurd <"^ident^">"),
("absurd "^
pr_ast
@@ -528,34 +528,34 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) =
"injection "^ident, "injection "^ident^"." ]
else
[]) @
-
+
(let _,t = splay_prod env sigma ast in
- if is_equality_type t then
+ if is_equality_type t then
[ "rewrite "^ident, "rewrite "^ident^".";
"rewrite <- "^ident, "rewrite <- "^ident^"." ]
else
[]) @
-
+
[("elim "^ident),
("elim "^ident^".");
-
+
("inversion "^ident),
("inversion "^ident^".");
-
+
("inversion clear "^ident),
- ("inversion_clear "^ident^".")]
+ ("inversion_clear "^ident^".")]
-let concl_menu (_,_,concl,_) =
+let concl_menu (_,_,concl,_) =
let is_eq = is_equality_type concl in
["intro", "intro.";
"intros", "intros.";
"intuition","intuition." ] @
-
- (if is_eq then
+
+ (if is_eq then
["reflexivity", "reflexivity.";
"discriminate", "discriminate.";
"symmetry", "symmetry." ]
- else
+ else
[]) @
["assumption" ,"assumption.";
@@ -577,41 +577,41 @@ let concl_menu (_,_,concl,_) =
]
-let id_of_name = function
- | Names.Anonymous -> id_of_string "x"
+let id_of_name = function
+ | Names.Anonymous -> id_of_string "x"
| Names.Name x -> x
-let make_cases s =
+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 ->
+ | Libnames.IndRef i ->
let {Declarations.mind_nparams = np},
{Declarations.mind_consnames = carr ;
- Declarations.mind_nf_lc = tarr }
- = Global.lookup_inductive i
+ Declarations.mind_nf_lc = tarr }
+ = Global.lookup_inductive i
in
- Util.array_fold_right2
- (fun n t l ->
+ 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
+ let rec rename avoid = function
| [] -> []
- | (n,_)::l ->
+ | (n,_)::l ->
let n' = next_global_ident_away true
- (id_of_name n)
+ (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
+ carr
tarr
[]
| _ -> raise Not_found
-let current_status () =
+let current_status () =
let path = msg (Libnames.pr_dirpath (Lib.cwd ())) in
let path = if path = "Top" then "Ready" else "Ready in " ^ String.sub path 4 (String.length path - 4) in
try
diff --git a/ide/coq.mli b/ide/coq.mli
index df369cc18..c2f96a1fe 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -42,15 +42,15 @@ val reset_initial : unit -> unit
val reset_to : reset_mark -> unit
val reset_to_mod : identifier -> unit
-val init : unit -> string list
+val init : unit -> string list
val interp : bool -> string -> reset_info * (Util.loc * Vernacexpr.vernac_expr)
val interp_last : Util.loc * Vernacexpr.vernac_expr -> unit
-val interp_and_replace : string ->
+val interp_and_replace : string ->
(reset_info * (Util.loc * Vernacexpr.vernac_expr)) * string
(* type hyp = (identifier * constr option * constr) * string *)
-type hyp = env * evar_map *
+type hyp = env * evar_map *
((identifier*string) * constr option * constr) * (string * string)
type meta = env * evar_map * string
type concl = env * evar_map * constr * string
@@ -74,7 +74,7 @@ val is_in_loadpath : string -> bool
val make_cases : string -> string list list
-type tried_tactic =
+type tried_tactic =
| Interrupted
| Success of int (* nb of goals after *)
| Failed
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index 80ac5a200..e4a3ae56a 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -43,7 +43,7 @@ let commands = [
];
["End";
"End Silent.";
- "Eval";
+ "Eval";
"Extract Constant";
"Extract Inductive";
"Extraction Inline";
@@ -84,7 +84,7 @@ let commands = [
["Parameter";
"Proof.";
"Program Definition";
- "Program Fixpoint";
+ "Program Fixpoint";
"Program Lemma";
"Program Theorem";
];
@@ -100,7 +100,7 @@ let commands = [
"Require Export";
"Require Import";
"Reset Extraction Inline";
- "Restore State";
+ "Restore State";
];
[ "Save.";
"Scheme";
@@ -166,7 +166,7 @@ let state_preserving = [
"Extraction Module";
"Inspect";
"Locate";
-
+
"Obligations";
"Print";
"Print All.";
@@ -192,7 +192,7 @@ let state_preserving = [
"Print Scope";
"Print Scopes.";
"Print Section";
-
+
"Print Table Printing If.";
"Print Table Printing Let.";
"Print Tables.";
@@ -230,7 +230,7 @@ let state_preserving = [
]
-let tactics =
+let tactics =
[
[
"abstract";
@@ -317,7 +317,7 @@ let tactics =
"generalize";
"generalize dependent";
];
-
+
[
"hnf";
];
@@ -416,7 +416,7 @@ let tactics =
"trivial";
"try";
];
-
+
[
"unfold";
"unfold __ in";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c0dfb9e6e..4b08f4b9b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -25,7 +25,7 @@ type 'a info = {start:'a;
}
-class type analyzed_views=
+class type analyzed_views=
object('self)
val mutable act_id : GtkSignal.id option
val mutable deact_id : GtkSignal.id option
@@ -142,7 +142,7 @@ let notebook_page_of_session {script=script;tab_label=bname;proof_view=proof;mes
then img#set_stock `SAVE
else img#set_stock `YES) in
let _ =
- session_paned#misc#connect#size_allocate
+ session_paned#misc#connect#size_allocate
(let old_paned_width = ref 2 in
let old_paned_height = ref 2 in
(fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
@@ -180,12 +180,12 @@ let cb = GData.clipboard Gdk.Atom.primary
exception Size of int
let update_on_end_of_segment cmd_stk id =
- let lookup_section = function
+ let lookup_section = function
| { reset_info = _,_,r } -> r := false
in
try Stack.iter lookup_section cmd_stk with Exit -> ()
-let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast =
+let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast =
let x = {start = start_of_phrase_mark;
stop = end_of_phrase_mark;
ast = ast;
@@ -193,7 +193,7 @@ let push_phrase cmd_stk reset_info start_of_phrase_mark end_of_phrase_mark ast =
} in
begin
match snd ast with
- | VernacEndSegment (_,id) ->
+ | VernacEndSegment (_,id) ->
prerr_endline "Updating on end of segment 1";
update_on_end_of_segment cmd_stk id
| _ -> ()
@@ -240,7 +240,7 @@ let pop_command cmd_stk undos t =
let undos = update_proofs undos undo_info in
add_backtrack undos (BacktrackToMark state_info)
else
- begin
+ begin
prerr_endline "In section";
(* An object inside a closed section *)
add_backtrack undos BacktrackToNextActiveMark
@@ -295,7 +295,7 @@ let rec apply_undos cmd_stk (n,a,b,p,l as undos) =
end
-
+
let last_cb_content = ref ""
@@ -308,9 +308,9 @@ let update_notebook_pos () =
| true , true -> `RIGHT
in
session_notebook#set_tab_pos pos
-
-
-let set_active_view i =
+
+
+let set_active_view i =
prerr_endline "entering set_active_view";
(try on_active_view (fun {tab_label=lbl} -> lbl#set_text lbl#text) with _ -> ());
session_notebook#goto_page i;
@@ -323,25 +323,25 @@ let set_active_view i =
let to_do_on_page_switch = ref []
-
-let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
- Sys.sigill; Sys.sigpipe; Sys.sigquit;
+
+let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
+ Sys.sigill; Sys.sigpipe; Sys.sigquit;
(* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2]
let crash_save i =
(* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
Pervasives.prerr_endline "Trying to save all buffers in .crashcoqide files";
- let count = ref 0 in
- List.iter
- (function {script=view; analyzed_view = av } ->
- (let filename = match av#filename with
- | None ->
- incr count;
+ let count = ref 0 in
+ List.iter
+ (function {script=view; analyzed_view = av } ->
+ (let filename = match av#filename with
+ | None ->
+ incr count;
"Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
| Some f -> f^".crashcoqide"
in
- try
+ try
if try_export filename (view#buffer#get_text ()) then
Pervasives.prerr_endline ("Saved "^filename)
else Pervasives.prerr_endline ("Could not save "^filename)
@@ -365,9 +365,9 @@ let coq_computing = Mutex.create ()
(* To prevent Coq from interrupting during undoing...*)
let coq_may_stop = Mutex.create ()
-let break () =
+let break () =
prerr_endline "User break received:";
- if not (Mutex.try_lock coq_computing) then
+ if not (Mutex.try_lock coq_computing) then
begin
prerr_endline " trying to stop computation:";
if Mutex.try_lock coq_may_stop then begin
@@ -381,7 +381,7 @@ let break () =
prerr_endline " ignored (not computing)"
end
-let do_if_not_computing text f x =
+let do_if_not_computing text f x =
if Mutex.try_lock coq_computing then
let threaded_task () =
prerr_endline "Getting lock";
@@ -400,12 +400,12 @@ let do_if_not_computing text f x =
then (Mutex.unlock coq_computing; false)
else (pbar#pulse (); true)));
ignore (Thread.create threaded_task ())
- else
- prerr_endline
- "Discarded order (computations are ongoing)"
+ else
+ prerr_endline
+ "Discarded order (computations are ongoing)"
(* XXX - 1 appel *)
-let kill_input_view i =
+let kill_input_view i =
let v = session_notebook#get_nth_term i in
v.analyzed_view#kill_detached_views ();
v.script#destroy ();
@@ -418,7 +418,7 @@ let kill_input_view i =
let get_current_view =
focused_session
*)
-let remove_current_view_page () =
+let remove_current_view_page () =
let c = session_notebook#current_page in
kill_input_view c
@@ -426,53 +426,53 @@ let remove_current_view_page () =
(* Reset this to None on page change ! *)
let (last_completion:(string*int*int*bool) option ref) = ref None
-let () = to_do_on_page_switch :=
+let () = to_do_on_page_switch :=
(fun i -> last_completion := None)::!to_do_on_page_switch
let rec complete input_buffer w (offset:int) =
- match !last_completion with
+ match !last_completion with
| Some (lw,loffset,lpos,backward)
when lw=w && loffset=offset ->
begin
let iter = input_buffer#get_iter (`OFFSET lpos) in
- if backward then
+ if backward then
match complete_backward w iter with
- | None ->
- last_completion :=
+ | None ->
+ last_completion :=
Some (lw,loffset,
- (find_word_end
+ (find_word_end
(input_buffer#get_iter (`OFFSET loffset)))#offset ,
- false);
+ false);
None
- | Some (ss,start,stop) as result ->
- last_completion :=
+ | Some (ss,start,stop) as result ->
+ last_completion :=
Some (w,offset,ss#offset,true);
result
else
match complete_forward w iter with
- | None ->
+ | None ->
last_completion := None;
None
- | Some (ss,start,stop) as result ->
- last_completion :=
+ | Some (ss,start,stop) as result ->
+ last_completion :=
Some (w,offset,ss#offset,false);
result
end
| _ -> begin
match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with
- | None ->
- last_completion :=
+ | None ->
+ last_completion :=
Some (w,offset,(find_word_end (input_buffer#get_iter
(`OFFSET offset)))#offset,false);
complete input_buffer w offset
- | Some (ss,start,stop) as result ->
+ | Some (ss,start,stop) as result ->
last_completion := Some (w,offset,ss#offset,true);
result
end
-
+
let get_current_word () =
match session_notebook#current_term,cb#text with
- | {script=script; analyzed_view=av;},None ->
+ | {script=script; analyzed_view=av;},None ->
prerr_endline "None selected";
let it = av#get_insert in
let start = find_word_start it in
@@ -484,7 +484,7 @@ let get_current_word () =
prerr_endline "Some selected";
prerr_endline t;
t
-
+
let input_channel b ic =
let buf = String.create 1024 and len = ref 0 in
@@ -506,7 +506,7 @@ exception Found
exception Stop of int
(* XXX *)
-let activate_input i =
+let activate_input i =
prerr_endline "entering activate_input";
(try on_active_view (fun {analyzed_view=a_v} -> a_v#reset_initial; a_v#deactivate ())
with _ -> ());
@@ -514,7 +514,7 @@ let activate_input i =
set_active_view i;
prerr_endline "exiting activate_input"
-let warning msg =
+let warning msg =
GToolbox.message_box ~title:"Warning"
~icon:(let img = GMisc.image () in
img#set_stock `DIALOG_WARNING;
@@ -534,7 +534,7 @@ object(self)
val cmd_stack = _cs
val mutable is_active = false
val mutable read_only = false
- val mutable filename = None
+ val mutable filename = None
val mutable stats = None
val mutable last_modification_time = 0.
val mutable last_auto_save_time = 0.
@@ -543,7 +543,7 @@ object(self)
val mutable auto_complete_on = !current.auto_complete
val hidden_proofs = Hashtbl.create 32
- method private toggle_auto_complete =
+ method private toggle_auto_complete =
auto_complete_on <- not auto_complete_on
method set_auto_complete t = auto_complete_on <- t
method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b = fun f x ->
@@ -552,30 +552,30 @@ object(self)
let y = f x in
self#set_auto_complete old;
y
- method add_detached_view (w:GWindow.window) =
+ method add_detached_view (w:GWindow.window) =
detached_views <- w::detached_views
- method remove_detached_view (w:GWindow.window) =
+ method remove_detached_view (w:GWindow.window) =
detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views
- method kill_detached_views () =
+ method kill_detached_views () =
List.iter (fun w -> w#destroy ()) detached_views;
detached_views <- []
method filename = filename
method stats = stats
- method set_filename f =
+ method set_filename f =
filename <- f;
- match f with
+ match f with
| Some f -> stats <- my_stat f
| None -> ()
- method update_stats =
- match filename with
- | Some f -> stats <- my_stat f
+ method update_stats =
+ match filename with
+ | Some f -> stats <- my_stat f
| _ -> ()
- method revert =
- match filename with
+ method revert =
+ match filename with
| Some f -> begin
let do_revert () = begin
push_info "Reverting buffer";
@@ -591,17 +591,17 @@ object(self)
pop_info ();
flash_info "Buffer reverted";
Highlight.highlight_all input_buffer;
- with _ ->
+ with _ ->
pop_info ();
flash_info "Warning: could not revert buffer";
end
in
- if input_buffer#modified then
- match (GToolbox.question_box
+ if input_buffer#modified then
+ match (GToolbox.question_box
~title:"Modified buffer changed on disk"
~buttons:["Revert from File";
"Overwrite File";
- "Disable Auto Revert"]
+ "Disable Auto Revert"]
~default:0
~icon:(stock_to_widget `DIALOG_WARNING)
"Some unsaved buffers changed on disk"
@@ -609,62 +609,62 @@ object(self)
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 ()
+ else do_revert ()
end
| None -> ()
- method save f =
+ method save f =
if try_export f (input_buffer#get_text ()) then begin
filename <- Some f;
input_buffer#set_modified false;
stats <- my_stat f;
- (match self#auto_save_name with
+ (match self#auto_save_name with
| None -> ()
| Some fn -> try Sys.remove fn with _ -> ());
true
end
else false
- method private auto_save_name =
- match filename with
+ method private auto_save_name =
+ match filename with
| None -> None
- | Some f ->
+ | Some f ->
let dir = Filename.dirname f in
- let base = (fst !current.auto_save_name) ^
- (Filename.basename f) ^
- (snd !current.auto_save_name)
+ 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 =
+ 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
+ match self#auto_save_name with
+ | None -> ()
+ | Some fn ->
+ try
last_auto_save_time <- Unix.time();
prerr_endline ("Autosave time : "^(string_of_float (Unix.time())));
if try_export fn (input_buffer#get_text ()) then begin
flash_info ~delay:1000 "Autosaved"
end
- else warning
+ else warning
("Autosave failed (check if " ^ fn ^ " is writable)")
- with _ ->
+ with _ ->
warning ("Autosave: unexpected error while writing "^fn)
- end
+ end
method save_as f =
- if Sys.file_exists f then
+ if Sys.file_exists f then
match (GToolbox.question_box ~title:"File exists on disk"
~buttons:["Overwrite";
- "Cancel";]
+ "Cancel";]
~default:1
~icon:
(let img = GMisc.image () in
@@ -691,30 +691,30 @@ object(self)
method clear_message = message_buffer#set_text ""
val mutable last_index = true
val last_array = [|"";""|]
- method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input")
+ method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input")
method get_insert = get_insert input_buffer
- method recenter_insert =
- (* BUG : to investigate further:
+ method recenter_insert =
+ (* BUG : to investigate further:
FIXED : Never call GMain.* in thread !
PLUS : GTK BUG ??? Cannot be called from a thread...
ADDITION: using sync instead of async causes deadlock...*)
ignore (GtkThread.async (
- input_view#scroll_to_mark
+ input_view#scroll_to_mark
~use_align:false
~yalign:0.75
~within_margin:0.25)
`INSERT)
- method indent_current_line =
+ method indent_current_line =
let get_nb_space it =
let it = it#copy in
let nb_sep = ref 0 in
let continue = ref true in
- while !continue do
- if it#char = space then begin
+ while !continue do
+ if it#char = space then begin
incr nb_sep;
if not it#nocopy#forward_char then continue := false;
end else continue := false
@@ -726,64 +726,64 @@ object(self)
let previous_line_spaces = get_nb_space previous_line in
let current_line_start = self#get_insert#set_line_offset 0 in
let current_line_spaces = get_nb_space current_line_start in
- if input_buffer#delete_interactive
- ~start:current_line_start
+ if input_buffer#delete_interactive
+ ~start:current_line_start
~stop:(current_line_start#forward_chars current_line_spaces)
()
- then
+ then
let current_line_start = self#get_insert#set_line_offset 0 in
- input_buffer#insert
+ input_buffer#insert
~iter:current_line_start
(String.make previous_line_spaces ' ')
end
- method show_pm_goal =
- proof_buffer#insert
+ method show_pm_goal =
+ proof_buffer#insert
(Printf.sprintf " *** Declarative Mode ***\n");
- try
+ try
let (hyps,concl) = get_current_pm_goal () in
List.iter
- (fun ((_,_,_,(s,_)) as _hyp) ->
+ (fun ((_,_,_,(s,_)) as _hyp) ->
proof_buffer#insert (s^"\n"))
hyps;
- proof_buffer#insert
+ proof_buffer#insert
(String.make 38 '_' ^ "\n");
- let (_,_,_,s) = concl in
+ let (_,_,_,s) = concl in
proof_buffer#insert ("thesis := \n "^s^"\n");
let my_mark = `NAME "end_of_conclusion" in
proof_buffer#move_mark
- ~where:((proof_buffer#get_iter_at_mark `INSERT))
+ ~where:((proof_buffer#get_iter_at_mark `INSERT))
my_mark;
- ignore (proof_view#scroll_to_mark my_mark)
- with Not_found ->
+ ignore (proof_view#scroll_to_mark my_mark)
+ with Not_found ->
match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with
Some endc ->
- proof_buffer#insert
- ("Subproof completed, now type "^endc^".")
+ proof_buffer#insert
+ ("Subproof completed, now type "^endc^".")
| None ->
proof_buffer#insert "Proof completed."
- method show_goals =
+ method show_goals =
try
proof_buffer#set_text "";
match Decl_mode.get_current_mode () with
Decl_mode.Mode_none -> ()
- | Decl_mode.Mode_tactic ->
+ | Decl_mode.Mode_tactic ->
begin
let s = Coq.get_current_goals () in
- match s with
+ match s with
| [] -> proof_buffer#insert (Coq.print_no_goal ())
- | (hyps,concl)::r ->
+ | (hyps,concl)::r ->
let goal_nb = List.length s in
- proof_buffer#insert
- (Printf.sprintf "%d subgoal%s\n"
+ proof_buffer#insert
+ (Printf.sprintf "%d subgoal%s\n"
goal_nb
(if goal_nb<=1 then "" else "s"));
List.iter
- (fun ((_,_,_,(s,_)) as _hyp) ->
+ (fun ((_,_,_,(s,_)) as _hyp) ->
proof_buffer#insert (s^"\n"))
hyps;
- proof_buffer#insert
+ proof_buffer#insert
(String.make 38 '_' ^ "(1/"^
(string_of_int goal_nb)^
")\n") ;
@@ -792,14 +792,14 @@ object(self)
proof_buffer#insert "\n";
let my_mark = `NAME "end_of_conclusion" in
proof_buffer#move_mark
- ~where:((proof_buffer#get_iter_at_mark `INSERT))
+ ~where:((proof_buffer#get_iter_at_mark `INSERT))
my_mark;
proof_buffer#insert "\n\n";
let i = ref 1 in
- List.iter
- (function (_,(_,_,_,concl)) ->
+ List.iter
+ (function (_,(_,_,_,concl)) ->
incr i;
- proof_buffer#insert
+ proof_buffer#insert
(String.make 38 '_' ^"("^
(string_of_int !i)^
"/"^
@@ -809,82 +809,82 @@ object(self)
proof_buffer#insert "\n\n";
)
r;
- ignore (proof_view#scroll_to_mark my_mark)
+ ignore (proof_view#scroll_to_mark my_mark)
end
- | Decl_mode.Mode_proof ->
+ | Decl_mode.Mode_proof ->
self#show_pm_goal
- with e ->
+ with e ->
prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e)
val mutable full_goal_done = true
- method show_goals_full =
+ method show_goals_full =
if not full_goal_done then
begin
try
proof_buffer#set_text "";
match Decl_mode.get_current_mode () with
Decl_mode.Mode_none -> ()
- | Decl_mode.Mode_tactic ->
+ | Decl_mode.Mode_tactic ->
begin
- match Coq.get_current_goals () with
+ match Coq.get_current_goals () with
[] -> Util.anomaly "show_goals_full"
| ((hyps,concl)::r) as s ->
let last_shown_area = Tags.Proof.highlight
in
let goal_nb = List.length s in
- proof_buffer#insert (Printf.sprintf "%d subgoal%s\n"
+ proof_buffer#insert (Printf.sprintf "%d subgoal%s\n"
goal_nb
(if goal_nb<=1 then "" else "s"));
- let coq_menu commands =
+ let coq_menu commands =
let tag = proof_buffer#create_tag []
- in
+ in
ignore
(tag#connect#event ~callback:
(fun ~origin ev it ->
- match GdkEvent.get_type ev with
- | `BUTTON_PRESS ->
+ match GdkEvent.get_type ev with
+ | `BUTTON_PRESS ->
let ev = (GdkEvent.Button.cast ev) in
if (GdkEvent.Button.button ev) = 3
then (
let loc_menu = GMenu.menu () in
- let factory =
+ let factory =
new GMenu.factory loc_menu in
- let add_coq_command (cp,ip) =
- ignore
- (factory#add_item cp
+ let add_coq_command (cp,ip) =
+ ignore
+ (factory#add_item cp
~callback:
(fun () -> ignore
- (self#insert_this_phrase_on_success
+ (self#insert_this_phrase_on_success
true
- true
- false
- ("progress "^ip^"\n")
+ true
+ false
+ ("progress "^ip^"\n")
(ip^"\n"))
)
)
in
List.iter add_coq_command commands;
- loc_menu#popup
+ loc_menu#popup
~button:3
~time:(GdkEvent.Button.time ev);
true)
else false
- | `MOTION_NOTIFY ->
+ | `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)
+ 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
+ proof_buffer#apply_tag
+ ~start:s
+ ~stop:e
last_shown_area;
prerr_endline "Applied tag";
@@ -896,14 +896,14 @@ object(self)
tag
in
List.iter
- (fun ((_,_,_,(s,_)) as hyp) ->
+ (fun ((_,_,_,(s,_)) as hyp) ->
let tag = coq_menu (hyp_menu hyp) in
proof_buffer#insert ~tags:[tag] (s^"\n"))
hyps;
- proof_buffer#insert
+ proof_buffer#insert
(String.make 38 '_' ^"(1/"^
(string_of_int goal_nb)^
- ")\n")
+ ")\n")
;
let tag = coq_menu (concl_menu concl) in
let _,_,_,sconcl = concl in
@@ -914,10 +914,10 @@ object(self)
~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark;
proof_buffer#insert "\n\n";
let i = ref 1 in
- List.iter
- (function (_,(_,_,_,concl)) ->
+ List.iter
+ (function (_,(_,_,_,concl)) ->
incr i;
- proof_buffer#insert
+ proof_buffer#insert
(String.make 38 '_' ^"("^
(string_of_int !i)^
"/"^
@@ -943,33 +943,33 @@ object(self)
assert (Glib.Utf8.validate s);
self#insert_message s;
message_view#misc#draw None;
- if localize then
- (match Option.map Util.unloc loc with
+ if localize then
+ (match Option.map Util.unloc loc with
| None -> ()
| Some (start,stop) ->
let convert_pos = byte_offset_to_char_offset phrase in
let start = convert_pos start in
let stop = convert_pos stop in
- let i = self#get_start_of_input in
+ let i = self#get_start_of_input in
let starti = i#forward_chars start in
let stopi = i#forward_chars stop in
input_buffer#apply_tag Tags.Script.error
~start:starti
~stop:stopi;
input_buffer#place_cursor starti) in
- try
+ try
full_goal_done <- false;
prerr_endline "Send_to_coq starting now";
Decl_mode.clear_daimon_flag ();
if replace then begin
let r,info = Coq.interp_and_replace ("info " ^ phrase) in
- let is_complete = not (Decl_mode.get_daimon_flag ()) in
+ let is_complete = not (Decl_mode.get_daimon_flag ()) in
let msg = read_stdout () in
sync display_output msg;
- Some (is_complete,r)
+ Some (is_complete,r)
end else begin
let r = Coq.interp verbosely phrase in
- let is_complete = not (Decl_mode.get_daimon_flag ()) in
+ let is_complete = not (Decl_mode.get_daimon_flag ()) in
let msg = read_stdout () in
sync display_output msg;
Some (is_complete,r)
@@ -978,29 +978,29 @@ object(self)
if show_error then sync display_error e;
None
- method find_phrase_starting_at (start:GText.iter) =
+ method find_phrase_starting_at (start:GText.iter) =
try
let end_iter = find_next_sentence start in
Some (start,end_iter)
with
| Not_found -> None
- method complete_at_offset (offset:int) =
+ method complete_at_offset (offset:int) =
prerr_endline ("Completion at offset : " ^ string_of_int offset);
let it () = input_buffer#get_iter (`OFFSET offset) in
let iit = it () in
let start = find_word_start iit in
- if ends_word iit then
- let w = input_buffer#get_text
+ if ends_word iit then
+ let w = input_buffer#get_text
~start
~stop:iit
()
in
if String.length w <> 0 then begin
prerr_endline ("Completion of prefix : '" ^ w^"'");
- match complete input_buffer w start#offset with
+ match complete input_buffer w start#offset with
| None -> false
- | Some (ss,start,stop) ->
+ | Some (ss,start,stop) ->
let completion = input_buffer#get_text ~start ~stop () in
ignore (input_buffer#delete_selection ());
ignore (input_buffer#insert_interactive completion);
@@ -1009,7 +1009,7 @@ object(self)
end else false
else false
- method process_next_phrase verbosely display_goals do_highlight =
+ method process_next_phrase verbosely display_goals do_highlight =
let get_next_phrase () =
self#clear_message;
prerr_endline "process_next_phrase starting now";
@@ -1017,7 +1017,7 @@ object(self)
push_info "Coq is computing";
input_view#set_editable false;
end;
- match self#find_phrase_starting_at self#get_start_of_input with
+ match self#find_phrase_starting_at self#get_start_of_input with
| None ->
if do_highlight then begin
input_view#set_editable true;
@@ -1041,9 +1041,9 @@ object(self)
let mark_processed reset_info is_complete (start,stop) ast =
let b = input_buffer in
b#move_mark ~where:stop (`NAME "start_of_input");
- b#apply_tag
+ b#apply_tag
(if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
+ if (self#get_insert#compare) stop <= 0 then
begin
b#place_cursor stop;
self#recenter_insert
@@ -1052,8 +1052,8 @@ object(self)
let end_of_phrase_mark = `MARK (b#create_mark stop) in
push_phrase
cmd_stack
- reset_info
- start_of_phrase_mark
+ reset_info
+ start_of_phrase_mark
end_of_phrase_mark ast;
if display_goals then self#show_goals;
remove_tag (start,stop) in
@@ -1062,42 +1062,42 @@ object(self)
None -> false
| Some (loc,phrase) ->
(match self#send_to_coq verbosely false phrase true true true with
- | Some (is_complete,(reset_info,ast)) ->
+ | Some (is_complete,(reset_info,ast)) ->
sync (mark_processed reset_info is_complete) loc ast; true
| None -> sync remove_tag loc; false)
end
- method insert_this_phrase_on_success
- show_output show_msg localize coqphrase insertphrase =
+ method insert_this_phrase_on_success
+ show_output show_msg localize coqphrase insertphrase =
let mark_processed reset_info is_complete ast =
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);
+ 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
+ input_buffer#apply_tag
(if is_complete then Tags.Script.processed else Tags.Script.unjustified) ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
+ 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 cmd_stack reset_info start_of_phrase_mark end_of_phrase_mark ast;
self#show_goals;
- (*Auto insert save on success...
- try (match Coq.get_current_goals () with
- | [] ->
+ (*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 ->
+ | 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";
+ 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
+ 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
@@ -1134,12 +1134,12 @@ object(self)
else begin
self#get_start_of_input
end
- in
- (try
- while ((stop#compare (get_current())>=0)
+ in
+ (try
+ while ((stop#compare (get_current())>=0)
&& (self#process_next_phrase false false false))
do Util.check_for_interrupt () done
- with Sys.Break ->
+ with Sys.Break ->
prerr_endline "Interrupted during process_until_iter_or_error");
sync (fun _ ->
self#show_goals;
@@ -1150,13 +1150,13 @@ object(self)
input_view#set_editable true) ();
pop_info()
- method process_until_end_or_error =
+ method process_until_end_or_error =
self#process_until_iter_or_error input_buffer#end_iter
method reset_initial =
sync (fun _ ->
- Stack.iter
- (function inf ->
+ Stack.iter
+ (function inf ->
let start = input_buffer#get_iter_at_mark inf.start in
let stop = input_buffer#get_iter_at_mark inf.stop in
input_buffer#move_mark ~where:start (`NAME "start_of_input");
@@ -1164,7 +1164,7 @@ object(self)
input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
input_buffer#delete_mark inf.start;
input_buffer#delete_mark inf.stop;
- )
+ )
cmd_stack;
Stack.clear cmd_stack;
self#clear_message)();
@@ -1175,10 +1175,10 @@ object(self)
prerr_endline "Backtracking_to iter starts now.";
(* pop Coq commands until we reach iterator [i] *)
let rec pop_commands done_smthg undos =
- if Stack.is_empty cmd_stack then
+ if Stack.is_empty cmd_stack then
done_smthg, undos
else
- let t = Stack.top cmd_stack in
+ let t = Stack.top cmd_stack in
if i#compare (input_buffer#get_iter_at_mark t.stop) < 0 then
begin
prerr_endline "Popped top command";
@@ -1191,21 +1191,21 @@ object(self)
let done_smthg, undos = pop_commands false undos in
prerr_endline "Popped commands";
if done_smthg then
- begin
- try
+ begin
+ try
apply_undos cmd_stack undos;
sync (fun _ ->
let start =
- if Stack.is_empty cmd_stack then input_buffer#start_iter
+ if Stack.is_empty cmd_stack then input_buffer#start_iter
else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
prerr_endline "Removing (long) processed tag...";
- input_buffer#remove_tag
+ input_buffer#remove_tag
Tags.Script.processed
- ~start
+ ~start
~stop:self#get_start_of_input;
- input_buffer#remove_tag
+ input_buffer#remove_tag
Tags.Script.unjustified
- ~start
+ ~start
~stop:self#get_start_of_input;
prerr_endline "Moving (long) start_of_input...";
input_buffer#move_mark ~where:start (`NAME "start_of_input");
@@ -1213,14 +1213,14 @@ object(self)
clear_stdout ();
self#clear_message)
();
- with _ ->
+ with _ ->
push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state.
Please restart and report NOW.";
end
else prerr_endline "backtrack_to : discarded (...)"
- method backtrack_to i =
- if Mutex.try_lock coq_may_stop then
+ 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 ())
@@ -1233,7 +1233,7 @@ object(self)
else self#backtrack_to point
method undo_last_step =
- if Mutex.try_lock coq_may_stop then
+ if Mutex.try_lock coq_may_stop then
(push_info "Undoing last step...";
(try
let last_command = Stack.top cmd_stack in
@@ -1268,19 +1268,19 @@ object(self)
else prerr_endline "undo_last_step discarded"
- method insert_command cp ip =
+ method insert_command cp ip =
async(fun _ -> self#clear_message)();
ignore (self#insert_this_phrase_on_success true false false cp ip)
method tactic_wizard l =
async(fun _ -> self#clear_message)();
- ignore
- (List.exists
- (fun p ->
- self#insert_this_phrase_on_success true false false
+ ignore
+ (List.exists
+ (fun p ->
+ self#insert_this_phrase_on_success true false false
("progress "^p^".\n") (p^".\n")) l)
- method active_keypress_handler k =
+ method active_keypress_handler k =
let state = GdkEvent.Key.state k in
begin
match state with
@@ -1295,12 +1295,12 @@ object(self)
self#process_until_iter_or_error i
end);
true
- | l when List.mem `CONTROL l ->
+ | l when List.mem `CONTROL l ->
let k = GdkEvent.Key.keyval k in
if GdkKeysyms._Break=k
then break ();
false
- | l ->
+ | l ->
if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
prerr_endline "active_kp_handler for Tab";
self#indent_current_line;
@@ -1309,9 +1309,9 @@ object(self)
end
- method disconnected_keypress_handler k =
+ method disconnected_keypress_handler k =
match GdkEvent.Key.state k with
- | l when List.mem `CONTROL l ->
+ | l when List.mem `CONTROL l ->
let k = GdkEvent.Key.keyval k in
if GdkKeysyms._c=k
then break ();
@@ -1322,16 +1322,16 @@ object(self)
val mutable deact_id = None
val mutable act_id = None
- method deactivate () =
+ method deactivate () =
is_active <- false;
- (match act_id with None -> ()
+ (match act_id with None -> ()
| Some id ->
reset_initial ();
input_view#misc#disconnect id;
prerr_endline "DISCONNECTED old active : ";
print_id id;
)(*;
- deact_id <- Some
+ deact_id <- Some
(input_view#event#connect#key_press self#disconnected_keypress_handler);
prerr_endline "CONNECTED inactive : ";
print_id (Option.get deact_id)*)
@@ -1339,17 +1339,17 @@ object(self)
(* XXX *)
method activate () =
is_active <- true;(*
- (match deact_id with None -> ()
+ (match deact_id with None -> ()
| Some id -> input_view#misc#disconnect id;
prerr_endline "DISCONNECTED old inactive : ";
print_id id
);*)
- act_id <- Some
+ act_id <- Some
(input_view#event#connect#key_press self#active_keypress_handler);
prerr_endline "CONNECTED active : ";
print_id (Option.get act_id);
- match
- filename
+ match
+ filename
with
| None -> ()
| Some f -> let dir = Filename.dirname f in
@@ -1359,9 +1359,9 @@ object(self)
(Printf.sprintf "Add LoadPath \"%s\". " dir))
end
- method electric_handler =
+ method electric_handler =
input_buffer#connect#insert_text ~callback:
- (fun it x ->
+ (fun it x ->
begin try
if last_index then begin
last_array.(0)<-x;
@@ -1370,7 +1370,7 @@ object(self)
last_array.(1)<-x;
if (last_array.(0) ^ last_array.(1) = ".\n") then raise Found
end
- with Found ->
+ with Found ->
begin
ignore (self#process_next_phrase false true true)
end;
@@ -1387,16 +1387,16 @@ object(self)
~stop:input_buffer#end_iter
tag;
if x = "" then () else
- match x.[String.length x - 1] with
- | ')' ->
+ 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
+ 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
+ else if c = oparen_code then
(decr count;false)
else false
)
@@ -1409,7 +1409,7 @@ object(self)
| _ -> ())
)
- method help_for_keyword () =
+ method help_for_keyword () =
browse_keyword (self#insert_message) (get_current_word ())
@@ -1449,9 +1449,9 @@ object(self)
input_buffer#remove_tag Tags.Script.hidden ~start:stmt_end ~stop:proof_end;
input_buffer#remove_tag Tags.Script.locked ~start:stmt_start ~stop:stmt_end
- initializer
+ initializer
ignore (message_buffer#connect#insert_text
- ~callback:(fun it s -> ignore
+ ~callback:(fun it s -> ignore
(message_view#scroll_to_mark
~use_align:false
~within_margin:0.49
@@ -1460,18 +1460,18 @@ object(self)
~callback:(fun it s ->
if (it#compare self#get_start_of_input)<0
then GtkSignal.stop_emit ();
- if String.length s > 1 then
+ if String.length s > 1 then
(prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor it)));
ignore (input_buffer#connect#after#apply_tag
~callback:(fun tag ~start ~stop ->
if (start#compare self#get_start_of_input)>=0
- then
+ then
begin
- input_buffer#remove_tag
+ input_buffer#remove_tag
Tags.Script.processed
~start
~stop;
- input_buffer#remove_tag
+ input_buffer#remove_tag
Tags.Script.unjustified
~start
~stop
@@ -1480,27 +1480,27 @@ object(self)
);
ignore (input_buffer#connect#after#insert_text
~callback:(fun it s ->
- if auto_complete_on &&
- String.length s = 1 && s <> " " && s <> "\n"
- then
- let v = session_notebook#current_term.analyzed_view
- in
- let has_completed =
- v#complete_at_offset
+ if auto_complete_on &&
+ String.length s = 1 && s <> " " && s <> "\n"
+ then
+ let v = session_notebook#current_term.analyzed_view
+ in
+ let has_completed =
+ v#complete_at_offset
((input_view#buffer#get_iter `SEL_BOUND)#offset)
in
- if has_completed then
+ if has_completed then
input_buffer#move_mark `SEL_BOUND (input_buffer#get_iter `SEL_BOUND)#forward_char;
)
);
ignore (input_buffer#connect#changed
- ~callback:(fun () ->
+ ~callback:(fun () ->
last_modification_time <- Unix.time ();
let r = input_view#visible_rect in
- let stop =
- input_view#get_iter_at_location
+ let stop =
+ input_view#get_iter_at_location
~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
in
@@ -1509,7 +1509,7 @@ object(self)
~start:self#get_start_of_input
~stop;
Highlight.highlight_around_current_line
- input_buffer
+ input_buffer
)
);
ignore (input_buffer#add_selection_clipboard cb);
@@ -1517,24 +1517,24 @@ object(self)
ignore (message_buffer#add_selection_clipboard cb);
let paren_highlight_tag = input_buffer#create_tag ~name:"paren" [`BACKGROUND "purple"] in
self#electric_paren paren_highlight_tag;
- ignore (input_buffer#connect#after#mark_set
+ ignore (input_buffer#connect#after#mark_set
~callback:(fun it (m:Gtk.text_mark) ->
- !set_location
- (Printf.sprintf
+ !set_location
+ (Printf.sprintf
"Line: %5d Char: %3d" (self#get_insert#line + 1)
(self#get_insert#line_offset + 1));
match GtkText.Mark.get_name m with
- | Some "insert" ->
+ | Some "insert" ->
input_buffer#remove_tag
~start:input_buffer#start_iter
~stop:input_buffer#end_iter
paren_highlight_tag;
- | Some s ->
+ | Some s ->
prerr_endline (s^" moved")
| None -> () )
);
ignore (input_buffer#connect#insert_text
- (fun it s ->
+ (fun it s ->
prerr_endline "Should recenter ?";
if String.contains s '\n' then begin
prerr_endline "Should recenter : yes";
@@ -1555,8 +1555,8 @@ let search_next_error () =
and b = int_of_string (Str.matched_group 3 !last_make)
and e = int_of_string (Str.matched_group 4 !last_make)
and msg_index = Str.match_beginning ()
- in
- last_make_index := Str.group_end 4;
+ in
+ last_make_index := Str.group_end 4;
(f,l,b,e,
String.sub !last_make msg_index (String.length !last_make - msg_index))
@@ -1638,7 +1638,7 @@ let create_session () =
proof#misc#set_can_focus true;
message#misc#set_can_focus true;
script#misc#modify_font !current.text_font;
- proof#misc#modify_font !current.text_font;
+ proof#misc#modify_font !current.text_font;
message#misc#modify_font !current.text_font;
{ tab_label=basename;
filename="";
@@ -1687,7 +1687,7 @@ let do_open session filename =
let do_save session =
- try
+ try
if session.script#buffer#modified then
save_session session session.filename [session.encoding]
with _ -> ()
@@ -1771,19 +1771,19 @@ let do_print session =
if session.filename = ""
then flash_info "Cannot print: this buffer has no name"
else begin
- let cmd =
+ let cmd =
"cd " ^ Filename.quote (Filename.dirname session.filename) ^ "; " ^
- !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename session.filename) ^
+ !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename session.filename) ^
" | " ^ !current.cmd_print
in
let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () in
let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in
let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in
- let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in
- let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in
+ let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in
+ let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in
let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in
- let callback_print () =
+ let callback_print () =
let cmd = print_entry#text in
let s,_ = run_command av#insert_message cmd in
flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
@@ -1795,15 +1795,15 @@ let do_print session =
end
-let main files =
+let main files =
(* Statup preferences *)
load_pref ();
(* Main window *)
- let w = GWindow.window
+ let w = GWindow.window
~wm_class:"CoqIde" ~wm_name:"CoqIde"
- ~allow_grow:true ~allow_shrink:true
- ~width:!current.window_width ~height:!current.window_height
+ ~allow_grow:true ~allow_shrink:true
+ ~width:!current.window_width ~height:!current.window_height
~title:"CoqIde" ()
in
(try
@@ -1819,15 +1819,15 @@ let main files =
let menubar = GMenu.menu_bar ~packing:vbox#pack () in
(* Toolbar *)
- let toolbar = GButton.toolbar
- ~orientation:`HORIZONTAL
+ let toolbar = GButton.toolbar
+ ~orientation:`HORIZONTAL
~style:`ICONS
- ~tooltips:true
+ ~tooltips:true
~packing:(* handle#add *)
(vbox#pack ~expand:false ~fill:false)
()
in
- show_toolbar :=
+ show_toolbar :=
(fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ());
let factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/" menubar in
@@ -1840,14 +1840,14 @@ let main files =
(* File/Load Menu *)
let load_file handler f =
- let f = absolute_filename f in
+ let f = absolute_filename f in
try
prerr_endline "Loading file starts";
if not (Util.list_fold_left_i
(fun i found x -> if found then found else
let {analyzed_view=av} = x in
- (match av#filename with
- | None -> false
+ (match av#filename with
+ | None -> false
| Some fn ->
if same_file f fn
then (session_notebook#goto_page i; true)
@@ -1861,7 +1861,7 @@ let main files =
prerr_endline "Loading: convert content";
let s = do_convert (Buffer.contents b) in
prerr_endline "Loading: create view";
- let session = create_session () in
+ let session = create_session () in
session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename f));
prerr_endline "Loading: adding view";
let index = session_notebook#append_term session in
@@ -1883,82 +1883,82 @@ let main files =
session.script#clear_undo;
prerr_endline "Loading: success"
end
- with
+ with
| e -> handler ("Load failed: "^(Printexc.to_string e))
- in
+ in
let load f = load_file flash_info f in
- let load_m = file_factory#add_item "_New"
+ let load_m = file_factory#add_item "_New"
~key:GdkKeysyms._N in
- let load_f () =
- match select_file_for_save ~title:"Create file" () with
+ let load_f () =
+ match select_file_for_save ~title:"Create file" () with
| None -> ()
| Some f -> load f
in
ignore (load_m#connect#activate (load_f));
- let load_m = file_factory#add_item "_Open"
+ let load_m = file_factory#add_item "_Open"
~key:GdkKeysyms._O in
- let load_f () =
- match select_file_for_open ~title:"Load file" () with
+ let load_f () =
+ match select_file_for_open ~title:"Load file" () with
| None -> ()
| Some f -> load f
in
ignore (load_m#connect#activate (load_f));
(* File/Save Menu *)
- let save_m = file_factory#add_item "_Save"
+ let save_m = file_factory#add_item "_Save"
~key:GdkKeysyms._S in
- let save_f () =
+ let save_f () =
let current = session_notebook#current_term in
try
- (match current.analyzed_view#filename with
+ (match current.analyzed_view#filename with
| None ->
begin match select_file_for_save ~title:"Save file" ()
with
| None -> ()
- | Some f ->
+ | Some f ->
if current.analyzed_view#save_as f then begin
current.tab_label#set_text (Filename.basename f);
flash_info ("File " ^ f ^ " saved")
end
else warning ("Save Failed (check if " ^ f ^ " is writable)")
end
- | Some f ->
- if current.analyzed_view#save f then
+ | Some f ->
+ if current.analyzed_view#save f then
flash_info ("File " ^ f ^ " saved")
else warning ("Save Failed (check if " ^ f ^ " is writable)")
-
+
)
- with
+ with
| e -> warning "Save: unexpected error"
in
ignore (save_m#connect#activate save_f);
(* File/Save As Menu *)
- let saveas_m = file_factory#add_item "S_ave as"
+ let saveas_m = file_factory#add_item "S_ave as"
in
- let saveas_f () =
+ let saveas_f () =
let current = session_notebook#current_term in
- try (match current.analyzed_view#filename with
- | None ->
+ try (match current.analyzed_view#filename with
+ | None ->
begin match select_file_for_save ~title:"Save file as" ()
with
| None -> ()
- | Some f ->
+ | Some f ->
if current.analyzed_view#save_as f then begin
current.tab_label#set_text (Filename.basename f);
flash_info "Saved"
end
else flash_info "Save Failed"
end
- | Some f ->
- begin match select_file_for_save
- ~dir:(ref (Filename.dirname f))
+ | Some f ->
+ begin match select_file_for_save
+ ~dir:(ref (Filename.dirname f))
~filename:(Filename.basename f)
~title:"Save file as" ()
with
| None -> ()
- | Some f ->
+ | Some f ->
if current.analyzed_view#save_as f then begin
current.tab_label#set_text (Filename.basename f);
flash_info "Saved"
@@ -1970,11 +1970,11 @@ let main files =
(* XXX *)
(* File/Save All Menu *)
let saveall_m = file_factory#add_item "Sa_ve all" in
- let saveall_f () =
+ let saveall_f () =
List.iter
- (function
- | {script = view ; analyzed_view = av} ->
- begin match av#filename with
+ (function
+ | {script = view ; analyzed_view = av} ->
+ begin match av#filename with
| None -> ()
| Some f ->
ignore (av#save f)
@@ -1982,26 +1982,26 @@ let main files =
) session_notebook#pages
in
(* XXX *)
- let has_something_to_save () =
+ let has_something_to_save () =
List.exists
- (function
- | {script=view} -> view#buffer#modified
+ (function
+ | {script=view} -> view#buffer#modified
)
session_notebook#pages
in
ignore (saveall_m#connect#activate saveall_f);
- (* XXX *)
+ (* XXX *)
(* File/Revert Menu *)
let revert_m = file_factory#add_item "_Revert all buffers" in
- let revert_f () =
- List.iter
- (function
- {analyzed_view = av} ->
- (try
- match av#filename,av#stats with
- | Some f,Some stats ->
+ let revert_f () =
+ List.iter
+ (function
+ {analyzed_view = av} ->
+ (try
+ match av#filename,av#stats with
+ | Some f,Some stats ->
let new_stats = Unix.stat f in
- if new_stats.Unix.st_mtime > stats.Unix.st_mtime
+ if new_stats.Unix.st_mtime > stats.Unix.st_mtime
then av#revert
| Some _, None -> av#revert
| _ -> ()
@@ -2009,18 +2009,18 @@ let main files =
) session_notebook#pages
in
ignore (revert_m#connect#activate revert_f);
-
+
(* File/Close Menu *)
let close_m =
file_factory#add_item "_Close buffer" ~key:GdkKeysyms._W in
- let close_f () =
+ let close_f () =
let v = !active_view in
let act = session_notebook#current_page in
if v = act then flash_info "Cannot close an active view"
else remove_current_view_page ()
in
ignore (close_m#connect#activate close_f);
-
+
(* File/Print Menu *)
let _ = file_factory#add_item "_Print..."
~key:GdkKeysyms._P
@@ -2031,62 +2031,62 @@ let main files =
let v = session_notebook#current_term in
let av = v.analyzed_view in
match av#filename with
- | None ->
+ | None ->
flash_info "Cannot print: this buffer has no name"
| Some f ->
let basef = Filename.basename f in
- let output =
+ let output =
let basef_we = try Filename.chop_extension basef with _ -> basef in
match kind with
| "latex" -> basef_we ^ ".tex"
| "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind
| _ -> assert false
in
- let cmd =
+ let cmd =
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^
!current.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
in
let s,_ = run_command av#insert_message cmd in
- flash_info (cmd ^
- if s = Unix.WEXITED 0
- then " succeeded"
+ flash_info (cmd ^
+ if s = Unix.WEXITED 0
+ then " succeeded"
else " failed")
in
let file_export_m = file_factory#add_submenu "E_xport to" in
let file_export_factory = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Export/" file_export_m ~accel_group in
- let _ =
- file_export_factory#add_item "_Html" ~callback:(export_f "html")
+ let _ =
+ file_export_factory#add_item "_Html" ~callback:(export_f "html")
in
- let _ =
+ let _ =
file_export_factory#add_item "_LaTeX" ~callback:(export_f "latex")
in
- let _ =
- file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi")
+ let _ =
+ file_export_factory#add_item "_Dvi" ~callback:(export_f "dvi")
in
- let _ =
- file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf")
+ let _ =
+ file_export_factory#add_item "_Pdf" ~callback:(export_f "pdf")
in
- let _ =
- file_export_factory#add_item "_Ps" ~callback:(export_f "ps")
+ let _ =
+ file_export_factory#add_item "_Ps" ~callback:(export_f "ps")
in
(* File/Rehighlight Menu *)
let rehighlight_m = file_factory#add_item "Reh_ighlight" ~key:GdkKeysyms._L in
- ignore (rehighlight_m#connect#activate
- (fun () ->
- Highlight.highlight_all
+ ignore (rehighlight_m#connect#activate
+ (fun () ->
+ Highlight.highlight_all
session_notebook#current_term.script#buffer;
session_notebook#current_term.analyzed_view#recenter_insert));
(* File/Quit Menu *)
let quit_f () =
save_pref();
- if has_something_to_save () then
+ if has_something_to_save () then
match (GToolbox.question_box ~title:"Quit"
~buttons:["Save Named Buffers and Quit";
"Quit without Saving";
- "Don't Quit"]
+ "Don't Quit"]
~default:0
~icon:
(let img = GMisc.image () in
@@ -2100,7 +2100,7 @@ let main files =
| _ -> ()
else exit 0
in
- let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q
+ let _ = file_factory#add_item "_Quit" ~key:GdkKeysyms._Q
~callback:quit_f
in
ignore (w#event#connect#delete (fun _ -> quit_f (); true));
@@ -2110,14 +2110,14 @@ let main files =
let edit_f = new GMenu.factory ~accel_path:"<CoqIde MenuBar>/Edit/" edit_menu ~accel_group in
ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback:
(do_if_not_computing "undo"
- (fun () ->
+ (fun () ->
ignore (session_notebook#current_term.analyzed_view#
- without_auto_complete
+ without_auto_complete
(fun () -> session_notebook#current_term.script#undo) ()))));
- ignore(edit_f#add_item "_Clear Undo Stack"
+ ignore(edit_f#add_item "_Clear Undo Stack"
(* ~key:GdkKeysyms._exclam *)
~callback:
- (fun () ->
+ (fun () ->
ignore session_notebook#current_term.script#clear_undo));
ignore(edit_f#add_separator ());
let get_active_view_for_cp () =
@@ -2131,31 +2131,31 @@ let main files =
in
ignore(edit_f#add_item "Cut" ~key:GdkKeysyms._X ~callback:
(fun () -> GtkSignal.emit_unit
- (get_active_view_for_cp ())
+ (get_active_view_for_cp ())
GtkText.View.S.cut_clipboard
- ));
+ ));
ignore(edit_f#add_item "Copy" ~key:GdkKeysyms._C ~callback:
(fun () -> GtkSignal.emit_unit
- (get_active_view_for_cp ())
+ (get_active_view_for_cp ())
GtkText.View.S.copy_clipboard));
ignore(edit_f#add_item "Paste" ~key:GdkKeysyms._V ~callback:
- (fun () ->
+ (fun () ->
try GtkSignal.emit_unit
- session_notebook#current_term.script#as_view
+ session_notebook#current_term.script#as_view
GtkText.View.S.paste_clipboard
with _ -> prerr_endline "EMIT PASTE FAILED"));
ignore (edit_f#add_separator ());
(*
- let toggle_auto_complete_i =
- edit_f#add_check_item "_Auto Completion"
+ let toggle_auto_complete_i =
+ edit_f#add_check_item "_Auto Completion"
~active:!current.auto_complete
~callback:
in
*)
(*
- auto_complete :=
+ auto_complete :=
(fun b -> match session_notebook#current_term.analyzed_view with
| Some av -> av#set_auto_complete b
| None -> ());
@@ -2163,7 +2163,7 @@ let main files =
let last_found = ref None in
let search_backward = ref false in
- let find_w = GWindow.window
+ let find_w = GWindow.window
(* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *)
(* ~allow_grow:true ~allow_shrink:true *)
(* ~width:!current.window_width ~height:!current.window_height *)
@@ -2174,28 +2174,28 @@ let main files =
~columns:3 ~rows:5
~col_spacings:10 ~row_spacings:10 ~border_width:10
~homogeneous:false ~packing:find_w#add () in
-
- let _ =
+
+ let _ =
GMisc.label ~text:"Find:"
~xalign:1.0
- ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) ()
+ ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) ()
in
let find_entry = GEdit.entry
~editable: true
~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X)
()
in
- let _ =
+ let _ =
GMisc.label ~text:"Replace with:"
~xalign:1.0
- ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) ()
+ ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) ()
in
let replace_entry = GEdit.entry
~editable: true
~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X)
()
in
- (* let _ =
+ (* let _ =
GButton.check_button
~label:"case sensitive"
~active:true
@@ -2205,7 +2205,7 @@ let main files =
in
*)
(*
- let find_backwards_check =
+ let find_backwards_check =
GButton.check_button
~label:"search backwards"
~active:false
@@ -2247,7 +2247,7 @@ let main files =
let v = session_notebook#current_term.script in
let b = v#buffer in
let start,stop =
- match !last_found with
+ match !last_found with
| None -> let i = b#get_iter_at_mark `INSERT in (i,i)
| Some(start,stop) ->
let start = b#get_iter_at_mark start
@@ -2262,7 +2262,7 @@ let main files =
let do_replace () =
let v = session_notebook#current_term.script in
let b = v#buffer in
- match !last_found with
+ match !last_found with
| None -> ()
| Some(start,stop) ->
let start = b#get_iter_at_mark start
@@ -2290,7 +2290,7 @@ let main files =
in
let do_find () =
let (v,b,starti,_) = last_find () in
- find_from v b starti find_entry#text
+ find_from v b starti find_entry#text
in
let do_replace_find () =
do_replace();
@@ -2302,8 +2302,8 @@ let main files =
find_w#misc#hide();
v#coerce#misc#grab_focus()
in
- to_do_on_page_switch :=
- (fun i -> if find_w#misc#visible then close_find())::
+ to_do_on_page_switch :=
+ (fun i -> if find_w#misc#visible then close_find())::
!to_do_on_page_switch;
let find_again_forward () =
search_backward := false;
@@ -2325,12 +2325,12 @@ let main files =
find_w#misc#hide();
v#coerce#misc#grab_focus();
true
- end
+ end
else if k = GdkKeysyms._Return then
begin
close_find();
true
- end
+ end
else if List.mem `CONTROL s && k = GdkKeysyms._f then
begin
find_again_forward ();
@@ -2343,7 +2343,7 @@ let main files =
end
else false (* to let default callback execute *)
in
- let find_f ~backward () =
+ let find_f ~backward () =
search_backward := backward;
find_w#show ();
find_w#present ();
@@ -2377,30 +2377,30 @@ let main files =
let complete_i = edit_f#add_item "_Complete"
~key:GdkKeysyms._comma
~callback:
- (do_if_not_computing
- (fun b ->
- let v = session_notebook#current_term.analyzed_view
-
- in v#complete_at_offset
+ (do_if_not_computing
+ (fun b ->
+ let v = session_notebook#current_term.analyzed_view
+
+ in v#complete_at_offset
((v#view#buffer#get_iter `SEL_BOUND)#offset)
))
in
complete_i#misc#set_state `INSENSITIVE;
*)
-
+
ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback:
- (fun () ->
+ (fun () ->
ignore (
- let av = session_notebook#current_term.analyzed_view in
+ let av = session_notebook#current_term.analyzed_view in
av#complete_at_offset (av#get_insert)#offset
)));
ignore(edit_f#add_separator ());
(* external editor *)
- let _ =
+ let _ =
edit_f#add_item "External editor" ~callback:
- (fun () ->
- let av = session_notebook#current_term.analyzed_view in
+ (fun () ->
+ let av = session_notebook#current_term.analyzed_view in
match av#filename with
| None -> warning "Call to external editor available only on named files"
| Some f ->
@@ -2413,33 +2413,33 @@ let main files =
(* Preferences *)
let reset_revert_timer () =
disconnect_revert_timer ();
- if !current.global_auto_revert then
+ if !current.global_auto_revert then
revert_timer := Some
- (GMain.Timeout.add ~ms:!current.global_auto_revert_delay
+ (GMain.Timeout.add ~ms:!current.global_auto_revert_delay
~callback:
- (fun () ->
+ (fun () ->
do_if_not_computing "revert" (sync revert_f) ();
true))
in reset_revert_timer (); (* to enable statup preferences timer *)
(* XXX *)
- let auto_save_f () =
- List.iter
- (function
- {script = view ; analyzed_view = av} ->
- (try
+ let auto_save_f () =
+ List.iter
+ (function
+ {script = view ; analyzed_view = av} ->
+ (try
av#auto_save
with _ -> ())
- )
+ )
session_notebook#pages
in
let reset_auto_save_timer () =
disconnect_auto_save_timer ();
- if !current.auto_save then
+ if !current.auto_save then
auto_save_timer := Some
- (GMain.Timeout.add ~ms:!current.auto_save_delay
+ (GMain.Timeout.add ~ms:!current.auto_save_delay
~callback:
- (fun () ->
+ (fun () ->
do_if_not_computing "autosave" (sync auto_save_f) ();
true))
in reset_auto_save_timer (); (* to enable statup preferences timer *)
@@ -2457,13 +2457,13 @@ let main files =
*)
(* Navigation Menu *)
let navigation_menu = factory#add_submenu "_Navigation" in
- let navigation_factory =
- new GMenu.factory navigation_menu
+ let navigation_factory =
+ new GMenu.factory navigation_menu
~accel_path:"<CoqIde MenuBar>/Navigation/"
- ~accel_group
- ~accel_modi:!current.modifier_for_navigation
+ ~accel_group
+ ~accel_modi:!current.modifier_for_navigation
in
- let _do_or_activate f () =
+ let _do_or_activate f () =
let current = session_notebook#current_term in
let analyzed_view = current.analyzed_view in
if analyzed_view#is_active then begin
@@ -2478,7 +2478,7 @@ let main files =
end
in
- let do_or_activate f =
+ let do_or_activate f =
do_if_not_computing "do_or_activate"
(_do_or_activate
(fun av -> f av;
@@ -2488,9 +2488,9 @@ let main files =
)
in
- let add_to_menu_toolbar text ~tooltip ?key ~callback icon =
+ let add_to_menu_toolbar text ~tooltip ?key ~callback icon =
begin
- match key with None -> ()
+ match key with None -> ()
| Some key -> ignore (navigation_factory#add_item text ~key ~callback)
end;
ignore (toolbar#insert_button
@@ -2500,49 +2500,49 @@ let main files =
~callback
())
in
- add_to_menu_toolbar
- "_Save"
- ~tooltip:"Save current buffer"
+ add_to_menu_toolbar
+ "_Save"
+ ~tooltip:"Save current buffer"
~callback:save_f
`SAVE;
- add_to_menu_toolbar
- "_Close"
- ~tooltip:"Close current buffer"
+ add_to_menu_toolbar
+ "_Close"
+ ~tooltip:"Close current buffer"
~callback:close_f
`CLOSE;
- add_to_menu_toolbar
- "_Forward"
- ~tooltip:"Forward one command"
- ~key:GdkKeysyms._Down
+ add_to_menu_toolbar
+ "_Forward"
+ ~tooltip:"Forward one command"
+ ~key:GdkKeysyms._Down
~callback:(do_or_activate (fun a -> a#process_next_phrase true true true ))
-
+
`GO_DOWN;
add_to_menu_toolbar "_Backward"
- ~tooltip:"Backward one command"
+ ~tooltip:"Backward one command"
~key:GdkKeysyms._Up
~callback:(do_or_activate (fun a -> a#undo_last_step))
`GO_UP;
- add_to_menu_toolbar
- "_Go to"
- ~tooltip:"Go to cursor"
+ add_to_menu_toolbar
+ "_Go to"
+ ~tooltip:"Go to cursor"
~key:GdkKeysyms._Right
~callback:(do_or_activate (fun a-> a#go_to_insert))
`JUMP_TO;
- add_to_menu_toolbar
- "_Start"
- ~tooltip:"Go to start"
+ add_to_menu_toolbar
+ "_Start"
+ ~tooltip:"Go to start"
~key:GdkKeysyms._Home
~callback:(do_or_activate (fun a -> a#reset_initial))
`GOTO_TOP;
- add_to_menu_toolbar
- "_End"
- ~tooltip:"Go to end"
+ add_to_menu_toolbar
+ "_End"
+ ~tooltip:"Go to end"
~key:GdkKeysyms._End
~callback:(do_or_activate (fun a -> a#process_until_end_or_error))
`GOTO_BOTTOM;
add_to_menu_toolbar "_Interrupt"
- ~tooltip:"Interrupt computations"
- ~key:GdkKeysyms._Break
+ ~tooltip:"Interrupt computations"
+ ~key:GdkKeysyms._Break
~callback:break
`STOP;
add_to_menu_toolbar "_Hide"
@@ -2555,13 +2555,13 @@ let main files =
(* Tactics Menu *)
let tactics_menu = factory#add_submenu "_Try Tactics" in
- let tactics_factory =
- new GMenu.factory tactics_menu
+ let tactics_factory =
+ new GMenu.factory tactics_menu
~accel_path:"<CoqIde MenuBar>/Tactics/"
- ~accel_group
+ ~accel_group
~accel_modi:!current.modifier_for_tactics
in
- let do_if_active_raw f () =
+ let do_if_active_raw f () =
let current = session_notebook#current_term in
let analyzed_view = current.analyzed_view in
if analyzed_view#is_active then ignore (f analyzed_view)
@@ -2569,36 +2569,36 @@ let main files =
let do_if_active f =
do_if_not_computing "do_if_active" (do_if_active_raw f) in
- ignore (tactics_factory#add_item "_auto"
+ ignore (tactics_factory#add_item "_auto"
~key:GdkKeysyms._a
~callback:(do_if_active (fun a -> a#insert_command "progress auto.\n" "auto.\n"))
);
ignore (tactics_factory#add_item "_auto with *"
~key:GdkKeysyms._asterisk
- ~callback:(do_if_active (fun a -> a#insert_command
+ ~callback:(do_if_active (fun a -> a#insert_command
"progress auto with *.\n"
"auto with *.\n")));
ignore (tactics_factory#add_item "_eauto"
~key:GdkKeysyms._e
- ~callback:(do_if_active (fun a -> a#insert_command
+ ~callback:(do_if_active (fun a -> a#insert_command
"progress eauto.\n"
"eauto.\n"))
);
ignore (tactics_factory#add_item "_eauto with *"
~key:GdkKeysyms._ampersand
- ~callback:(do_if_active (fun a -> a#insert_command
- "progress eauto with *.\n"
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "progress eauto with *.\n"
"eauto with *.\n"))
);
ignore (tactics_factory#add_item "_intuition"
~key:GdkKeysyms._i
- ~callback:(do_if_active (fun a -> a#insert_command
- "progress intuition.\n"
+ ~callback:(do_if_active (fun a -> a#insert_command
+ "progress intuition.\n"
"intuition.\n"))
);
ignore (tactics_factory#add_item "_omega"
~key:GdkKeysyms._o
- ~callback:(do_if_active (fun a -> a#insert_command
+ ~callback:(do_if_active (fun a -> a#insert_command
"omega.\n" "omega.\n"))
);
ignore (tactics_factory#add_item "_simpl"
@@ -2628,15 +2628,15 @@ let main files =
ignore (tactics_factory#add_item "<Proof _Wizard>"
~key:GdkKeysyms._dollar
- ~callback:(do_if_active (fun a -> a#tactic_wizard
+ ~callback:(do_if_active (fun a -> a#tactic_wizard
!current.automatic_tactics
))
);
-
+
ignore (tactics_factory#add_separator ());
- let add_simple_template (factory: GMenu.menu GMenu.factory)
+ let add_simple_template (factory: GMenu.menu GMenu.factory)
(menu_text, text) =
- let text =
+ let text =
let l = String.length text - 1 in
if String.get text l = '.'
then text ^"\n"
@@ -2647,33 +2647,33 @@ let main files =
(fun () -> let {script = view } = session_notebook#current_term in
ignore (view#buffer#insert_interactive text)))
in
- List.iter
- (fun l ->
- match l with
+ List.iter
+ (fun l ->
+ match l with
| [] -> ()
- | [s] -> add_simple_template tactics_factory ("_"^s, s)
- | s::_ ->
+ | [s] -> add_simple_template tactics_factory ("_"^s, s)
+ | s::_ ->
let a = "_@..." in
a.[1] <- s.[0];
- let f = tactics_factory#add_submenu a in
+ let f = tactics_factory#add_submenu a in
let ff = new GMenu.factory f ~accel_group in
- List.iter
- (fun x ->
+ List.iter
+ (fun x ->
add_simple_template
- ff
+ ff
((String.sub x 0 1)^
"_"^
(String.sub x 1 (String.length x - 1)),
x))
l
- )
+ )
Coq_commands.tactics;
-
+
(* Templates Menu *)
let templates_menu = factory#add_submenu "Te_mplates" in
- let templates_factory = new GMenu.factory templates_menu
+ let templates_factory = new GMenu.factory templates_menu
~accel_path:"<CoqIde MenuBar>/Templates/"
- ~accel_group
+ ~accel_group
~accel_modi:!current.modifier_for_templates
in
let add_complex_template (menu_text, text, offset, len, key) =
@@ -2689,19 +2689,19 @@ let main files =
end in
ignore (templates_factory#add_item menu_text ~callback ?key)
in
- add_complex_template
- ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n",
+ add_complex_template
+ ("_Lemma __", "Lemma new_lemma : .\nProof.\n\nSave.\n",
19, 9, Some GdkKeysyms._L);
- add_complex_template
- ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n",
+ add_complex_template
+ ("_Theorem __", "Theorem new_theorem : .\nProof.\n\nSave.\n",
19, 11, Some GdkKeysyms._T);
- add_complex_template
+ add_complex_template
("_Definition __", "Definition ident := .\n",
6, 5, Some GdkKeysyms._D);
- add_complex_template
+ add_complex_template
("_Inductive __", "Inductive ident : :=\n | : .\n",
14, 5, Some GdkKeysyms._I);
- add_complex_template
+ add_complex_template
("_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n",
29, 5, Some GdkKeysyms._F);
add_complex_template("_Scheme __",
@@ -2709,14 +2709,14 @@ let main files =
with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
(* Template for match *)
- let callback () =
+ let callback () =
let w = get_current_word () in
- try
+ try
let cases = Coq.make_cases w
in
let print c = function
| [x] -> Format.fprintf c " | %s => _@\n" x
- | x::l -> Format.fprintf c " | (%s%a) => _@\n" x
+ | x::l -> Format.fprintf c " | (%s%a) => _@\n" x
(print_list (fun c s -> Format.fprintf c " %s" s)) l
| [] -> assert false
in
@@ -2728,26 +2728,26 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
prerr_endline s;
let {script = view } = session_notebook#current_term in
ignore (view#buffer#delete_selection ());
- let m = view#buffer#create_mark
+ let m = view#buffer#create_mark
(view#buffer#get_iter `INSERT)
in
- if view#buffer#insert_interactive s then
+ if view#buffer#insert_interactive s then
let i = view#buffer#get_iter (`MARK m) in
let _ = i#nocopy#forward_chars 9 in
view#buffer#place_cursor i;
view#buffer#move_mark ~where:(i#backward_chars 3)
- `SEL_BOUND
+ `SEL_BOUND
with Not_found -> flash_info "Not an inductive type"
in
ignore (templates_factory#add_item "match ..."
~key:GdkKeysyms._C
~callback
);
-
+
(*
- let add_simple_template (factory: GMenu.menu GMenu.factory)
+ let add_simple_template (factory: GMenu.menu GMenu.factory)
(menu_text, text) =
- let text =
+ let text =
let l = String.length text - 1 in
if String.get text l = '.'
then text ^"\n"
@@ -2774,100 +2774,100 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
];
ignore (templates_factory#add_separator ());
*)
- List.iter
- (fun l ->
- match l with
+ List.iter
+ (fun l ->
+ match l with
| [] -> ()
- | [s] -> add_simple_template templates_factory ("_"^s, s)
- | s::_ ->
+ | [s] -> add_simple_template templates_factory ("_"^s, s)
+ | s::_ ->
let a = "_@..." in
a.[1] <- s.[0];
- let f = templates_factory#add_submenu a in
+ let f = templates_factory#add_submenu a in
let ff = new GMenu.factory f ~accel_group in
- List.iter
- (fun x ->
- add_simple_template
- ff
+ List.iter
+ (fun x ->
+ add_simple_template
+ ff
((String.sub x 0 1)^
"_"^
(String.sub x 1 (String.length x - 1)),
x))
l
- )
+ )
Coq_commands.commands;
-
+
(* Queries Menu *)
let queries_menu = factory#add_submenu "_Queries" in
let queries_factory = new GMenu.factory queries_menu ~accel_group
~accel_path:"<CoqIde MenuBar>/Queries"
~accel_modi:[]
in
-
+
(* Command/Show commands *)
- let _ =
+ let _ =
queries_factory#add_item "_SearchAbout " ~key:GdkKeysyms._F2
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"SearchAbout"
- ~term
+ ~term
())
in
- let _ =
+ let _ =
queries_factory#add_item "_Check " ~key:GdkKeysyms._F3
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"Check"
- ~term
+ ~term
())
in
- let _ =
+ let _ =
queries_factory#add_item "_Print " ~key:GdkKeysyms._F4
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"Print"
- ~term
+ ~term
())
in
- let _ =
+ let _ =
queries_factory#add_item "_About " ~key:GdkKeysyms._F5
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"About"
- ~term
+ ~term
())
in
- let _ =
- queries_factory#add_item "_Locate"
+ let _ =
+ queries_factory#add_item "_Locate"
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"Locate"
- ~term
+ ~term
())
in
- let _ =
- queries_factory#add_item "_Whelp Locate"
+ let _ =
+ queries_factory#add_item "_Whelp Locate"
~callback:(fun () -> let term = get_current_word () in
(Command_windows.command_window ())#new_command
~command:"Whelp Locate"
- ~term
+ ~term
())
in
(* Display menu *)
-
+
let display_menu = factory#add_submenu "_Display" in
let view_factory = new GMenu.factory display_menu
~accel_path:"<CoqIde MenuBar>/Display/"
- ~accel_group
+ ~accel_group
~accel_modi:!current.modifier_for_display
in
- let _ = ignore (view_factory#add_check_item
- "Display _implicit arguments"
+ let _ = ignore (view_factory#add_check_item
+ "Display _implicit arguments"
~key:GdkKeysyms._i
~callback:(fun _ -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display _coercions"
~key:GdkKeysyms._c
~callback:(fun _ -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ())) in
@@ -2877,51 +2877,51 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
~key:GdkKeysyms._m
~callback:(fun _ -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Deactivate _notations display"
~key:GdkKeysyms._n
~callback:(fun _ -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display _all basic low-level contents"
~key:GdkKeysyms._a
- ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in
+ ~callback:(fun _ -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display _existential variable instances"
~key:GdkKeysyms._e
~callback:(fun _ -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display _universe levels"
~key:GdkKeysyms._u
~callback:(fun _ -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ())) in
- let _ = ignore (view_factory#add_check_item
+ let _ = ignore (view_factory#add_check_item
"Display all _low-level contents"
~key:GdkKeysyms._l
- ~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) in
+ ~callback:(fun _ -> printing_state.printing_full_all <- not printing_state.printing_full_all; do_or_activate (fun a -> a#show_goals) ())) in
+
+
-
-
(* Externals *)
let externals_menu = factory#add_submenu "_Compile" in
- let externals_factory = new GMenu.factory externals_menu
+ let externals_factory = new GMenu.factory externals_menu
~accel_path:"<CoqIde MenuBar>/Compile/"
- ~accel_group
+ ~accel_group
~accel_modi:[]
in
-
+
(* Command/Compile Menu *)
let compile_f () =
let v = session_notebook#current_term in
let av = v.analyzed_view in
save_f ();
match av#filename with
- | None ->
+ | None ->
flash_info "Active buffer has no name"
| Some f ->
- let cmd = !current.cmd_coqc ^ " -I "
+ let cmd = !current.cmd_coqc ^ " -I "
^ (Filename.quote (Filename.dirname f))
^ " " ^ (Filename.quote f) in
let s,res = run_command av#insert_message cmd in
@@ -2935,8 +2935,8 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
av#insert_message res
end
in
- let _ =
- externals_factory#add_item "_Compile Buffer" ~callback:compile_f
+ let _ =
+ externals_factory#add_item "_Compile Buffer" ~callback:compile_f
in
(* Command/Make Menu *)
@@ -2944,10 +2944,10 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let v = session_notebook#current_term in
let av = v.analyzed_view in
match av#filename with
- | None ->
+ | None ->
flash_info "Cannot make: this buffer has no name"
| Some f ->
- let cmd =
+ let cmd =
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_make in
(*
@@ -2959,14 +2959,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
last_make_index := 0;
flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
- let _ = externals_factory#add_item "_Make"
+ let _ = externals_factory#add_item "_Make"
~key:GdkKeysyms._F6
- ~callback:make_f
+ ~callback:make_f
in
-
+
(* Compile/Next Error *)
- let next_error () =
+ let next_error () =
try
let file,line,start,stop,error_msg = search_next_error () in
load file;
@@ -3000,131 +3000,131 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let av = v.analyzed_view in
av#set_message "No more errors.\n"
in
- let _ =
- externals_factory#add_item "_Next error"
+ let _ =
+ externals_factory#add_item "_Next error"
~key:GdkKeysyms._F7
~callback:next_error in
-
+
(* Command/CoqMakefile Menu*)
let coq_makefile_f () =
let v = session_notebook#current_term in
let av = v.analyzed_view in
match av#filename with
- | None ->
+ | None ->
flash_info "Cannot make makefile: this buffer has no name"
| Some f ->
- let cmd =
+ let cmd =
"cd " ^ Filename.quote (Filename.dirname f) ^ "; " ^ !current.cmd_coqmakefile in
let s,res = run_command av#insert_message cmd in
- flash_info
+ flash_info
(!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
- let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f
+ let _ = externals_factory#add_item "_Make makefile" ~callback:coq_makefile_f
in
(* Windows Menu *)
let configuration_menu = factory#add_submenu "_Windows" in
- let configuration_factory = new GMenu.factory configuration_menu
+ let configuration_factory = new GMenu.factory configuration_menu
~accel_path:"<CoqIde MenuBar>/Windows"
~accel_modi:[]
~accel_group
in
let _ =
- configuration_factory#add_item
+ configuration_factory#add_item
"Show/Hide _Query Pane"
~key:GdkKeysyms._Escape
- ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then
+ ~callback:(fun () -> if (Command_windows.command_window ())#frame#misc#visible then
(Command_windows.command_window ())#frame#misc#hide ()
else
(Command_windows.command_window ())#frame#misc#show ())
- in
- let _ =
- configuration_factory#add_check_item
- "Show/Hide _Toolbar"
- ~callback:(fun _ ->
- !current.show_toolbar <- not !current.show_toolbar;
- !show_toolbar !current.show_toolbar)
in
- let _ = configuration_factory#add_item
+ let _ =
+ configuration_factory#add_check_item
+ "Show/Hide _Toolbar"
+ ~callback:(fun _ ->
+ !current.show_toolbar <- not !current.show_toolbar;
+ !show_toolbar !current.show_toolbar)
+ in
+ let _ = configuration_factory#add_item
"Detach _Script Window"
~callback:
(do_if_not_computing "detach script window" (sync
- (fun () ->
+ (fun () ->
let nb = session_notebook in
if nb#misc#toplevel#get_oid=w#coerce#get_oid then
- begin
- let nw = GWindow.window
+ begin
+ let nw = GWindow.window
~width:(!current.window_width*2/3)
~height:(!current.window_height*2/3)
~position:`CENTER
~wm_name:"CoqIde"
~wm_class:"CoqIde"
- ~title:"Script"
+ ~title:"Script"
~show:true () in
let parent = Option.get nb#misc#parent in
- ignore (nw#connect#destroy
+ ignore (nw#connect#destroy
~callback:
(fun () -> nb#misc#reparent parent));
nw#add_accel_group accel_group;
nb#misc#reparent nw#coerce
- end
+ end
)))
in
- let _ =
- configuration_factory#add_item
+ let _ =
+ configuration_factory#add_item
"Detach _View"
~callback:
(do_if_not_computing "detach view"
- (fun () ->
- match session_notebook#current_term with
- | {script=v;analyzed_view=av} ->
- let w = GWindow.window ~show:true
+ (fun () ->
+ match session_notebook#current_term with
+ | {script=v;analyzed_view=av} ->
+ let w = GWindow.window ~show:true
~width:(!current.window_width*2/3)
~height:(!current.window_height*2/3)
~position:`CENTER
~title:(match av#filename with
| None -> "*Unnamed*"
- | Some f -> f)
- ()
+ | Some f -> f)
+ ()
in
- let sb = GBin.scrolled_window
- ~packing:w#add ()
+ let sb = GBin.scrolled_window
+ ~packing:w#add ()
in
- let nv = GText.view
- ~buffer:v#buffer
- ~packing:sb#add
+ let nv = GText.view
+ ~buffer:v#buffer
+ ~packing:sb#add
()
in
- nv#misc#modify_font
- !current.text_font;
- ignore (w#connect#destroy
+ nv#misc#modify_font
+ !current.text_font;
+ ignore (w#connect#destroy
~callback:
(fun () -> av#remove_detached_view w));
av#add_detached_view w
-
+
))
in
(* Help Menu *)
let help_menu = factory#add_submenu "_Help" in
- let help_factory = new GMenu.factory help_menu
+ let help_factory = new GMenu.factory help_menu
~accel_path:"<CoqIde MenuBar>/Help/"
~accel_modi:[]
~accel_group in
- let _ = help_factory#add_item "Browse Coq _Manual"
+ let _ = help_factory#add_item "Browse Coq _Manual"
~callback:
- (fun () ->
- let av = session_notebook#current_term.analyzed_view in
+ (fun () ->
+ let av = session_notebook#current_term.analyzed_view in
browse av#insert_message (doc_url ())) in
- let _ = help_factory#add_item "Browse Coq _Library"
+ let _ = help_factory#add_item "Browse Coq _Library"
~callback:
- (fun () ->
- let av = session_notebook#current_term.analyzed_view in
+ (fun () ->
+ let av = session_notebook#current_term.analyzed_view in
browse av#insert_message !current.library_url) in
- let _ =
+ let _ =
help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1
- ~callback:(fun () ->
- let av = session_notebook#current_term.analyzed_view in
+ ~callback:(fun () ->
+ let av = session_notebook#current_term.analyzed_view in
av#help_for_keyword ())
in
let _ = help_factory#add_separator () in
@@ -3143,13 +3143,13 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
lower_hbox#pack ~expand:true status#coerce;
let search_lbl = GMisc.label ~text:"Search:"
~show:false
- ~packing:(lower_hbox#pack ~expand:false) ()
+ ~packing:(lower_hbox#pack ~expand:false) ()
in
let search_history = ref [] in
let search_input = GEdit.combo ~popdown_strings:!search_history
~enable_arrow_keys:true
~show:false
- ~packing:(lower_hbox#pack ~expand:false) ()
+ ~packing:(lower_hbox#pack ~expand:false) ()
in
search_input#disable_activate ();
let ready_to_wrap_search = ref false in
@@ -3160,10 +3160,10 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
let search_forward = ref true in
let matched_word = ref None in
- let memo_search () =
+ let memo_search () =
matched_word := Some search_input#entry#text
in
- let end_search () =
+ let end_search () =
prerr_endline "End Search";
memo_search ();
let v = session_notebook#current_term.script in
@@ -3173,7 +3173,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
search_lbl#misc#hide ();
search_input#misc#hide ()
in
- let end_search_focus_out () =
+ let end_search_focus_out () =
prerr_endline "End Search(focus out)";
memo_search ();
let v = session_notebook#current_term.script in
@@ -3183,67 +3183,67 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
search_input#misc#hide ()
in
ignore (search_input#entry#connect#activate ~callback:end_search);
- ignore (search_input#entry#event#connect#key_press
+ ignore (search_input#entry#event#connect#key_press
~callback:(fun k -> let kv = GdkEvent.Key.keyval k in
- if
+ if
kv = GdkKeysyms._Right
- || kv = GdkKeysyms._Up
+ || kv = GdkKeysyms._Up
|| kv = GdkKeysyms._Left
- || (kv = GdkKeysyms._g
+ || (kv = GdkKeysyms._g
&& (List.mem `CONTROL (GdkEvent.Key.state k)))
- then end_search ();
+ then end_search ();
false));
ignore (search_input#entry#event#connect#focus_out
~callback:(fun _ -> end_search_focus_out (); false));
- to_do_on_page_switch :=
- (fun i ->
+ to_do_on_page_switch :=
+ (fun i ->
start_of_search := None;
ready_to_wrap_search:=false)::!to_do_on_page_switch;
(* TODO : make it work !!! *)
- let rec search_f () =
+ let rec search_f () =
search_lbl#misc#show ();
search_input#misc#show ();
prerr_endline "search_f called";
if !start_of_search = None then begin
(* A full new search is starting *)
- start_of_search :=
- Some (session_notebook#current_term.script#buffer#create_mark
+ start_of_search :=
+ Some (session_notebook#current_term.script#buffer#create_mark
(session_notebook#current_term.script#buffer#get_iter_at_mark `INSERT));
start_of_found := !start_of_search;
end_of_found := !start_of_search;
matched_word := Some "";
end;
- let txt = search_input#entry#text in
+ let txt = search_input#entry#text in
let v = session_notebook#current_term.script in
- let iit = v#buffer#get_iter_at_mark `SEL_BOUND
+ let iit = v#buffer#get_iter_at_mark `SEL_BOUND
and insert_iter = v#buffer#get_iter_at_mark `INSERT
in
prerr_endline ("SELBOUND="^(string_of_int iit#offset));
prerr_endline ("INSERT="^(string_of_int insert_iter#offset));
-
+
(match
- if !search_forward then iit#forward_search txt
+ if !search_forward then iit#forward_search txt
else let npi = iit#forward_chars (Glib.Utf8.length txt) in
- match
+ match
(npi#offset = (v#buffer#get_iter_at_mark `INSERT)#offset),
- (let t = iit#get_text ~stop:npi in
+ (let t = iit#get_text ~stop:npi in
flash_info (t^"\n"^txt);
t = txt)
- with
- | true,true ->
+ with
+ | true,true ->
(flash_info "T,T";iit#backward_search txt)
| false,true -> flash_info "F,T";Some (iit,npi)
| _,false ->
(iit#backward_search txt)
- with
- | None ->
+ with
+ | None ->
if !ready_to_wrap_search then begin
ready_to_wrap_search := false;
flash_info "Search wrapped";
- v#buffer#place_cursor
+ v#buffer#place_cursor
(if !search_forward then v#buffer#start_iter else
v#buffer#end_iter);
search_f ()
@@ -3252,7 +3252,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
else flash_info "Search at start";
ready_to_wrap_search := true
end
- | Some (start,stop) ->
+ | Some (start,stop) ->
prerr_endline "search: before moving marks";
prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
@@ -3265,47 +3265,47 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
v#scroll_to_mark `SEL_BOUND
)
in
- ignore (search_input#entry#event#connect#key_release
+ ignore (search_input#entry#event#connect#key_release
~callback:
(fun ev ->
if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin
let v = session_notebook#current_term.script in
- (match !start_of_search with
- | None ->
+ (match !start_of_search with
+ | None ->
prerr_endline "search_key_rel: Placing sel_bound";
- v#buffer#move_mark
- `SEL_BOUND
+ v#buffer#move_mark
+ `SEL_BOUND
(v#buffer#get_iter_at_mark `INSERT)
- | Some mk -> let it = v#buffer#get_iter_at_mark
+ | Some mk -> let it = v#buffer#get_iter_at_mark
(`MARK mk) in
prerr_endline "search_key_rel: Placing cursor";
v#buffer#place_cursor it;
start_of_search := None
);
- search_input#entry#set_text "";
+ search_input#entry#set_text "";
v#coerce#misc#grab_focus ();
- end;
+ end;
false
));
ignore (search_input#entry#connect#changed search_f);
push_info "Ready";
(* Location display *)
let l = GMisc.label
- ~text:"Line: 1 Char: 1"
- ~packing:lower_hbox#pack () in
+ ~text:"Line: 1 Char: 1"
+ ~packing:lower_hbox#pack () in
l#coerce#misc#set_name "location";
set_location := l#set_text;
(* Progress Bar *)
lower_hbox#pack pbar#coerce;
pbar#set_text "CoqIde started";
(* XXX *)
- change_font :=
- (fun fd ->
- List.iter
+ change_font :=
+ (fun fd ->
+ List.iter
(fun {script=view; proof_view=prf_v; message_view=msg_v} ->
view#misc#modify_font fd;
prf_v#misc#modify_font fd;
- msg_v#misc#modify_font fd
+ msg_v#misc#modify_font fd
)
session_notebook#pages;
);
@@ -3333,7 +3333,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
b#insert ~iter:b#start_iter "\n\n";
if Glib.Utf8.validate ("You are running " ^ coq_version) then b#insert ~iter:b#start_iter ("You are running " ^ coq_version);
if Glib.Utf8.validate initial_string then b#insert ~iter:b#start_iter initial_string;
- (try
+ (try
let image = lib_ide_file "coq.png" in
let startup_image = GdkPixbuf.from_file image in
b#insert ~iter:b#start_iter "\n\n";
@@ -3343,7 +3343,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
in
let about (b:GText.buffer) =
- (try
+ (try
let image = lib_ide_file "coq.png" in
let startup_image = GdkPixbuf.from_file image in
b#insert ~iter:b#start_iter "\n\n";
@@ -3360,27 +3360,27 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
w#add_accel_group accel_group;
(* Remove default pango menu for textviews *)
w#show ();
- ignore (about_m#connect#activate
+ ignore (about_m#connect#activate
~callback:(fun () -> let prf_v = session_notebook#current_term.proof_view in
prf_v#buffer#set_text ""; about prf_v#buffer));
(*
-
+
*)
- resize_window := (fun () ->
- w#resize
+ resize_window := (fun () ->
+ w#resize
~width:!current.window_width
~height:!current.window_height);
ignore(nb#connect#switch_page
~callback:
- (fun i ->
+ (fun i ->
prerr_endline ("switch_page: starts " ^ string_of_int i);
List.iter (function f -> f i) !to_do_on_page_switch;
prerr_endline "switch_page: success")
);
if List.length files >=1 then
begin
- List.iter (fun f ->
- if Sys.file_exists f then load f else
+ List.iter (fun f ->
+ if Sys.file_exists f then load f else
let f = if Filename.check_suffix f ".v" then f else f^".v" in
load_file (fun s -> print_endline s; exit 1) f)
files;
@@ -3396,53 +3396,53 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
;;
-(* This function check every half of second if GeoProof has send
+(* This function check every half of second if GeoProof has send
something on his private clipboard *)
-let rec check_for_geoproof_input () =
+let rec check_for_geoproof_input () =
let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in
while true do
Thread.delay 0.1;
let s = cb_Dr#text in
- (match s with
- Some s ->
+ (match s with
+ Some s ->
if s <> "Ack" then
session_notebook#current_term.script#buffer#insert (s^"\n");
cb_Dr#set_text "Ack"
| None -> ()
);
(* cb_Dr#clear does not work so i use : *)
- (* cb_Dr#set_text "Ack" *)
+ (* cb_Dr#set_text "Ack" *)
done
-
-
-let start () =
+
+
+let start () =
let files = Coq.init () in
ignore_break ();
GtkMain.Rc.add_default_file (lib_ide_file ".coqide-gtk2rc");
- (try
+ (try
GtkMain.Rc.add_default_file (Filename.concat System.home ".coqide-gtk2rc");
with Not_found -> ());
ignore (GtkMain.Main.init ());
- GtkData.AccelGroup.set_default_mod_mask
+ GtkData.AccelGroup.set_default_mod_mask
(Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);
ignore (
Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
`WARNING;`CRITICAL]
- (fun ~level msg ->
+ (fun ~level msg ->
if level land Glib.Message.log_level `WARNING <> 0
then Pp.warning msg
else failwith ("Coqide internal error: " ^ msg)));
Command_windows.main ();
init_stdout ();
main files;
- if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ());
- while true do
- try
- GtkThread.main ()
+ if !Coq_config.with_geoproof then ignore (Thread.create check_for_geoproof_input ());
+ while true do
+ try
+ GtkThread.main ()
with
| Sys.Break -> prerr_endline "Interrupted." ; flush stderr
- | e ->
+ | e ->
Pervasives.prerr_endline ("CoqIde unexpected error:" ^ (Printexc.to_string e));
flush stderr;
crash_save 127
diff --git a/ide/coqide.mli b/ide/coqide.mli
index d84158a0b..4c01e747a 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -9,7 +9,7 @@
(*i $Id$ i*)
(* The CoqIde main module. The following function [start] will parse the
- command line, initialize the load path, load the input
+ command line, initialize the load path, load the input
state, load the files given on the command line, load the ressource file,
produce the output state if any, and finally will launch the interface. *)
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index 8da4d9dda..e92a345e3 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -24,38 +24,38 @@ let is_word_char c =
Glib.Unichar.isalnum c || c = underscore || c = prime
-let starts_word (it:GText.iter) =
+let starts_word (it:GText.iter) =
prerr_endline ("Starts word ? '"^(Glib.Utf8.from_unichar it#char)^"'");
(not it#copy#nocopy#backward_char ||
(let c = it#backward_char#char in
not (is_word_char c)))
-let ends_word (it:GText.iter) =
+let ends_word (it:GText.iter) =
(not it#copy#nocopy#forward_char ||
let c = it#forward_char#char in
not (is_word_char c)
)
-let inside_word (it:GText.iter) =
+let inside_word (it:GText.iter) =
let c = it#char in
not (starts_word it) &&
not (ends_word it) &&
is_word_char c
-let is_on_word_limit (it:GText.iter) = inside_word it || ends_word it
+let is_on_word_limit (it:GText.iter) = inside_word it || ends_word it
let find_word_start (it:GText.iter) =
let rec step_to_start it =
prerr_endline "Find word start";
- if not it#nocopy#backward_char then
+ if not it#nocopy#backward_char then
(prerr_endline "find_word_start: cannot backward"; it)
else if is_word_char it#char
then step_to_start it
- else (it#nocopy#forward_char;
+ else (it#nocopy#forward_char;
prerr_endline ("Word start at: "^(string_of_int it#offset));it)
in
step_to_start it#copy
@@ -64,8 +64,8 @@ let find_word_start (it:GText.iter) =
let find_word_end (it:GText.iter) =
let rec step_to_end (it:GText.iter) =
prerr_endline "Find word end";
- let c = it#char in
- if c<>0 && is_word_char c then (
+ let c = it#char in
+ if c<>0 && is_word_char c then (
ignore (it#nocopy#forward_char);
step_to_end it
) else (
@@ -75,34 +75,34 @@ let find_word_end (it:GText.iter) =
step_to_end it#copy
-let get_word_around (it:GText.iter) =
+let get_word_around (it:GText.iter) =
let start = find_word_start it in
let stop = find_word_end it in
start,stop
-let rec complete_backward w (it:GText.iter) =
+let rec complete_backward w (it:GText.iter) =
prerr_endline "Complete backward...";
- match it#backward_search w with
+ match it#backward_search w with
| None -> (prerr_endline "backward_search failed";None)
- | Some (start,stop) ->
+ | Some (start,stop) ->
prerr_endline ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
- if starts_word start then
+ if starts_word start then
let ne = find_word_end stop in
if ne#compare stop = 0
then complete_backward w start
else Some (start,stop,ne)
else complete_backward w start
-
-let rec complete_forward w (it:GText.iter) =
+
+let rec complete_forward w (it:GText.iter) =
prerr_endline "Complete forward...";
- match it#forward_search w with
+ match it#forward_search w with
| None -> None
- | Some (start,stop) ->
- if starts_word start then
+ | Some (start,stop) ->
+ if starts_word start then
let ne = find_word_end stop in
- if ne#compare stop = 0 then
+ if ne#compare stop = 0 then
complete_forward w stop
else Some (stop,stop,ne)
else complete_forward w stop
diff --git a/ide/highlight.mll b/ide/highlight.mll
index 44018ff09..21516f7cf 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -24,7 +24,7 @@
let h = Hashtbl.create 97 in
List.iter (fun s -> Hashtbl.add h s ())
[ "Add" ; "Check"; "Eval"; "Extraction" ;
- "Load" ; "Undo"; "Goal";
+ "Load" ; "Undo"; "Goal";
"Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ;
"End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments"
];
@@ -33,9 +33,9 @@
let is_constr_kw =
let h = Hashtbl.create 97 in
List.iter (fun s -> Hashtbl.add h s ())
- [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for";
+ [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for";
"end"; "as"; "let"; "in"; "dest"; "if"; "then"; "else"; "return";
- "Prop"; "Set"; "Type" ];
+ "Prop"; "Set"; "Type" ];
Hashtbl.mem h
(* Without this table, the automaton would be too big and
@@ -62,11 +62,11 @@
let starting = ref true
}
-let space =
+let space =
[' ' '\010' '\013' '\009' '\012']
-let firstchar =
+let firstchar =
['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
-let identchar =
+let identchar =
['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
let ident = firstchar identchar*
@@ -79,8 +79,8 @@ let multiword_declaration =
let locality = ("Local" space+)?
let multiword_command =
- "Set" (space+ ident)*
-| "Unset" (space+ ident)*
+ "Set" (space+ ident)*
+| "Unset" (space+ ident)*
| "Open" space+ locality "Scope"
| "Close" space+ locality "Scope"
| "Bind" space+ "Scope"
@@ -109,12 +109,12 @@ rule next_starting_order = parse
{ starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl }
| multiword_command
{ starting:=false; lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd }
- | ident as id
+ | ident as id
{ if id = "Time" then next_starting_order lexbuf else
begin
- starting:=false;
- if is_one_word_command id then
- lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd
+ starting:=false;
+ if is_one_word_command id then
+ lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd
else if is_one_word_declaration id then
lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.decl
else
@@ -125,9 +125,9 @@ rule next_starting_order = parse
| eof { raise End_of_file }
and next_interior_order = parse
- | "(*"
+ | "(*"
{ comment_start := lexeme_start lexbuf; comment lexbuf }
- | ident as id
+ | ident as id
{ if is_constr_kw id then
lexeme_start lexbuf, lexeme_end lexbuf, Tags.Script.kwd
else
@@ -154,9 +154,9 @@ and string_in_comment = parse
let highlighting = ref false
- let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop =
+ let highlight_slice (input_buffer:GText.buffer) (start:GText.iter) stop =
starting := true; (* approximation: assume the beginning of a sentence *)
- if !highlighting then prerr_endline "Rejected highlight"
+ if !highlighting then prerr_endline "Rejected highlight"
else begin
highlighting := true;
prerr_endline "Highlighting slice now";
@@ -170,16 +170,16 @@ and string_in_comment = parse
let s = start#get_slice ~stop in
let convert_pos = byte_offset_to_char_offset s in
let lb = Lexing.from_string s in
- try
+ try
while true do
let b,e,o =
if !starting then next_starting_order lb
else next_interior_order lb in
-
+
let b,e = convert_pos b,convert_pos e in
let start = input_buffer#get_iter_at_char (offset + b) in
let stop = input_buffer#get_iter_at_char (offset + e) in
- input_buffer#apply_tag ~start ~stop o
+ input_buffer#apply_tag ~start ~stop o
done
with End_of_file -> ()
end
@@ -188,22 +188,22 @@ and string_in_comment = parse
end
let highlight_current_line input_buffer =
- try
+ try
let i = get_insert input_buffer in
highlight_slice input_buffer (i#set_line_offset 0) i
with _ -> ()
- let highlight_around_current_line input_buffer =
- try
+ let highlight_around_current_line input_buffer =
+ try
let i = get_insert input_buffer in
- highlight_slice input_buffer
- (i#backward_lines 10)
+ highlight_slice input_buffer
+ (i#backward_lines 10)
(ignore (i#nocopy#forward_lines 10);i)
with _ -> ()
-
- let highlight_all input_buffer =
- try
+
+ let highlight_all input_buffer =
+ try
highlight_slice input_buffer input_buffer#start_iter input_buffer#end_iter
with _ -> ()
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index ebf789fb3..14e803899 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -15,7 +15,7 @@ exception Forbidden
(* status bar and locations *)
-let status = GMisc.statusbar ()
+let status = GMisc.statusbar ()
let push_info,pop_info =
let status_context = status#new_context "Messages" in
@@ -41,12 +41,12 @@ let prerr_string s =
let lib_ide_file f =
let coqlib = Envars.coqlib () in
Filename.concat (Filename.concat coqlib "ide") f
-
+
let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT
let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0
-let byte_offset_to_char_offset s byte_offset =
+let byte_offset_to_char_offset s byte_offset =
if (byte_offset < String.length s) then begin
let count_delta = ref 0 in
for i = 0 to byte_offset do
@@ -68,19 +68,19 @@ let print_id id =
prerr_endline ("GOT sig id :"^(string_of_int (Obj.magic id)))
-let do_convert s =
+let do_convert s =
Utf8_convert.f
(if Glib.Utf8.validate s then begin
prerr_endline "Input is UTF-8";s
end else
- let from_loc () =
+ let from_loc () =
let _,char_set = Glib.Convert.get_charset () in
flash_info
("Converting from locale ("^char_set^")");
Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s
in
- let from_manual () =
- flash_info
+ let from_manual () =
+ flash_info
("Converting from "^ !current.encoding_manual);
Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:!current.encoding_manual
in
@@ -90,30 +90,30 @@ let do_convert s =
with _ -> from_manual ()
end else begin
try
- from_manual ()
+ from_manual ()
with _ -> from_loc ()
end)
-let try_convert s =
+let try_convert s =
try
do_convert s
- with _ ->
+ with _ ->
"(* Fatal error: wrong encoding in input.
Please choose a correct encoding in the preference panel.*)";;
-let try_export file_name s =
- try let s =
+let try_export file_name s =
+ try let s =
try if !current.encoding_use_utf8 then begin
(prerr_endline "UTF-8 is enforced" ;s)
end else if !current.encoding_use_locale then begin
let is_unicode,char_set = Glib.Convert.get_charset () in
- if is_unicode then
- (prerr_endline "Locale is UTF-8" ;s)
+ if is_unicode then
+ (prerr_endline "Locale is UTF-8" ;s)
else
(prerr_endline ("Locale is "^char_set);
Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s)
- end else
+ end else
(prerr_endline ("Manual charset is "^ !current.encoding_manual);
Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:!current.encoding_manual s)
with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s)
@@ -137,16 +137,16 @@ let disconnect_auto_save_timer () = match !auto_save_timer with
| Some id -> GMain.Timeout.remove id; auto_save_timer := None
let highlight_timer = ref None
-let set_highlight_timer f =
- match !highlight_timer with
- | None ->
- revert_timer :=
- Some (GMain.Timeout.add ~ms:2000
+let set_highlight_timer f =
+ match !highlight_timer with
+ | None ->
+ revert_timer :=
+ Some (GMain.Timeout.add ~ms:2000
~callback:(fun () -> f (); highlight_timer := None; true))
- | Some id ->
+ | Some id ->
GMain.Timeout.remove id;
- revert_timer :=
- Some (GMain.Timeout.add ~ms:2000
+ revert_timer :=
+ Some (GMain.Timeout.add ~ms:2000
~callback:(fun () -> f (); highlight_timer := None; true))
@@ -156,31 +156,31 @@ let init_stdout,read_stdout,clear_stdout =
let out_ft = Format.formatter_of_buffer out_buff in
let deep_out_ft = Format.formatter_of_buffer out_buff in
let _ = Pp_control.set_gp deep_out_ft Pp_control.deep_gp in
- (fun () ->
+ (fun () ->
Pp_control.std_ft := out_ft;
Pp_control.err_ft := out_ft;
Pp_control.deep_ft := deep_out_ft;
),
- (fun () -> Format.pp_print_flush out_ft ();
+ (fun () -> Format.pp_print_flush out_ft ();
let r = Buffer.contents out_buff in
prerr_endline "Output from Coq is: "; prerr_endline r;
Buffer.clear out_buff; r),
- (fun () ->
+ (fun () ->
Format.pp_print_flush out_ft (); Buffer.clear out_buff)
let last_dir = ref ""
-let filter_all_files () = GFile.filter
- ~name:"All"
- ~patterns:["*"] ()
-
-let filter_coq_files () = GFile.filter
- ~name:"Coq source code"
+let filter_all_files () = GFile.filter
+ ~name:"All"
+ ~patterns:["*"] ()
+
+let filter_coq_files () = GFile.filter
+ ~name:"Coq source code"
~patterns:[ "*.v"] ()
let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () =
- let file = ref None in
+ let file = ref None in
let file_chooser = GWindow.file_chooser_dialog ~action:`OPEN ~modal:true ~title () in
file_chooser#add_button_stock `CANCEL `CANCEL ;
file_chooser#add_select_button_stock `OPEN `OPEN ;
@@ -189,8 +189,8 @@ let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () =
file_chooser#set_default_response `OPEN;
ignore (file_chooser#set_current_folder !dir);
begin match file_chooser#run () with
- | `OPEN ->
- begin
+ | `OPEN ->
+ begin
file := file_chooser#filename;
match !file with
None -> ()
@@ -198,27 +198,27 @@ let select_file_for_open ~title ?(dir = last_dir) ?(filename="") () =
end
| `DELETE_EVENT | `CANCEL -> ()
end ;
- file_chooser#destroy ();
+ file_chooser#destroy ();
!file
let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () =
- let file = ref None in
+ let file = ref None in
let file_chooser = GWindow.file_chooser_dialog ~action:`SAVE ~modal:true ~title () in
file_chooser#add_button_stock `CANCEL `CANCEL ;
file_chooser#add_select_button_stock `SAVE `SAVE ;
file_chooser#add_filter (filter_coq_files ());
file_chooser#add_filter (filter_all_files ());
- (* this line will be used when a lablgtk >= 2.10.0 is the default on most distributions
+ (* this line will be used when a lablgtk >= 2.10.0 is the default on most distributions
file_chooser#set_do_overwrite_confirmation true;
*)
file_chooser#set_default_response `SAVE;
ignore (file_chooser#set_current_folder !dir);
ignore (file_chooser#set_current_name filename);
-
+
begin match file_chooser#run () with
- | `SAVE ->
- begin
+ | `SAVE ->
+ begin
file := file_chooser#filename;
match !file with
None -> ()
@@ -226,7 +226,7 @@ let select_file_for_save ~title ?(dir = last_dir) ?(filename="") () =
end
| `DELETE_EVENT | `CANCEL -> ()
end ;
- file_chooser#destroy ();
+ file_chooser#destroy ();
!file
let find_tag_start (tag :GText.tag) (it:GText.iter) =
@@ -243,7 +243,7 @@ let find_tag_stop (tag :GText.tag) (it:GText.iter) =
()
done;
it
-let find_tag_limits (tag :GText.tag) (it:GText.iter) =
+let find_tag_limits (tag :GText.tag) (it:GText.iter) =
(find_tag_start tag it , find_tag_stop tag it)
(* explanations: Win32 threads won't work if events are produced
@@ -251,16 +251,16 @@ let find_tag_limits (tag :GText.tag) (it:GText.iter) =
case we must use GtkThread.async to push a callback in the
main thread. Beware that the synchronus version may produce
deadlocks. *)
-let async =
+let async =
if Sys.os_type = "Win32" then GtkThread.async else (fun x -> x)
-let sync =
+let sync =
if Sys.os_type = "Win32" then GtkThread.sync else (fun x -> x)
let mutex text f =
let m = Mutex.create() in
fun x ->
if Mutex.try_lock m
- then
+ then
(try
prerr_endline ("Got lock on "^text);
f x;
@@ -275,8 +275,8 @@ let mutex text f =
("Discarded call for "^text^": computations ongoing")
-let stock_to_widget ?(size=`DIALOG) s =
- let img = GMisc.image ()
+let stock_to_widget ?(size=`DIALOG) s =
+ let img = GMisc.image ()
in img#set_stock s;
img#coerce
@@ -296,12 +296,12 @@ let run_command f c =
let ne = ref 0 in
while n:= input cin buff 0 127 ; ne := input cerr buffe 0 127 ; !n+ !ne <> 0
do
- let r = try_convert (String.sub buff 0 !n) in
+ let r = try_convert (String.sub buff 0 !n) in
f r;
Buffer.add_string result r;
- let r = try_convert (String.sub buffe 0 !ne) in
+ let r = try_convert (String.sub buffe 0 !ne) in
f r;
- Buffer.add_string result r
+ Buffer.add_string result r
done;
(Unix.close_process_full (cin,cout,cerr), Buffer.contents result)
@@ -313,7 +313,7 @@ let browse f url =
"\"\ncheck your preferences for setting a valid browser command\n")
let doc_url () =
- if !current.doc_url = use_default_doc_url || !current.doc_url = "" then
+ if !current.doc_url = use_default_doc_url || !current.doc_url = "" then
if Sys.file_exists
(String.sub Coq_config.localwwwrefman 7
(String.length Coq_config.localwwwrefman - 7))
@@ -327,7 +327,7 @@ let url_for_keyword =
let ht = Hashtbl.create 97 in
lazy (
begin try
- let cin =
+ let cin =
try open_in (lib_ide_file "index_urls.txt")
with _ ->
let doc_url = doc_url () in
@@ -339,7 +339,7 @@ let url_for_keyword =
in
try while true do
let s = input_line cin in
- try
+ try
let i = String.index s ',' in
let k = String.sub s 0 i in
let u = String.sub s (i + 1) (String.length s - i - 1) in
@@ -356,16 +356,16 @@ let url_for_keyword =
Hashtbl.find ht : string -> string)
-let browse_keyword f text =
- try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u)
+let browse_keyword f text =
+ try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u)
with Not_found -> f ("No documentation found for \""^text^"\".\n")
(*
checks if two file names refer to the same (existing) file by
- comparing their device and inode.
+ comparing their device and inode.
It seems that under Windows, inode is always 0, so we cannot
- accurately check if
+ accurately check if
*)
(* Optimised for partial application (in case many candidates must be
@@ -377,7 +377,7 @@ let same_file f1 =
try
let s2 = Unix.stat f2 in
s1.Unix.st_dev = s2.Unix.st_dev &&
- if Sys.os_type = "Win32" then f1 = f2
+ if Sys.os_type = "Win32" then f1 = f2
else s1.Unix.st_ino = s2.Unix.st_ino
with
Unix.Unix_error _ -> false)
@@ -385,7 +385,7 @@ let same_file f1 =
Unix.Unix_error _ -> (fun _ -> false)
let absolute_filename f =
- if Filename.is_relative f then
+ if Filename.is_relative f then
Filename.concat (Sys.getcwd ()) f
else f
-
+
diff --git a/ide/preferences.ml b/ide/preferences.ml
index daa3839e0..bb35ed246 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -16,7 +16,7 @@ let pref_file = Filename.concat System.home ".coqiderc"
let accel_file = Filename.concat System.home ".coqide.keys"
-let mod_to_str (m:Gdk.Tags.modifier) =
+let mod_to_str (m:Gdk.Tags.modifier) =
match m with
| `MOD1 -> "MOD1"
| `MOD2 -> "MOD2"
@@ -34,19 +34,19 @@ let mod_to_str (m:Gdk.Tags.modifier) =
let (str_to_mod:string -> Gdk.Tags.modifier) =
function
- | "MOD1" -> `MOD1
- | "MOD2" -> `MOD2
- | "MOD3" -> `MOD3
- | "MOD4" -> `MOD4
- | "MOD5" -> `MOD5
- | "BUTTON1" -> `BUTTON1
- | "BUTTON2" -> `BUTTON2
- | "BUTTON3" -> `BUTTON3
- | "BUTTON4" -> `BUTTON4
- | "BUTTON5" -> `BUTTON5
- | "CONTROL" -> `CONTROL
- | "LOCK" -> `LOCK
- | "SHIFT" -> `SHIFT
+ | "MOD1" -> `MOD1
+ | "MOD2" -> `MOD2
+ | "MOD3" -> `MOD3
+ | "MOD4" -> `MOD4
+ | "MOD5" -> `MOD5
+ | "BUTTON1" -> `BUTTON1
+ | "BUTTON2" -> `BUTTON2
+ | "BUTTON3" -> `BUTTON3
+ | "BUTTON4" -> `BUTTON4
+ | "BUTTON5" -> `BUTTON5
+ | "CONTROL" -> `CONTROL
+ | "LOCK" -> `LOCK
+ | "SHIFT" -> `SHIFT
| s -> `MOD1
type pref =
@@ -103,7 +103,7 @@ type pref =
let use_default_doc_url = "(automatic)"
-let (current:pref ref) =
+let (current:pref ref) =
ref {
cmd_coqc = "coqc";
cmd_make = "make";
@@ -113,38 +113,38 @@ let (current:pref ref) =
global_auto_revert = false;
global_auto_revert_delay = 10000;
-
+
auto_save = true;
auto_save_delay = 10000;
auto_save_name = "#","#";
-
+
encoding_use_locale = true;
encoding_use_utf8 = false;
encoding_manual = "ISO_8859-1";
automatic_tactics = ["trivial"; "tauto"; "auto"; "omega";
"auto with *"; "intuition" ];
-
+
modifier_for_navigation = [`CONTROL; `MOD1];
modifier_for_templates = [`CONTROL; `SHIFT];
modifier_for_tactics = [`CONTROL; `MOD1];
modifier_for_display = [`MOD1;`SHIFT];
modifiers_valid = [`SHIFT; `CONTROL; `MOD1];
-
+
cmd_browse = Flags.browser_cmd_fmt;
cmd_editor = if Sys.os_type = "Win32" then "NOTEPAD %s" else "emacs %s";
-
+
(* text_font = Pango.Font.from_string "sans 12";*)
text_font = Pango.Font.from_string "Monospace 10";
doc_url = Coq_config.wwwrefman;
library_url = Coq_config.wwwstdlib;
-
+
show_toolbar = true;
contextual_menus_on_goal = true;
window_width = 800;
- window_height = 600;
+ window_height = 600;
query_window_width = 600;
query_window_height = 400;
fold_delay_ms = 400;
@@ -170,10 +170,10 @@ let contextual_menus_on_goal = ref (fun x -> ())
let resize_window = ref (fun () -> ())
let save_pref () =
- (try GtkData.AccelMap.save accel_file
+ (try GtkData.AccelMap.save accel_file
with _ -> ());
let p = !current in
- try
+ try
let add = Stringmap.add in
let (++) x f = f x in
Stringmap.empty ++
@@ -182,7 +182,7 @@ let save_pref () =
add "cmd_coqmakefile" [p.cmd_coqmakefile] ++
add "cmd_coqdoc" [p.cmd_coqdoc] ++
add "global_auto_revert" [string_of_bool p.global_auto_revert] ++
- add "global_auto_revert_delay"
+ add "global_auto_revert_delay"
[string_of_int p.global_auto_revert_delay] ++
add "auto_save" [string_of_bool p.auto_save] ++
add "auto_save_delay" [string_of_int p.auto_save_delay] ++
@@ -194,15 +194,15 @@ let save_pref () =
add "automatic_tactics" p.automatic_tactics ++
add "cmd_print" [p.cmd_print] ++
- add "modifier_for_navigation"
+ add "modifier_for_navigation"
(List.map mod_to_str p.modifier_for_navigation) ++
- add "modifier_for_templates"
+ add "modifier_for_templates"
(List.map mod_to_str p.modifier_for_templates) ++
- add "modifier_for_tactics"
+ add "modifier_for_tactics"
(List.map mod_to_str p.modifier_for_tactics) ++
- add "modifier_for_display"
+ add "modifier_for_display"
(List.map mod_to_str p.modifier_for_display) ++
- add "modifiers_valid"
+ add "modifiers_valid"
(List.map mod_to_str p.modifiers_valid) ++
add "cmd_browse" [p.cmd_browse] ++
add "cmd_editor" [p.cmd_editor] ++
@@ -212,7 +212,7 @@ let save_pref () =
add "doc_url" [p.doc_url] ++
add "library_url" [p.library_url] ++
add "show_toolbar" [string_of_bool p.show_toolbar] ++
- add "contextual_menus_on_goal"
+ add "contextual_menus_on_goal"
[string_of_bool p.contextual_menus_on_goal] ++
add "window_height" [string_of_int p.window_height] ++
add "window_width" [string_of_int p.window_width] ++
@@ -229,8 +229,8 @@ let save_pref () =
let load_pref () =
(try GtkData.AccelMap.load accel_file with _ -> ());
- let p = !current in
- try
+ 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 set k f = try let v = Stringmap.find k m in f v with _ -> () in
@@ -238,7 +238,7 @@ let load_pref () =
let set_bool k f = set_hd k (fun v -> f (bool_of_string v)) in
let set_int k f = set_hd k (fun v -> f (int_of_string v)) in
let set_pair k f = set k (function [v1;v2] -> f v1 v2 | _ -> raise Exit) in
- let set_command_with_pair_compat k f =
+ let set_command_with_pair_compat k f =
set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit)
in
set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v);
@@ -246,7 +246,7 @@ let load_pref () =
set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v);
set_hd "cmd_coqdoc" (fun v -> np.cmd_coqdoc <- v);
set_bool "global_auto_revert" (fun v -> np.global_auto_revert <- v);
- set_int "global_auto_revert_delay"
+ set_int "global_auto_revert_delay"
(fun v -> np.global_auto_revert_delay <- v);
set_bool "auto_save" (fun v -> np.auto_save <- v);
set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v);
@@ -257,15 +257,15 @@ let load_pref () =
set "automatic_tactics"
(fun v -> np.automatic_tactics <- v);
set_hd "cmd_print" (fun v -> np.cmd_print <- v);
- set "modifier_for_navigation"
+ set "modifier_for_navigation"
(fun v -> np.modifier_for_navigation <- List.map str_to_mod v);
- set "modifier_for_templates"
+ set "modifier_for_templates"
(fun v -> np.modifier_for_templates <- List.map str_to_mod v);
- set "modifier_for_tactics"
+ set "modifier_for_tactics"
(fun v -> np.modifier_for_tactics <- List.map str_to_mod v);
- set "modifier_for_display"
+ set "modifier_for_display"
(fun v -> np.modifier_for_display <- List.map str_to_mod v);
- set "modifiers_valid"
+ set "modifiers_valid"
(fun v -> np.modifiers_valid <- List.map str_to_mod v);
set_command_with_pair_compat "cmd_browse" (fun v -> np.cmd_browse <- v);
set_command_with_pair_compat "cmd_editor" (fun v -> np.cmd_editor <- v);
@@ -276,7 +276,7 @@ let load_pref () =
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_bool "contextual_menus_on_goal"
+ set_bool "contextual_menus_on_goal"
(fun v -> np.contextual_menus_on_goal <- v);
set_int "window_width" (fun v -> np.window_width <- v);
set_int "window_height" (fun v -> np.window_height <- v);
@@ -292,38 +292,38 @@ let load_pref () =
(*
Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
*)
- with e ->
+ with e ->
prerr_endline ("Could not load preferences ("^
(Printexc.to_string e)^").")
-
+
let split_string_format s =
- try
+ try
let i = Util.string_index_from s 0 "%s" in
let pre = (String.sub s 0 i) in
let post = String.sub s (i+2) (String.length s - i - 2) in
pre,post
with Not_found -> s,""
-let configure ?(apply=(fun () -> ())) () =
- let cmd_coqc =
+let configure ?(apply=(fun () -> ())) () =
+ let cmd_coqc =
string
- ~f:(fun s -> !current.cmd_coqc <- s)
+ ~f:(fun s -> !current.cmd_coqc <- s)
" coqc" !current.cmd_coqc in
- let cmd_make =
- string
+ let cmd_make =
+ string
~f:(fun s -> !current.cmd_make <- s)
" make" !current.cmd_make in
- let cmd_coqmakefile =
- string
+ let cmd_coqmakefile =
+ string
~f:(fun s -> !current.cmd_coqmakefile <- s)
"coqmakefile" !current.cmd_coqmakefile in
- let cmd_coqdoc =
- string
+ let cmd_coqdoc =
+ string
~f:(fun s -> !current.cmd_coqdoc <- s)
" coqdoc" !current.cmd_coqdoc in
- let cmd_print =
- string
- ~f:(fun s -> !current.cmd_print <- s)
+ let cmd_print =
+ string
+ ~f:(fun s -> !current.cmd_print <- s)
" Print ps" !current.cmd_print in
let config_font =
@@ -332,15 +332,15 @@ let configure ?(apply=(fun () -> ())) () =
w#set_preview_text
"Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
box#pack w#coerce;
- ignore (w#misc#connect#realize
- ~callback:(fun () -> w#set_font_name
+ 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 () ->
+ (fun () ->
let fd = w#font_name in
- !current.text_font <- (Pango.Font.from_string fd) ;
+ !current.text_font <- (Pango.Font.from_string fd) ;
(*
Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
*)
@@ -348,73 +348,73 @@ let configure ?(apply=(fun () -> ())) () =
true
in
(*
- let show_toolbar =
- bool
- ~f:(fun s ->
- !current.show_toolbar <- s;
- !show_toolbar s)
+ 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"
+ )
+ "Window height"
(string_of_int !current.window_height)
- in
+ in
let window_width =
string
- ~f:(fun s -> !current.window_width <-
- (try int_of_string s with _ -> 800))
- "Window width"
+ ~f:(fun s -> !current.window_width <-
+ (try int_of_string s with _ -> 800))
+ "Window width"
(string_of_int !current.window_width)
- in
+ in
*)
- let auto_complete =
- bool
- ~f:(fun s ->
- !current.auto_complete <- s;
- !auto_complete s)
+ let auto_complete =
+ bool
+ ~f:(fun s ->
+ !current.auto_complete <- s;
+ !auto_complete s)
"Auto Complete" !current.auto_complete
in
-(* let use_utf8_notation =
- bool
- ~f:(fun b ->
+(* let use_utf8_notation =
+ bool
+ ~f:(fun b ->
!current.use_utf8_notation <- b;
- )
+ )
"Use Unicode Notation: " !current.use_utf8_notation
in
-*)
+*)
(*
let config_appearance = [show_toolbar; window_width; window_height] in
*)
- let global_auto_revert =
- bool
- ~f:(fun s -> !current.global_auto_revert <- s)
+ let global_auto_revert =
+ bool
+ ~f:(fun s -> !current.global_auto_revert <- s)
"Enable global auto revert" !current.global_auto_revert
in
let global_auto_revert_delay =
string
- ~f:(fun s -> !current.global_auto_revert_delay <-
- (try int_of_string s with _ -> 10000))
- "Global auto revert delay (ms)"
+ ~f:(fun s -> !current.global_auto_revert_delay <-
+ (try int_of_string s with _ -> 10000))
+ "Global auto revert delay (ms)"
(string_of_int !current.global_auto_revert_delay)
- in
+ in
- let auto_save =
- bool
- ~f:(fun s -> !current.auto_save <- s)
+ 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)"
+ ~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
+ in
let fold_delay_ms =
string
@@ -429,7 +429,7 @@ let configure ?(apply=(fun () -> ())) () =
~f:(fun s -> !current.stop_before <- s)
"Stop interpreting before the current point" !current.stop_before
in
-
+
let lax_syntax =
bool
~f:(fun s -> !current.lax_syntax <- s)
@@ -448,31 +448,31 @@ let configure ?(apply=(fun () -> ())) () =
"Tabs on opposite side" !current.opposite_tabs
in
- let encodings =
- combo
+ let encodings =
+ combo
"File charset encoding "
- ~f:(fun s ->
+ ~f:(fun s ->
match s with
- | "UTF-8" ->
+ | "UTF-8" ->
!current.encoding_use_utf8 <- true;
!current.encoding_use_locale <- false
| "LOCALE" ->
!current.encoding_use_utf8 <- false;
!current.encoding_use_locale <- true
- | _ ->
+ | _ ->
!current.encoding_use_utf8 <- false;
!current.encoding_use_locale <- false;
!current.encoding_manual <- s;
)
~new_allowed: true
["UTF-8";"LOCALE";!current.encoding_manual]
- (if !current.encoding_use_utf8 then "UTF-8"
+ (if !current.encoding_use_utf8 then "UTF-8"
else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual)
in
- let help_string =
+ let help_string =
"Press a set of modifiers and an extra key together (needs then a restart to apply!)"
in
- let modifier_for_tactics =
+ let modifier_for_tactics =
modifiers
~allow:!current.modifiers_valid
~f:(fun l -> !current.modifier_for_tactics <- l)
@@ -480,7 +480,7 @@ let configure ?(apply=(fun () -> ())) () =
"Modifiers for Tactics Menu"
!current.modifier_for_tactics
in
- let modifier_for_templates =
+ let modifier_for_templates =
modifiers
~allow:!current.modifiers_valid
~f:(fun l -> !current.modifier_for_templates <- l)
@@ -488,7 +488,7 @@ let configure ?(apply=(fun () -> ())) () =
"Modifiers for Templates Menu"
!current.modifier_for_templates
in
- let modifier_for_navigation =
+ let modifier_for_navigation =
modifiers
~allow:!current.modifiers_valid
~f:(fun l -> !current.modifier_for_navigation <- l)
@@ -496,7 +496,7 @@ let configure ?(apply=(fun () -> ())) () =
"Modifiers for Navigation Menu"
!current.modifier_for_navigation
in
- let modifier_for_display =
+ let modifier_for_display =
modifiers
~allow:!current.modifiers_valid
~f:(fun l -> !current.modifier_for_display <- l)
@@ -504,23 +504,23 @@ let configure ?(apply=(fun () -> ())) () =
"Modifiers for Display Menu"
!current.modifier_for_display
in
- let modifiers_valid =
+ let modifiers_valid =
modifiers
~f:(fun l -> !current.modifiers_valid <- l)
"Allowed modifiers"
!current.modifiers_valid
in
- let cmd_editor =
+ let cmd_editor =
let predefined = [ "emacs %s"; "vi %s"; "NOTEPAD %s" ] in
combo
- ~help:"(%s for file name)"
+ ~help:"(%s for file name)"
"External editor"
~f:(fun s -> !current.cmd_editor <- s)
~new_allowed: true
(predefined@[if List.mem !current.cmd_editor predefined then ""
else !current.cmd_editor])
!current.cmd_editor
- in
+ in
let cmd_browse =
let predefined = [
Coq_config.browser;
@@ -530,15 +530,15 @@ let configure ?(apply=(fun () -> ())) () =
"seamonkey -remote \"openURL(%s)\" || seamonkey %s &";
"open -a Safari %s &"
] in
- combo
- ~help:"(%s for url)"
+ combo
+ ~help:"(%s for url)"
"Browser"
~f:(fun s -> !current.cmd_browse <- s)
~new_allowed: true
(predefined@[if List.mem !current.cmd_browse predefined then ""
else !current.cmd_browse])
!current.cmd_browse
- in
+ in
let doc_url =
let predefined = [
use_default_doc_url
@@ -550,7 +550,7 @@ let configure ?(apply=(fun () -> ())) () =
(predefined@[if List.mem !current.doc_url predefined then ""
else !current.doc_url])
!current.doc_url in
- let library_url =
+ let library_url =
let predefined = [
Coq_config.wwwstdlib
] in
@@ -561,26 +561,26 @@ let configure ?(apply=(fun () -> ())) () =
else !current.library_url])
!current.library_url
in
- let automatic_tactics =
+ let automatic_tactics =
strings
- ~f:(fun l -> !current.automatic_tactics <- l)
+ ~f:(fun l -> !current.automatic_tactics <- l)
~add:(fun () -> ["<edit me>"])
- "Wizard tactics to try in order"
+ "Wizard tactics to try in order"
!current.automatic_tactics
in
let contextual_menus_on_goal =
- bool
- ~f:(fun s ->
- !current.contextual_menus_on_goal <- s;
- !contextual_menus_on_goal s)
+ bool
+ ~f:(fun s ->
+ !current.contextual_menus_on_goal <- s;
+ !contextual_menus_on_goal s)
"Contextual menus on goal" !current.contextual_menus_on_goal
- in
+ in
let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax;
vertical_tabs;opposite_tabs] in
-
+
(* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
(shame on Benjamin) *)
let cmds =
@@ -590,7 +590,7 @@ let configure ?(apply=(fun () -> ())) () =
[global_auto_revert;global_auto_revert_delay;
auto_save; auto_save_delay; (* auto_save_name*)
encodings;
- ]);
+ ]);
(*
Section("Appearance",
config_appearance);
@@ -614,6 +614,6 @@ let configure ?(apply=(fun () -> ())) () =
(*
Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
*)
- match x with
+ match x with
| Return_apply | Return_ok -> save_pref ()
| Return_cancel -> ()
diff --git a/ide/tags.ml b/ide/tags.ml
index 89adad2c1..b0b9dc6fb 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -38,7 +38,7 @@ struct
let hypothesis = make_tag table ~name:"hypothesis" []
let goal = make_tag table ~name:"goal" []
end
-module Message =
+module Message =
struct
let table = GText.tag_table ()
let error = make_tag table ~name:"error" [`FOREGROUND "red"]
diff --git a/ide/typed_notebook.ml b/ide/typed_notebook.ml
index edc5c599c..39e8155d3 100644
--- a/ide/typed_notebook.ml
+++ b/ide/typed_notebook.ml
@@ -12,7 +12,7 @@ class ['a] typed_notebook default_build nb =
object(self)
inherit GPack.notebook nb as super
val mutable term_list = []
-
+
method append_term ?(build=default_build) (term:'a) =
let tab_label,menu_label,page = build term in
(* XXX - Temporary hack to compile with archaic lablgtk *)
diff --git a/ide/undo.ml b/ide/undo.ml
index d2fe81e1d..18c2f7a4d 100644
--- a/ide/undo.ml
+++ b/ide/undo.ml
@@ -10,16 +10,16 @@
open GText
open Ideutils
-type action =
- | Insert of string * int * int (* content*pos*length *)
- | Delete of string * int * int (* content*pos*length *)
+type action =
+ | Insert of string * int * int (* content*pos*length *)
+ | Delete of string * int * int (* content*pos*length *)
let neg act = match act with
| Insert (s,i,l) -> Delete (s,i,l)
| Delete (s,i,l) -> Insert (s,i,l)
class undoable_view (tv:[>Gtk.text_view] Gtk.obj) =
- let undo_lock = ref true in
+ let undo_lock = ref true in
object(self)
inherit GText.view tv as super
val history = (Stack.create () : action Stack.t)
@@ -29,25 +29,25 @@ object(self)
method private dump_debug =
if false (* !debug *) then begin
prerr_endline "==========Stack top=============";
- Stack.iter
+ 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) ->
+ | 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
+ 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) ->
+ | 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=========="
+ prerr_endline "==========Queue End=========="
end
@@ -57,16 +57,16 @@ object(self)
undo_lock := false;
prerr_endline "UNDO";
try begin
- let r =
+ let r =
match Stack.pop history with
- | Insert(s,p,l) as act ->
+ | Insert(s,p,l) as act ->
let start = self#buffer#get_iter_at_char p in
- (self#buffer#delete_interactive
+ (self#buffer#delete_interactive
~start
~stop:(start#forward_chars l)
()) or
(Stack.push act history; false)
- | Delete(s,p,l) as act ->
+ | 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)
@@ -75,11 +75,11 @@ object(self)
Queue.push act redo;
Stack.push act nredo
end;
- undo_lock := true;
+ undo_lock := true;
r
end
- with Stack.Empty ->
- undo_lock := true;
+ with Stack.Empty ->
+ undo_lock := true;
false
end else
(prerr_endline "UNDO DISCARDED"; true)
@@ -97,7 +97,7 @@ object(self)
end)
);
*)
- ignore (self#buffer#connect#insert_text
+ ignore (self#buffer#connect#insert_text
~callback:
(fun it s ->
if !undo_lock && not (Queue.is_empty redo) then begin
@@ -107,18 +107,18 @@ object(self)
Queue.clear redo;
end;
(* let pos = it#offset in
- if Stack.is_empty history or
+ if Stack.is_empty history or
s=" " or s="\t" or s="\n" or
- (match Stack.top history with
- | Insert(old,opos,olen) ->
+ (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,offset,len) ->
+ Stack.push
(Insert(olds^s,
offset,
len+(Glib.Utf8.length s)))
@@ -129,7 +129,7 @@ object(self)
));
ignore (self#buffer#connect#delete_range
~callback:
- (fun ~start ~stop ->
+ (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;
@@ -138,12 +138,12 @@ object(self)
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) ->
+ | Delete(old,opos,olen) ->
olen=1 or opos <> start_offset
| _ -> true
)
then
-*) Stack.push
+*) Stack.push
(Delete(s,
start_offset,
stop_offset - start_offset
@@ -151,27 +151,27 @@ object(self)
history
(* else begin
match Stack.pop history with
- | Delete(olds,offset,len) ->
- Stack.push
+ | 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 ?(buffer:GText.buffer option) =
- GtkText.View.make_params []
- ~cont:(GContainer.pack_container
+ GtkText.View.make_params []
+ ~cont:(GContainer.pack_container
~create:
- (fun pl -> let w = match buffer with
+ (fun pl -> let w = match buffer with
| None -> GtkText.View.create []
| Some b -> GtkText.View.create_with_buffer b#as_buffer
in
Gobject.set_params w pl; ((new undoable_view w):undoable_view)))
-
-
+
+
diff --git a/ide/undo_lablgtk_ge212.mli b/ide/undo_lablgtk_ge212.mli
index 916a06e92..32717fa8e 100644
--- a/ide/undo_lablgtk_ge212.mli
+++ b/ide/undo_lablgtk_ge212.mli
@@ -18,7 +18,7 @@ object
method clear_undo : unit
end
-val undoable_view :
+val undoable_view :
?buffer:GText.buffer ->
?editable:bool ->
?cursor_visible:bool ->
diff --git a/ide/undo_lablgtk_ge26.mli b/ide/undo_lablgtk_ge26.mli
index e949daafe..52bd67215 100644
--- a/ide/undo_lablgtk_ge26.mli
+++ b/ide/undo_lablgtk_ge26.mli
@@ -18,7 +18,7 @@ object
method clear_undo : unit
end
-val undoable_view :
+val undoable_view :
?buffer:GText.buffer ->
?editable:bool ->
?cursor_visible:bool ->
diff --git a/ide/undo_lablgtk_lt26.mli b/ide/undo_lablgtk_lt26.mli
index 82bcf2384..46ecfb1d7 100644
--- a/ide/undo_lablgtk_lt26.mli
+++ b/ide/undo_lablgtk_lt26.mli
@@ -18,7 +18,7 @@ object
method clear_undo : unit
end
-val undoable_view :
+val undoable_view :
?buffer:GText.buffer ->
?editable:bool ->
?cursor_visible:bool ->
diff --git a/ide/utf8_convert.mll b/ide/utf8_convert.mll
index c6e4b803b..82b305347 100644
--- a/ide/utf8_convert.mll
+++ b/ide/utf8_convert.mll
@@ -9,7 +9,7 @@
(* $Id$ *)
{
- open Lexing
+ open Lexing
let b = Buffer.create 127
}
@@ -24,16 +24,16 @@ rule entry = parse
| "\\x{" (short | long ) '}'
{ let s = lexeme lexbuf in
let n = String.length s in
- let code =
- try Glib.Utf8.from_unichar
- (int_of_string ("0x"^(String.sub s 3 (n - 4))))
+ let code =
+ try Glib.Utf8.from_unichar
+ (int_of_string ("0x"^(String.sub s 3 (n - 4))))
with _ -> s
in
let c = if Glib.Utf8.validate code then code else s in
Buffer.add_string b c;
entry lexbuf
}
- | _
+ | _
{ let s = lexeme lexbuf in
Buffer.add_string b s;
entry lexbuf}
diff --git a/ide/utils/configwin.mli b/ide/utils/configwin.mli
index 2d4dd4a78..386ef82af 100644
--- a/ide/utils/configwin.mli
+++ b/ide/utils/configwin.mli
@@ -248,7 +248,7 @@ val hotkey : ?editable: bool -> ?expand: bool -> ?help: string ->
val modifiers : ?editable: bool -> ?expand: bool -> ?help: string ->
?allow:(Gdk.Tags.modifier list) ->
- ?f: (Gdk.Tags.modifier list -> unit) ->
+ ?f: (Gdk.Tags.modifier list -> unit) ->
string -> Gdk.Tags.modifier list -> parameter_kind
(** [custom box f expand] creates a custom parameter, with
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 3ab3823de..ff74a3c33 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -810,13 +810,13 @@ class modifiers_param_box param =
()
in
let value = ref param.md_value in
- let _ =
+ let _ =
match param.md_help with
None -> ()
| Some help ->
let tooltips = GData.tooltips () in
ignore (hbox#connect#destroy ~callback: tooltips#destroy);
- tooltips#set_tip wev#coerce ~text: help ~privat: help
+ tooltips#set_tip wev#coerce ~text: help ~privat: help
in
let _ = we#set_text (Configwin_types.modifiers_to_string param.md_value) in
let mods_we_care = param.md_allow in
@@ -830,7 +830,7 @@ class modifiers_param_box param =
we#set_text (Configwin_types.modifiers_to_string !value);
false
in
- let _ =
+ let _ =
if param.md_editable then
ignore (we#event#connect#key_press capture)
else
@@ -1093,13 +1093,13 @@ let edit ?(with_apply=true)
(fun conf_struct -> new configuration_box tooltips conf_struct wnote)
conf_struct_list
in
-
+
if with_apply then
dialog#add_button Configwin_messages.mApply `APPLY;
-
+
dialog#add_button Configwin_messages.mOk `OK;
dialog#add_button Configwin_messages.mCancel `CANCEL;
-
+
let f_apply () =
List.iter (fun param_box -> param_box#apply) list_param_box ;
apply ()
@@ -1441,11 +1441,11 @@ let hotkey ?(editable=true) ?(expand=true) ?help ?(f=(fun _ -> ())) label v =
hk_expand = expand ;
}
-let modifiers
- ?(editable=true)
- ?(expand=true)
- ?help
- ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5])
+let modifiers
+ ?(editable=true)
+ ?(expand=true)
+ ?help
+ ?(allow=[`CONTROL;`SHIFT;`LOCK;`MOD1;`MOD1;`MOD2;`MOD3;`MOD4;`MOD5])
?(f=(fun _ -> ())) label v =
Modifiers_param
{
@@ -1456,7 +1456,7 @@ let modifiers
md_f_apply = f ;
md_expand = expand ;
md_allow = allow ;
- }
+ }
(** Create a custom param.*)
let custom ?label box f expand =
diff --git a/ide/utils/configwin_keys.ml b/ide/utils/configwin_keys.ml
index e1d7f33bb..9f44e5c6b 100644
--- a/ide/utils/configwin_keys.ml
+++ b/ide/utils/configwin_keys.ml
@@ -25,7 +25,7 @@
(** Key codes
- Ce fichier provient de X11/keysymdef.h
+ Ce fichier provient de X11/keysymdef.h
les noms des symboles deviennent : XK_ -> xk_
Thanks to Fabrice Le Fessant.
@@ -1334,11 +1334,11 @@ let xk_Thai_khokhai = 0xda2
let xk_Thai_khokhuat = 0xda3
let xk_Thai_khokhwai = 0xda4
let xk_Thai_khokhon = 0xda5
-let xk_Thai_khorakhang = 0xda6
-let xk_Thai_ngongu = 0xda7
-let xk_Thai_chochan = 0xda8
-let xk_Thai_choching = 0xda9
-let xk_Thai_chochang = 0xdaa
+let xk_Thai_khorakhang = 0xda6
+let xk_Thai_ngongu = 0xda7
+let xk_Thai_chochan = 0xda8
+let xk_Thai_choching = 0xda9
+let xk_Thai_chochang = 0xdaa
let xk_Thai_soso = 0xdab
let xk_Thai_chochoe = 0xdac
let xk_Thai_yoying = 0xdad
@@ -1380,39 +1380,39 @@ let xk_Thai_saraa = 0xdd0
let xk_Thai_maihanakat = 0xdd1
let xk_Thai_saraaa = 0xdd2
let xk_Thai_saraam = 0xdd3
-let xk_Thai_sarai = 0xdd4
-let xk_Thai_saraii = 0xdd5
-let xk_Thai_saraue = 0xdd6
-let xk_Thai_sarauee = 0xdd7
-let xk_Thai_sarau = 0xdd8
-let xk_Thai_sarauu = 0xdd9
+let xk_Thai_sarai = 0xdd4
+let xk_Thai_saraii = 0xdd5
+let xk_Thai_saraue = 0xdd6
+let xk_Thai_sarauee = 0xdd7
+let xk_Thai_sarau = 0xdd8
+let xk_Thai_sarauu = 0xdd9
let xk_Thai_phinthu = 0xdda
let xk_Thai_maihanakat_maitho = 0xdde
let xk_Thai_baht = 0xddf
-let xk_Thai_sarae = 0xde0
+let xk_Thai_sarae = 0xde0
let xk_Thai_saraae = 0xde1
let xk_Thai_sarao = 0xde2
-let xk_Thai_saraaimaimuan = 0xde3
-let xk_Thai_saraaimaimalai = 0xde4
+let xk_Thai_saraaimaimuan = 0xde3
+let xk_Thai_saraaimaimalai = 0xde4
let xk_Thai_lakkhangyao = 0xde5
let xk_Thai_maiyamok = 0xde6
let xk_Thai_maitaikhu = 0xde7
-let xk_Thai_maiek = 0xde8
+let xk_Thai_maiek = 0xde8
let xk_Thai_maitho = 0xde9
let xk_Thai_maitri = 0xdea
let xk_Thai_maichattawa = 0xdeb
let xk_Thai_thanthakhat = 0xdec
let xk_Thai_nikhahit = 0xded
-let xk_Thai_leksun = 0xdf0
-let xk_Thai_leknung = 0xdf1
-let xk_Thai_leksong = 0xdf2
+let xk_Thai_leksun = 0xdf0
+let xk_Thai_leknung = 0xdf1
+let xk_Thai_leksong = 0xdf2
let xk_Thai_leksam = 0xdf3
-let xk_Thai_leksi = 0xdf4
-let xk_Thai_lekha = 0xdf5
-let xk_Thai_lekhok = 0xdf6
-let xk_Thai_lekchet = 0xdf7
-let xk_Thai_lekpaet = 0xdf8
-let xk_Thai_lekkao = 0xdf9
+let xk_Thai_leksi = 0xdf4
+let xk_Thai_lekha = 0xdf5
+let xk_Thai_lekhok = 0xdf6
+let xk_Thai_lekchet = 0xdf7
+let xk_Thai_lekpaet = 0xdf8
+let xk_Thai_lekkao = 0xdf9
(*
diff --git a/ide/utils/configwin_types.ml b/ide/utils/configwin_types.ml
index 0def0b25d..bf2b74ee6 100644
--- a/ide/utils/configwin_types.ml
+++ b/ide/utils/configwin_types.ml
@@ -111,7 +111,7 @@ let modifiers_to_string m =
) ^ s)
in
iter m ""
-
+
let value_to_key v =
match v with
Raw.String s -> string_to_key s
@@ -233,7 +233,7 @@ type hotkey_param = {
type modifiers_param = {
md_label : string ; (** the label of the parameter *)
- mutable md_value : Gdk.Tags.modifier list ;
+ mutable md_value : Gdk.Tags.modifier list ;
(** The value, as a list of modifiers and a key code *)
md_editable : bool ; (** indicates if the value can be changed *)
md_f_apply : Gdk.Tags.modifier list -> unit ;
@@ -241,7 +241,7 @@ type modifiers_param = {
md_help : string option ; (** optional help string *)
md_expand : bool ; (** expand or not *)
md_allow : Gdk.Tags.modifier list
- }
+ }
let mk_custom_text_string_param (a : 'a string_param) : string string_param =
diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml
index 5441f4abe..1ab107c77 100644
--- a/ide/utils/editable_cells.ml
+++ b/ide/utils/editable_cells.ml
@@ -1,21 +1,21 @@
open GTree
open Gobject
-let create l =
+let create l =
let hbox = GPack.hbox () in
- let scw = GBin.scrolled_window
- ~hpolicy:`AUTOMATIC
- ~vpolicy:`AUTOMATIC
+ 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
+ in
(* populate the store *)
- let _ = List.iter (fun (x,y) ->
+ let _ = List.iter (fun (x,y) ->
let row = store#append () in
store#set ~row ~column:command_col x;
store#set ~row ~column:coq_col y)
@@ -27,61 +27,61 @@ let create l =
view#set_rules_hint true;
let renderer_comm = GTree.cell_renderer_text [`EDITABLE true] in
- ignore (renderer_comm#connect#edited
- ~callback:(fun (path:Gtk.tree_path) (s:string) ->
- store#set
- ~row:(store#get_iter path)
+ ignore (renderer_comm#connect#edited
+ ~callback:(fun (path:Gtk.tree_path) (s:string) ->
+ store#set
+ ~row:(store#get_iter path)
~column:command_col s));
- let first =
- GTree.view_column ~title:"Coq Command to try"
- ~renderer:(renderer_comm,["text",command_col])
- ()
+ let first =
+ GTree.view_column ~title:"Coq Command to try"
+ ~renderer:(renderer_comm,["text",command_col])
+ ()
in ignore (view#append_column first);
let renderer_coq = GTree.cell_renderer_text [`EDITABLE true] in
ignore(renderer_coq#connect#edited
- ~callback:(fun (path:Gtk.tree_path) (s:string) ->
- store#set
- ~row:(store#get_iter path)
+ ~callback:(fun (path:Gtk.tree_path) (s:string) ->
+ store#set
+ ~row:(store#get_iter path)
~column:coq_col s));
- let second =
- GTree.view_column ~title:"Coq Command to insert"
- ~renderer:(renderer_coq,["text",coq_col])
- ()
+ let second =
+ GTree.view_column ~title:"Coq Command to insert"
+ ~renderer:(renderer_coq,["text",coq_col])
+ ()
in ignore (view#append_column second);
- let vbox = GPack.button_box `VERTICAL ~packing:hbox#pack ~layout:`SPREAD ()
+ 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) ()
+ 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)
- ()
+ 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) ()
+ let remove = GButton.button ~stock:`REMOVE
+ ~label:"Remove"
+ ~packing:(vbox#pack ~expand:true ~fill:false) ()
in
- ignore (add#connect#clicked
- ~callback:(fun b ->
+ 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
+ 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
+ ignore (up#connect#clicked
+ ~callback:(fun b ->
+ match view#selection#get_selected_rows with
| [] -> ()
| path::_ ->
let iter = store#get_iter path in
@@ -89,9 +89,9 @@ let create l =
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
+ ignore (down#connect#clicked
+ ~callback:(fun b ->
+ match view#selection#get_selected_rows with
| [] -> ()
| path::_ ->
let iter = store#get_iter path in
@@ -100,13 +100,13 @@ let create l =
ignore (store#swap iter upiter)
with _ -> ()
));
- let get_data () =
+ 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 rec all acc =
let new_acc = (store#get ~row:start_iter ~column:command_col,
store#get ~row:start_iter ~column:coq_col)::acc
- in
+ in
if store#iter_next start_iter then all new_acc else List.rev new_acc
in all []
in
diff --git a/ide/utils/okey.mli b/ide/utils/okey.mli
index c8d48389c..84ea4df44 100644
--- a/ide/utils/okey.mli
+++ b/ide/utils/okey.mli
@@ -23,7 +23,7 @@
(* *)
(*********************************************************************************)
-(** Okey interface.
+(** Okey interface.
Once the lib is compiled and installed, you can use it by referencing
it with the [Okey] module. You must add [okey.cmo] or [okey.cmx]
@@ -35,7 +35,7 @@ type modifier = Gdk.Tags.modifier
(** Set the default modifier list. The first default value is [[]].*)
val set_default_modifiers : modifier list -> unit
-(** Set the default modifier mask. The first default value is
+(** Set the default modifier mask. The first default value is
[[`MOD2 ; `MOD3 ; `MOD4 ; `MOD5 ; `LOCK]].
The mask defines the modifiers not taken into account
when looking for the handler of a key press event.
@@ -48,67 +48,67 @@ val set_default_mask : modifier list -> unit
@param remove when true, the previous handlers for the given key and modifier
list are not kept.
@param cond this function is a guard: the [callback] function is not called
- if the [cond] function returns [false].
+ if the [cond] function returns [false].
The default [cond] function always returns [true].
@param mods the list of modifiers. If not given, the default modifiers
- are used.
+ are used.
You can set the default modifiers with function {!Okey.set_default_modifiers}.
@param mask the list of modifiers which must not be taken
into account to trigger the given handler. [mods]
and [mask] must not have common modifiers. If not given, the default mask
- is used.
+ is used.
You can set the default modifiers mask with function {!Okey.set_default_mask}.
*)
val add :
< connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
- event : GObj.event_ops; get_oid : int; .. > ->
- ?cond: (unit -> bool) ->
- ?mods: modifier list ->
- ?mask: modifier list ->
- Gdk.keysym ->
- (unit -> unit) ->
+ event : GObj.event_ops; get_oid : int; .. > ->
+ ?cond: (unit -> bool) ->
+ ?mods: modifier list ->
+ ?mask: modifier list ->
+ Gdk.keysym ->
+ (unit -> unit) ->
unit
(** It calls {!Okey.add} for each given key.*)
-val add_list :
+val add_list :
< connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
- event : GObj.event_ops; get_oid : int; .. > ->
- ?cond: (unit -> bool) ->
- ?mods: modifier list ->
- ?mask: modifier list ->
- Gdk.keysym list ->
- (unit -> unit) ->
+ event : GObj.event_ops; get_oid : int; .. > ->
+ ?cond: (unit -> bool) ->
+ ?mods: modifier list ->
+ ?mask: modifier list ->
+ Gdk.keysym list ->
+ (unit -> unit) ->
unit
-
+
(** Like {!Okey.add} but the previous handlers for the
given modifiers and key are not kept.*)
val set :
< connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
- event : GObj.event_ops; get_oid : int; .. > ->
- ?cond: (unit -> bool) ->
- ?mods: modifier list ->
- ?mask: modifier list ->
- Gdk.keysym ->
- (unit -> unit) ->
+ event : GObj.event_ops; get_oid : int; .. > ->
+ ?cond: (unit -> bool) ->
+ ?mods: modifier list ->
+ ?mask: modifier list ->
+ Gdk.keysym ->
+ (unit -> unit) ->
unit
(** It calls {!Okey.set} for each given key.*)
-val set_list :
+val set_list :
< connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
event : GObj.event_ops; get_oid : int; .. > ->
- ?cond: (unit -> bool) ->
- ?mods: modifier list ->
- ?mask: modifier list ->
- Gdk.keysym list ->
- (unit -> unit) ->
+ ?cond: (unit -> bool) ->
+ ?mods: modifier list ->
+ ?mask: modifier list ->
+ Gdk.keysym list ->
+ (unit -> unit) ->
unit
(** Remove the handlers associated to the given widget.
This is automatically done when a widget is destroyed but
you can do it yourself. *)
-val remove_widget :
+val remove_widget :
< connect : < destroy : callback: (unit -> unit) -> GtkSignal.id; .. >;
event : GObj.event_ops; get_oid : int; .. > ->
unit ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-25 00:30:35 +0000