aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/config_lexer.mli10
-rw-r--r--ide/coq_commands.mli11
-rw-r--r--ide/coq_lex.mli11
-rw-r--r--ide/coq_lex.mll4
-rw-r--r--ide/coqide_main.ml43
-rw-r--r--ide/coqide_main.mli10
-rw-r--r--ide/coqide_ui.mli10
-rw-r--r--ide/gtk_parsing.ml109
-rw-r--r--ide/gtk_parsing.mli26
-rw-r--r--ide/ide_slave.mli10
-rw-r--r--ide/macos_prehook.mli10
-rw-r--r--ide/nanoPG.mli11
-rw-r--r--ide/utf8_convert.mli9
-rw-r--r--ide/wg_Find.ml61
14 files changed, 174 insertions, 121 deletions
diff --git a/ide/config_lexer.mli b/ide/config_lexer.mli
new file mode 100644
index 000000000..0c0c5d1e7
--- /dev/null
+++ b/ide/config_lexer.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val print_file : string -> string list Util.String.Map.t -> unit
+val load_file : string -> string list Util.String.Map.t
diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli
new file mode 100644
index 000000000..53026be38
--- /dev/null
+++ b/ide/coq_commands.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val tactics : string list list
+val commands : string list list
+val state_preserving : string list
diff --git a/ide/coq_lex.mli b/ide/coq_lex.mli
new file mode 100644
index 000000000..417e0a76f
--- /dev/null
+++ b/ide/coq_lex.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val delimit_sentences : (int -> GText.tag -> unit) -> string -> unit
+
+exception Unterminated
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index 8bfd937e3..a7e9003db 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -17,7 +17,9 @@
let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *)
-let undotted_sep = '{' | '}' | '-'+ | '+'+ | '*'+
+let number = [ '0'-'9' ]+
+
+let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+
let dot_sep = '.' (space | eof)
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 8d99cc3e6..6e330c62b 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -55,6 +55,8 @@ let os_specific_init () = ()
(** Win32 *)
+IFDEF WIN32 THEN
+
(* On win32, we add the directory of coqide to the PATH at launch-time
(this used to be done in a .bat script). *)
@@ -86,7 +88,6 @@ let reroute_stdout_stderr () =
(* We also provide specific kill and interrupt functions. *)
-IFDEF WIN32 THEN
external win32_kill : int -> unit = "win32_kill"
external win32_interrupt : int -> unit = "win32_interrupt"
let () =
diff --git a/ide/coqide_main.mli b/ide/coqide_main.mli
new file mode 100644
index 000000000..e1555ba2e
--- /dev/null
+++ b/ide/coqide_main.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+ that does not have a corresponding .mli file *)
diff --git a/ide/coqide_ui.mli b/ide/coqide_ui.mli
new file mode 100644
index 000000000..9f6fa5635
--- /dev/null
+++ b/ide/coqide_ui.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val init : unit -> unit
+val ui_m : GAction.ui_manager
diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml
index f0575e325..7c0a7495a 100644
--- a/ide/gtk_parsing.ml
+++ b/ide/gtk_parsing.ml
@@ -7,11 +7,7 @@
(************************************************************************)
let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0)
-let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0)
let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0)
-let bn = Glib.Utf8.to_unichar "\n" ~pos:(ref 0)
-let space = Glib.Utf8.to_unichar " " ~pos:(ref 0)
-let tab = Glib.Utf8.to_unichar "\t" ~pos:(ref 0)
(* TODO: avoid num and prime at the head of a word *)
@@ -30,17 +26,6 @@ let ends_word (it:GText.iter) =
not (is_word_char c)
)
-
-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 find_word_start (it:GText.iter) =
let rec step_to_start it =
Minilib.log "Find word start";
@@ -72,100 +57,6 @@ let get_word_around (it:GText.iter) =
let stop = find_word_end it in
start,stop
-
-let rec complete_backward w (it:GText.iter) =
- Minilib.log "Complete backward...";
- match it#backward_search w with
- | None -> (Minilib.log "backward_search failed";None)
- | Some (start,stop) ->
- Minilib.log ("complete_backward got a match:"^(string_of_int start#offset)^(string_of_int stop#offset));
- 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) =
- Minilib.log "Complete forward...";
- match it#forward_search w with
- | None -> None
- | Some (start,stop) ->
- if starts_word start then
- let ne = find_word_end stop in
- if ne#compare stop = 0 then
- complete_forward w stop
- else Some (stop,stop,ne)
- else complete_forward w stop
-
-
-let find_comment_end (start:GText.iter) =
- let rec find_nested_comment (search_start:GText.iter) (search_end:GText.iter) (comment_end:GText.iter) =
- match (search_start#forward_search ~limit:search_end "(*"),(comment_end#forward_search "*)") with
- | None,_ -> comment_end
- | Some _, None -> raise Not_found
- | Some (_,next_search_start),Some (next_search_end,next_comment_end) ->
- find_nested_comment next_search_start next_search_end next_comment_end
- in
- match start#forward_search "*)" with
- | None -> raise Not_found
- | Some (search_end,comment_end) -> find_nested_comment start search_end comment_end
-
-
-let rec find_string_end (start:GText.iter) =
- let dblquote = int_of_char '"' in
- let rec escaped_dblquote c =
- (c#char = dblquote) && not (escaped_dblquote c#backward_char)
- in
- match start#forward_search "\"" with
- | None -> raise Not_found
- | Some (stop,next_start) ->
- if escaped_dblquote stop#backward_char
- then find_string_end next_start
- else next_start
-
-
-let rec find_next_sentence (from:GText.iter) =
- match (from#forward_search ".") with
- | None -> raise Not_found
- | Some (non_vernac_search_end,next_sentence) ->
- match from#forward_search ~limit:non_vernac_search_end "(*",from#forward_search ~limit:non_vernac_search_end "\"" with
- | None,None ->
- if Glib.Unichar.isspace next_sentence#char || next_sentence#compare next_sentence#forward_char == 0
- then next_sentence else find_next_sentence next_sentence
- | None,Some (_,string_search_start) -> find_next_sentence (find_string_end string_search_start)
- | Some (_,comment_search_start),None -> find_next_sentence (find_comment_end comment_search_start)
- | Some (_,comment_search_start),Some (_,string_search_start) ->
- find_next_sentence (
- if comment_search_start#compare string_search_start < 0
- then find_comment_end comment_search_start
- else find_string_end string_search_start)
-
-
-let find_nearest_forward (cursor:GText.iter) targets =
- let fold_targets acc target =
- match cursor#forward_search target,acc with
- | Some (t_start,_),Some nearest when (t_start#compare nearest < 0) -> Some t_start
- | Some (t_start,_),None -> Some t_start
- | _ -> acc
- in
- match List.fold_left fold_targets None targets with
- | None -> raise Not_found
- | Some nearest -> nearest
-
-
-let find_nearest_backward (cursor:GText.iter) targets =
- let fold_targets acc target =
- match cursor#backward_search target,acc with
- | Some (t_start,_),Some nearest when (t_start#compare nearest > 0) -> Some t_start
- | Some (t_start,_),None -> Some t_start
- | _ -> acc
- in
- match List.fold_left fold_targets None targets with
- | None -> raise Not_found
- | Some nearest -> nearest
-
(** On double-click on a view, select the whole word. This is a workaround for
a deficient word handling in TextView. *)
let fix_double_click self =
diff --git a/ide/gtk_parsing.mli b/ide/gtk_parsing.mli
new file mode 100644
index 000000000..b54f731b3
--- /dev/null
+++ b/ide/gtk_parsing.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val fix_double_click :
+ < buffer : < get_iter : [> `INSERT ] -> GText.iter;
+ move_mark : [> `INSERT | `SEL_BOUND ] ->
+ where:GText.iter -> unit;
+ .. >;
+ event : < connect :
+ < button_press :
+ callback:([> `TWO_BUTTON_PRESS ] Gdk.event ->
+ bool) ->
+ 'a;
+ .. >;
+ .. >;
+ .. > ->
+ unit
+val starts_word : GText.iter -> bool
+val ends_word : GText.iter -> bool
+val find_word_start : GText.iter -> GText.iter
+val find_word_end : GText.iter -> GText.iter
diff --git a/ide/ide_slave.mli b/ide/ide_slave.mli
new file mode 100644
index 000000000..e1555ba2e
--- /dev/null
+++ b/ide/ide_slave.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+ that does not have a corresponding .mli file *)
diff --git a/ide/macos_prehook.mli b/ide/macos_prehook.mli
new file mode 100644
index 000000000..e1555ba2e
--- /dev/null
+++ b/ide/macos_prehook.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+ that does not have a corresponding .mli file *)
diff --git a/ide/nanoPG.mli b/ide/nanoPG.mli
new file mode 100644
index 000000000..3ad8435b5
--- /dev/null
+++ b/ide/nanoPG.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val get_documentation : unit -> string
+val init : GWindow.window -> Session.session Wg_Notebook.typed_notebook ->
+ GAction.action_group list -> unit
diff --git a/ide/utf8_convert.mli b/ide/utf8_convert.mli
new file mode 100644
index 000000000..06a131a68
--- /dev/null
+++ b/ide/utf8_convert.mli
@@ -0,0 +1,9 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+val f : string -> string
diff --git a/ide/wg_Find.ml b/ide/wg_Find.ml
index a62ff2de5..cb182465a 100644
--- a/ide/wg_Find.ml
+++ b/ide/wg_Find.ml
@@ -84,8 +84,10 @@ class finder name (view : GText.view) =
method private backward_search starti =
let text = view#buffer#start_iter#get_text ~stop:starti in
let regexp = self#regex in
- try
- let i = Str.search_backward regexp text (String.length text - 1) in
+ let offs = (String.length text - 1) in
+ if offs < 0 then None
+ else try
+ let i = Str.search_backward regexp text offs in
let j = Str.match_end () in
Some(view#buffer#start_iter#forward_chars (b2c text i),
view#buffer#start_iter#forward_chars (b2c text j))
@@ -101,24 +103,33 @@ class finder name (view : GText.view) =
with Not_found -> None
method replace_all () =
- let rec replace_at (iter : GText.iter) =
+ let rec replace_at (iter : GText.iter) ct tot =
let found = self#forward_search iter in
match found with
- | None -> ()
+ | None ->
+ let tot_str = if Int.equal ct tot then "" else " of " ^ string_of_int tot in
+ let occ_str = CString.plural tot "occurrence" in
+ let _ = Ideutils.flash_info ("Replaced " ^ string_of_int ct ^ tot_str ^ " " ^ occ_str) in
+ ()
| Some (start, stop) ->
let text = iter#get_text ~stop:view#buffer#end_iter in
let start_mark = view#buffer#create_mark start in
let stop_mark = view#buffer#create_mark ~left_gravity:false stop in
+ let mod_save = view#buffer#modified in
+ let _ = view#buffer#set_modified false in
let _ = view#buffer#delete_interactive ~start ~stop () in
let iter = view#buffer#get_iter_at_mark (`MARK start_mark) in
- let _ = view#buffer#insert_interactive ~iter (self#replacement text)in
+ let _ = view#buffer#insert_interactive ~iter (self#replacement text) in
+ let edited = view#buffer#modified in
+ let _ = view#buffer#set_modified (edited || mod_save) in
let next = view#buffer#get_iter_at_mark (`MARK stop_mark) in
let () = view#buffer#delete_mark (`MARK start_mark) in
let () = view#buffer#delete_mark (`MARK stop_mark) in
- replace_at next
+ let next_ct = if edited then ct + 1 else ct in
+ replace_at next next_ct (tot + 1)
in
let () = view#buffer#begin_user_action () in
- let () = replace_at view#buffer#start_iter in
+ let () = replace_at view#buffer#start_iter 0 0 in
view#buffer#end_user_action ()
method private set_not_found () =
@@ -130,22 +141,52 @@ class finder name (view : GText.view) =
method private set_normal () =
find_entry#misc#modify_base [`NORMAL, `NAME "white"]
- method private find_from backward (starti : GText.iter) =
+ method private find_from backward ?(wrapped=false) (starti : GText.iter) =
let found =
if backward then self#backward_search starti
else self#forward_search starti in
match found with
| None ->
if not backward && not (starti#equal view#buffer#start_iter) then
- self#find_from backward view#buffer#start_iter
+ self#find_from backward ~wrapped:true view#buffer#start_iter
else if backward && not (starti#equal view#buffer#end_iter) then
- self#find_from backward view#buffer#end_iter
+ self#find_from backward ~wrapped:true view#buffer#end_iter
else
+ let _ = Ideutils.flash_info "String not found" in
self#set_not_found ()
| Some (start, stop) ->
+ let text = view#buffer#start_iter#get_text ~stop:view#buffer#end_iter in
+ let rec find_all offs accum =
+ if offs > String.length text then
+ List.rev accum
+ else try
+ let i = Str.search_forward self#regex text offs in
+ let j = Str.match_end () in
+ find_all (j + 1) (i :: accum)
+ with Not_found -> List.rev accum
+ in
+ let occurs = find_all 0 [] in
+ let num_occurs = List.length occurs in
+ (* assoc table of offset, occurrence index pairs *)
+ let occur_tbl = List.mapi (fun ndx occ -> (occ,ndx+1)) occurs in
let _ = view#buffer#select_range start stop in
let scroll = `MARK (view#buffer#create_mark stop) in
let _ = view#scroll_to_mark ~use_align:false scroll in
+ let _ =
+ try
+ let occ_ndx = List.assoc start#offset occur_tbl in
+ let occ_str = CString.plural num_occurs "occurrence" in
+ let wrap_str = if wrapped then
+ if backward then " (wrapped backwards)"
+ else " (wrapped)"
+ else ""
+ in
+ Ideutils.flash_info
+ (string_of_int occ_ndx ^ " of " ^ string_of_int num_occurs ^
+ " " ^ occ_str ^ wrap_str)
+ with Not_found ->
+ CErrors.anomaly (Pp.str "Occurrence of Find string not in table")
+ in
self#set_found ()
method find_forward () =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 12:41:36 +0000