aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml6
-rw-r--r--ide/coqide.ml4
-rw-r--r--ide/ideutils.ml19
-rw-r--r--ide/ideutils.mli1
-rw-r--r--ide/preferences.ml57
-rw-r--r--ide/preferences.mli2
-rw-r--r--ide/session.ml28
7 files changed, 28 insertions, 89 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 91cd448eda..e7eea4ced2 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -119,7 +119,7 @@ let rec filter_coq_opts args =
and asks_for_coqtop args =
let pb_mes = GWindow.message_dialog
- ~message:"Failed to load coqtop. Reset the preference to default ?"
+ ~message:"Failed to load coqidetop. Reset the preference to default ?"
~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
match pb_mes#run () with
| `YES ->
@@ -130,7 +130,7 @@ and asks_for_coqtop args =
| `DELETE_EVENT | `NO ->
let () = pb_mes#destroy () in
let cmd_sel = GWindow.file_selection
- ~title:"Coqtop to execute (edit your preference then)"
+ ~title:"coqidetop to execute (edit your preference then)"
~filename:(coqtop_path ()) ~urgency_hint:true () in
match cmd_sel#run () with
| `OK ->
@@ -419,7 +419,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
let title = "Warning" in
let icon = (warn_image ())#coerce in
let buttons = ["Reset"; "Save all and quit"; "Quit without saving"] in
- let ans = GToolbox.question_box ~title ~buttons ~icon "Coqtop died badly." in
+ let ans = GToolbox.question_box ~title ~buttons ~icon "coqidetop died badly." in
if ans = 2 then (!save_all (); GtkMain.Main.quit ())
else if ans = 3 then GtkMain.Main.quit ()
| Planned -> ()
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 48c08899e0..94778e0c60 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1182,10 +1182,10 @@ let build_ui () =
item "Help" ~label:"_Help";
item "Browse Coq Manual" ~label:"Browse Coq _Manual"
~callback:(fun _ ->
- browse notebook#current_term.messages#default_route#add_string (doc_url ()));
+ browse notebook#current_term.messages#default_route#add_string Coq_config.wwwrefman);
item "Browse Coq Library" ~label:"Browse Coq _Library"
~callback:(fun _ ->
- browse notebook#current_term.messages#default_route#add_string library_url#get);
+ browse notebook#current_term.messages#default_route#add_string Coq_config.wwwstdlib);
item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
~callback:(fun _ -> on_current_term (fun sn ->
browse_keyword sn.messages#default_route#add_string (get_current_word sn)));
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index c14af7d21d..5beaba3604 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -458,15 +458,6 @@ let browse prerr url =
in
run_command (fun _ -> ()) finally com
-let doc_url () =
- if doc_url#get = use_default_doc_url || doc_url#get = ""
- then
- let addr = List.fold_left Filename.concat (Envars.docdir ())
- ["html";"refman";"index.html"]
- in
- if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman
- else doc_url#get
-
let url_for_keyword =
let ht = Hashtbl.create 97 in
lazy (
@@ -476,13 +467,7 @@ let url_for_keyword =
(fun x -> Sys.file_exists (Filename.concat x "index_urls.txt"))
(Minilib.coqide_data_dirs ())) "index_urls.txt" in
open_in index_urls
- with Not_found ->
- let doc_url = doc_url () in
- let n = String.length doc_url in
- if n > 8 && String.sub doc_url 0 7 = "file://" then
- open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt")
- else
- raise Exit
+ with Not_found -> raise Exit
in
try while true do
let s = input_line cin in
@@ -503,7 +488,7 @@ let url_for_keyword =
let browse_keyword prerr text =
try
let u = Lazy.force url_for_keyword text in
- browse prerr (doc_url() ^ u)
+ browse prerr (Coq_config.wwwrefman ^ u)
with Not_found -> prerr ("No documentation found for \""^text^"\".\n")
let rec is_valid (s : Pp.t) = match Pp.repr s with
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 0031c59c17..531c71cd4b 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -13,7 +13,6 @@ val warning : string -> unit
val cb : GData.clipboard
-val doc_url : unit -> string
val browse : (string -> unit) -> string -> unit
val browse_keyword : (string -> unit) -> string -> unit
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 4aa8c92f73..fb0eea1405 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -366,33 +366,6 @@ let text_font =
in
new preference ~name:["text_font"] ~init ~repr:Repr.(string)
-let is_standard_doc_url url =
- let wwwcompatprefix = "http://www.lix.polytechnique.fr/coq/" in
- let n = String.length Coq_config.wwwcoq in
- let n' = String.length Coq_config.wwwrefman in
- url = Coq_config.localwwwrefman ||
- url = Coq_config.wwwrefman ||
- url = wwwcompatprefix ^ String.sub Coq_config.wwwrefman n (n'-n)
-
-let doc_url =
-object
- inherit [string] preference
- ~name:["doc_url"] ~init:Coq_config.wwwrefman ~repr:Repr.(string)
- as super
-
- method! set v =
- if not (is_standard_doc_url v) &&
- v <> use_default_doc_url &&
- (* Extra hack to support links to last released doc version *)
- v <> Coq_config.wwwcoq ^ "doc" &&
- v <> Coq_config.wwwcoq ^ "doc/"
- then super#set v
-
-end
-
-let library_url =
- new preference ~name:["library_url"] ~init:Coq_config.wwwstdlib ~repr:Repr.(string)
-
let show_toolbar =
new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool)
@@ -692,7 +665,7 @@ let configure ?(apply=(fun () -> ())) parent =
let cmd_coqtop =
string
~f:(fun s -> cmd_coqtop#set (if s = "AUTO" then None else Some s))
- " coqtop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in
+ " coqidetop" (match cmd_coqtop#get with |None -> "AUTO" | Some x -> x) in
let cmd_coqc = pstring " coqc" cmd_coqc in
let cmd_make = pstring " make" cmd_make in
let cmd_coqmakefile = pstring "coqmakefile" cmd_coqmakefile in
@@ -948,32 +921,6 @@ let configure ?(apply=(fun () -> ())) parent =
else cmd_browse#get])
cmd_browse#get
in
- let doc_url =
- let predefined = [
- "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["refman";"html"]);
- Coq_config.wwwrefman;
- use_default_doc_url
- ] in
- combo
- "Manual URL"
- ~f:doc_url#set
- ~new_allowed: true
- (predefined@[if List.mem doc_url#get predefined then ""
- else doc_url#get])
- doc_url#get in
- let library_url =
- let predefined = [
- "file://"^(List.fold_left Filename.concat (Envars.docdir ()) ["stdlib";"html"]);
- Coq_config.wwwstdlib
- ] in
- combo
- "Library URL"
- ~f:(fun s -> library_url#set s)
- ~new_allowed: true
- (predefined@[if List.mem library_url#get predefined then ""
- else library_url#get])
- library_url#get
- in
let automatic_tactics =
strings
~f:automatic_tactics#set
@@ -1039,7 +986,7 @@ let configure ?(apply=(fun () -> ())) parent =
Section("Appearance", Some `PREFERENCES, [window_width; window_height]);
Section("Externals", None,
[cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
- cmd_print;cmd_editor;cmd_browse;doc_url;library_url]);
+ cmd_print;cmd_editor;cmd_browse]);
Section("Tactics Wizard", None,
[automatic_tactics]);
Section("Shortcuts", Some `PREFERENCES,
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 7ed6a40bdb..cf2265781c 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -74,8 +74,6 @@ val modifiers_valid : string preference
val cmd_browse : string preference
val cmd_editor : string preference
val text_font : string preference
-val doc_url : string preference
-val library_url : string preference
val show_toolbar : bool preference
val contextual_menus_on_goal : bool preference
val window_width : int preference
diff --git a/ide/session.ml b/ide/session.ml
index 805e1d38a7..e2427a9b51 100644
--- a/ide/session.ml
+++ b/ide/session.ml
@@ -145,10 +145,12 @@ let set_buffer_handlers
buffer#apply_tag Tags.Script.edit_zone
~start:(get_start()) ~stop:(get_stop())
end in
- let backto_before_error it =
+ let processed_sentence_just_before_error it =
let rec aux old it =
- if it#is_start || not(it#has_tag Tags.Script.error_bg) then old
- else aux it it#backward_char in
+ if it#is_start then None
+ else if it#has_tag Tags.Script.processed then Some old
+ else if it#has_tag Tags.Script.error_bg then aux it it#backward_char
+ else None in
aux it it in
let insert_cb it s = if String.length s = 0 then () else begin
Minilib.log ("insert_cb " ^ string_of_int it#offset);
@@ -156,12 +158,16 @@ let set_buffer_handlers
let () = update_prev it in
if it#has_tag Tags.Script.to_process then
cancel_signal "Altering the script being processed in not implemented"
+ else if it#has_tag Tags.Script.incomplete then
+ cancel_signal "Altering the script being processed in not implemented"
else if it#has_tag Tags.Script.processed then
call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
else if it#has_tag Tags.Script.error_bg then begin
- let prev_sentence_end = backto_before_error it in
- let text_mark = add_mark prev_sentence_end in
- call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
+ match processed_sentence_just_before_error it with
+ | None -> ()
+ | Some prev_sentence_end ->
+ let text_mark = add_mark prev_sentence_end in
+ call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
end end in
let delete_cb ~start ~stop =
Minilib.log (Printf.sprintf "delete_cb %d %d" start#offset stop#offset);
@@ -171,14 +177,18 @@ let set_buffer_handlers
let text_mark = add_mark min_iter in
let rec aux min_iter =
if min_iter#equal max_iter then ()
+ else if min_iter#has_tag Tags.Script.incomplete then
+ cancel_signal "Altering the script being processed in not implemented"
else if min_iter#has_tag Tags.Script.to_process then
cancel_signal "Altering the script being processed in not implemented"
else if min_iter#has_tag Tags.Script.processed then
call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
else if min_iter#has_tag Tags.Script.error_bg then
- let prev_sentence_end = backto_before_error min_iter in
- let text_mark = add_mark prev_sentence_end in
- call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
+ match processed_sentence_just_before_error min_iter with
+ | None -> ()
+ | Some prev_sentence_end ->
+ let text_mark = add_mark prev_sentence_end in
+ call_coq_or_cancel_action (coqops#go_to_mark (`MARK text_mark))
else aux min_iter#forward_char in
aux min_iter in
let begin_action_cb () =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:26:16 +0000