diff options
Diffstat (limited to 'ide')
-rw-r--r-- | ide/config_lexer.mli | 10 | ||||
-rw-r--r-- | ide/coq_commands.mli | 11 | ||||
-rw-r--r-- | ide/coq_lex.mli | 11 | ||||
-rw-r--r-- | ide/coq_lex.mll | 10 | ||||
-rw-r--r-- | ide/coqide.ml | 11 | ||||
-rw-r--r-- | ide/coqide_main.ml4 | 3 | ||||
-rw-r--r-- | ide/coqide_main.mli | 10 | ||||
-rw-r--r-- | ide/coqide_ui.mli | 10 | ||||
-rw-r--r-- | ide/gtk_parsing.ml | 109 | ||||
-rw-r--r-- | ide/gtk_parsing.mli | 26 | ||||
-rw-r--r-- | ide/ide_slave.ml | 10 | ||||
-rw-r--r-- | ide/ide_slave.mli | 10 | ||||
-rw-r--r-- | ide/ideutils.ml | 7 | ||||
-rw-r--r-- | ide/ideutils.mli | 2 | ||||
-rw-r--r-- | ide/macos_prehook.mli | 10 | ||||
-rw-r--r-- | ide/nanoPG.mli | 11 | ||||
-rw-r--r-- | ide/session.ml | 5 | ||||
-rw-r--r-- | ide/utf8_convert.mli | 9 | ||||
-rw-r--r-- | ide/wg_Find.ml | 61 |
19 files changed, 201 insertions, 135 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..fcc242e07 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -17,7 +17,13 @@ let space = [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *) -let undotted_sep = '{' | '}' | '-'+ | '+'+ | '*'+ +let number = [ '0'-'9' ]+ + +let string = "\"" _+ "\"" + +let undotted_sep = (number space* ':' space*)? '{' | '}' | '-'+ | '+'+ | '*'+ + +let vernac_control = "Fail" | "Time" | "Redirect" space+ string | "Timeout" space+ number let dot_sep = '.' (space | eof) @@ -65,7 +71,7 @@ and sentence initial stamp = parse stamp (utf8_lexeme_start lexbuf) Tags.Script.sentence; sentence true stamp lexbuf } - | undotted_sep { + | (vernac_control space+)* undotted_sep { (* Separators like { or } and bullets * - + are only active at the start of a sentence *) if initial then stamp (utf8_lexeme_start lexbuf + String.length (Lexing.lexeme lexbuf) - 1) Tags.Script.sentence; diff --git a/ide/coqide.ml b/ide/coqide.ml index 842d06859..3cc46b6aa 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1221,9 +1221,14 @@ let build_ui () = (* Emacs/PG mode *) NanoPG.init w notebook all_menus; - (* Reset on tab switch *) - let _ = notebook#connect#switch_page ~callback:(fun _ -> - if reset_on_tab_switch#get then Nav.restart ()) + (* On tab switch, reset, update location *) + let _ = notebook#connect#switch_page ~callback:(fun n -> + let _ = if reset_on_tab_switch#get then Nav.restart () in + try + let session = notebook#get_nth_term n in + let ins = session.buffer#get_iter_at_mark `INSERT in + Ideutils.display_location ins + with _ -> ()) in (* Vertical Separator between Scripts and Goals *) 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.ml b/ide/ide_slave.ml index 5f40a2242..6d1064d25 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -454,9 +454,11 @@ let slave_feeder fmt xml_oc msg = let msg_format = ref (fun () -> let margin = Option.default 72 (Topfmt.get_margin ()) in Xmlprotocol.Richpp margin -) + ) -let loop doc = +(* The loop ignores the command line arguments as the current model delegates + its handing to the toplevel container. *) +let loop _args doc = set_doc doc; init_signal_handler (); catch_break := false; @@ -504,8 +506,8 @@ let rec parse = function | x :: rest -> x :: parse rest | [] -> [] -let () = Coqtop.toploop_init := (fun args -> - let args = parse args in +let () = Coqtop.toploop_init := (fun coq_args extra_args -> + let args = parse extra_args in Flags.quiet := true; CoqworkmgrApi.(init High); args) 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/ideutils.ml b/ide/ideutils.ml index 0977a1890..9c5b06a0d 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -69,6 +69,12 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let set_location = ref (function s -> failwith "not ready") +let display_location ins = + let line = ins#line + 1 in + let off = ins#line_offset + 1 in + let msg = Printf.sprintf "Line: %5d Char: %3d" line off in + !set_location msg + (** A utf8 char is either a single byte (ascii char, 0xxxxxxx) or multi-byte (with a leading byte 11xxxxxx and extra bytes 10xxxxxx) *) @@ -465,4 +471,3 @@ let browse_keyword prerr text = let u = Lazy.force url_for_keyword text in browse prerr (doc_url() ^ u) with Not_found -> prerr ("No documentation found for \""^text^"\".\n") - diff --git a/ide/ideutils.mli b/ide/ideutils.mli index f06a48aeb..99ff763e2 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -56,6 +56,7 @@ val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list -> #GText.buffer_skel -> Richpp.richpp -> unit val set_location : (string -> unit) ref +val display_location : GText.iter -> unit (* In win32, when a command-line is to be executed via cmd.exe (i.e. Sys.command, Unix.open_process, ...), it cannot contain several @@ -95,4 +96,3 @@ val io_read_all : Glib.Io.channel -> string val run_command : (string -> unit) -> (Unix.process_status -> unit) -> string -> unit - 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/session.ml b/ide/session.ml index 0a09cc9f5..8dada8ff2 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -209,10 +209,7 @@ let set_buffer_handlers let mark_set_cb it m = debug_edit_zone (); let ins = get_insert () in - let line = ins#line + 1 in - let off = ins#line_offset + 1 in - let msg = Printf.sprintf "Line: %5d Char: %3d" line off in - let () = !Ideutils.set_location msg in + let () = Ideutils.display_location ins in match GtkText.Mark.get_name m with | Some "insert" -> () | Some s -> Minilib.log (s^" moved") 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 () = |