summaryrefslogtreecommitdiff
path: root/ide/coqide.ml
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml209
1 files changed, 94 insertions, 115 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 450bfcdf..f5ff0899 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Preferences
@@ -46,7 +48,7 @@ open Session
(** The arguments that will be passed to coqtop. No quoting here, since
no /bin/sh when using create_process instead of open_process. *)
-let custom_project_files = ref []
+let custom_project_file = ref None
let sup_args = ref []
let logfile = ref None
@@ -81,17 +83,27 @@ let pr_exit_status = function
| Unix.WEXITED 0 -> " succeeded"
| _ -> " failed"
-let make_coqtop_args = function
- |None -> "", !sup_args
- |Some the_file ->
- let get_args f = Project_file.args_from_project f
- !custom_project_files project_file_name#get
- in
- match read_project#get with
- |Ignore_args -> "", !sup_args
- |Append_args ->
- let fname, args = get_args the_file in fname, args @ !sup_args
- |Subst_args -> get_args the_file
+let make_coqtop_args fname =
+ let open CoqProject_file in
+ let base_args = match read_project#get with
+ | Ignore_args -> !sup_args
+ | Append_args -> !sup_args
+ | Subst_args -> [] in
+ if read_project#get = Ignore_args then "", base_args
+ else
+ match !custom_project_file, fname with
+ | Some (d,proj), _ -> d, coqtop_args_from_project proj @ base_args
+ | None, None -> "", base_args
+ | None, Some the_file ->
+ match
+ CoqProject_file.find_project_file
+ ~from:(Filename.dirname the_file)
+ ~projfile_name:project_file_name#get
+ with
+ | None -> "", base_args
+ | Some proj ->
+ proj, coqtop_args_from_project (read_project_file proj) @ base_args
+;;
(** Setting drag & drop on widgets *)
@@ -274,6 +286,8 @@ let saveall _ =
| Some f -> ignore (sn.fileops#save f))
notebook#pages
+let () = Coq.save_all := saveall
+
let revert_all _ =
List.iter
(fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert)
@@ -318,10 +332,10 @@ let export kind sn =
local_cd f ^ cmd_coqdoc#get ^ " --" ^ kind ^ " -o " ^
(Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
in
- sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
+ sn.messages#default_route#set (Pp.str ("Running: "^cmd));
let finally st = flash_info (cmd ^ pr_exit_status st)
in
- run_command (fun msg -> sn.messages#add_string msg) finally cmd
+ run_command (fun msg -> sn.messages#default_route#add_string msg) finally cmd
let export kind = cb_on_current_term (export kind)
@@ -427,13 +441,15 @@ let compile sn =
match sn.fileops#filename with
|None -> flash_info "Active buffer has no name"
|Some f ->
- let cmd = cmd_coqc#get ^ " -I " ^ (Filename.quote (Filename.dirname f))
+ let args = Coq.get_arguments sn.coqtop in
+ let cmd = cmd_coqc#get
+ ^ " " ^ String.concat " " args
^ " " ^ (Filename.quote f) ^ " 2>&1"
in
let buf = Buffer.create 1024 in
- sn.messages#set (Richpp.richpp_of_string ("Running: "^cmd));
+ sn.messages#default_route#set (Pp.str ("Running: "^cmd));
let display s =
- sn.messages#add_string s;
+ sn.messages#default_route#add_string s;
Buffer.add_string buf s
in
let finally st =
@@ -441,8 +457,8 @@ let compile sn =
flash_info (f ^ " successfully compiled")
else begin
flash_info (f ^ " failed to compile");
- sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
- sn.messages#add (Richpp.richpp_of_string (Buffer.contents buf));
+ sn.messages#default_route#set (Pp.str "Compilation output:\n");
+ sn.messages#default_route#add (Pp.str (Buffer.contents buf));
end
in
run_command display finally cmd
@@ -464,13 +480,13 @@ let make sn =
|Some f ->
File.saveall ();
let cmd = local_cd f ^ cmd_make#get ^ " 2>&1" in
- sn.messages#set (Richpp.richpp_of_string "Compilation output:\n");
+ sn.messages#default_route#set (Pp.str "Compilation output:\n");
Buffer.reset last_make_buf;
last_make := "";
last_make_index := 0;
last_make_dir := Filename.dirname f;
let display s =
- sn.messages#add_string s;
+ sn.messages#default_route#add_string s;
Buffer.add_string last_make_buf s
in
let finally st = flash_info (cmd_make#get ^ pr_exit_status st)
@@ -508,11 +524,11 @@ let next_error sn =
let stopi = b#get_iter_at_byte ~line:(line-1) stop in
b#apply_tag Tags.Script.error ~start:starti ~stop:stopi;
b#place_cursor ~where:starti;
- sn.messages#set (Richpp.richpp_of_string error_msg);
+ sn.messages#default_route#set (Pp.str error_msg);
sn.script#misc#grab_focus ()
with Not_found ->
last_make_index := 0;
- sn.messages#set (Richpp.richpp_of_string "No more errors.\n")
+ sn.messages#default_route#set (Pp.str "No more errors.\n")
let next_error = cb_on_current_term next_error
@@ -536,7 +552,7 @@ let update_status sn =
display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name);
Coq.return ()
in
- Coq.bind (Coq.status ~logger:sn.messages#push false) next
+ Coq.bind (Coq.status false) next
let find_next_occurrence ~backward sn =
(** go to the next occurrence of the current word, forward or backward *)
@@ -593,16 +609,14 @@ let get_current_word term =
(** Then look at the current selected word *)
let buf1 = term.script#buffer in
let buf2 = term.proof#buffer in
- let buf3 = term.messages#buffer in
if buf1#has_selection then
let (start, stop) = buf1#selection_bounds in
buf1#get_text ~slice:true ~start ~stop ()
else if buf2#has_selection then
let (start, stop) = buf2#selection_bounds in
buf2#get_text ~slice:true ~start ~stop ()
- else if buf3#has_selection then
- let (start, stop) = buf3#selection_bounds in
- buf3#get_text ~slice:true ~start ~stop ()
+ else if term.messages#has_selection then
+ term.messages#get_selected_text
(** Otherwise try to find the word around the cursor *)
else
let it = term.script#buffer#get_iter_at_mark `INSERT in
@@ -652,36 +666,18 @@ let match_callback = cb_on_current_term match_callback
module Query = struct
-let searchabout sn =
- let word = get_current_word sn in
- let buf = sn.messages#buffer in
- let insert result =
- let qualid = result.Interface.coq_object_qualid in
- let name = String.concat "." qualid in
- let tpe = result.Interface.coq_object_object in
- buf#insert ~tags:[Tags.Message.item] name;
- buf#insert "\n";
- buf#insert tpe;
- buf#insert "\n";
- in
- let display_results r =
- sn.messages#clear;
- List.iter insert (match r with Interface.Good l -> l | _ -> []);
- Coq.return ()
- in
- let launch_query =
- let search = Coq.search [Interface.SubType_Pattern word, true] in
- Coq.bind search display_results
- in
- Coq.try_grab sn.coqtop launch_query ignore
-
-let searchabout () = on_current_term searchabout
-
let doquery query sn =
- sn.messages#clear;
- Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
-
-let otherquery command sn =
+ sn.messages#default_route#clear;
+ Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query ~route_id:0
+ ~next:(function
+ | Interface.Fail (_, _, err) ->
+ let err = Ideutils.validate err in
+ sn.messages#default_route#add err;
+ Coq.return ()
+ | Interface.Good () -> Coq.return ()))
+ ignore
+
+let queryif command sn =
Option.iter (fun query -> doquery (query ^ ".") sn)
begin try
let i = CString.string_index_from command 0 "..." in
@@ -690,12 +686,7 @@ let otherquery command sn =
else Some (CString.sub command 0 i ^ " " ^ word)
with Not_found -> Some command end
-let otherquery command = cb_on_current_term (otherquery command)
-
-let query command _ =
- if command = "Search" || command = "SearchAbout"
- then searchabout ()
- else otherquery command ()
+let query command _ = cb_on_current_term (queryif command) ()
end
@@ -724,7 +715,7 @@ let initial_about () =
else ""
in
let msg = initial_string ^ version_info ^ log_file_message () in
- on_current_term (fun term -> term.messages#add_string msg)
+ on_current_term (fun term -> term.messages#default_route#add_string msg)
let coq_icon () =
(* May raise Nof_found *)
@@ -788,15 +779,15 @@ let coqtop_arguments sn =
| args ->
let args = String.concat " " args in
let msg = Printf.sprintf "Invalid arguments: %s" args in
- let () = sn.messages#clear in
- sn.messages#push Feedback.Error (Richpp.richpp_of_string msg)
+ let () = sn.messages#default_route#clear in
+ sn.messages#default_route#push Feedback.Error (Pp.str msg)
else dialog#destroy ()
in
- let _ = entry#connect#activate ok_cb in
- let _ = ok#connect#clicked ok_cb in
+ let _ = entry#connect#activate ~callback:ok_cb in
+ let _ = ok#connect#clicked ~callback:ok_cb in
let cancel = GButton.button ~stock:`CANCEL ~packing:box#add () in
let cancel_cb () = dialog#destroy () in
- let _ = cancel#connect#clicked cancel_cb in
+ let _ = cancel#connect#clicked ~callback:cancel_cb in
dialog#show ()
let coqtop_arguments = cb_on_current_term coqtop_arguments
@@ -887,8 +878,8 @@ let alpha_items menu_name item_name l =
| [] -> ()
| [s] -> mk_item s
| s::_ as ll ->
- let name = item_name^" "^(String.make 1 s.[0]) in
- let label = "_@..." in label.[1] <- s.[0];
+ let name = Printf.sprintf "%s %c" item_name s.[0] in
+ let label = Printf.sprintf "_%c..." s.[0] in
item name ~label menu_name;
List.iter mk_item ll
in
@@ -1103,8 +1094,8 @@ let build_ui () =
menu templates_menu [
item "Templates" ~label:"Te_mplates";
- template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "J");
- template_item ("Theorem new_theorem : .\nProof.\n\nSave.\n", 8,11, "T");
+ template_item ("Lemma new_lemma : .\nProof.\n\nQed.\n", 6,9, "J");
+ template_item ("Theorem new_theorem : .\nProof.\n\nQed.\n", 8,11, "T");
template_item ("Definition ident := .\n", 11,5, "E");
template_item ("Inductive ident : :=\n | : .\n", 10,5, "I");
template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F");
@@ -1115,15 +1106,15 @@ let build_ui () =
];
alpha_items templates_menu "Template" Coq_commands.commands;
- let qitem s sc ?(dots = true) =
- let query = if dots then s ^ "..." else s in
+ let qitem s sc =
+ let query = s ^ "..." in
item s ~label:("_"^s)
~accel:(modifier_for_queries#get^sc)
~callback:(Query.query query)
in
menu queries_menu [
item "Queries" ~label:"_Queries";
- qitem "Search" "K" ~dots:false;
+ qitem "Search" "K";
qitem "Check" "C";
qitem "Print" "P";
qitem "About" "A";
@@ -1161,17 +1152,17 @@ let build_ui () =
item "Help" ~label:"_Help";
item "Browse Coq Manual" ~label:"Browse Coq _Manual"
~callback:(fun _ ->
- browse notebook#current_term.messages#add_string (doc_url ()));
+ browse notebook#current_term.messages#default_route#add_string (doc_url ()));
item "Browse Coq Library" ~label:"Browse Coq _Library"
~callback:(fun _ ->
- browse notebook#current_term.messages#add_string library_url#get);
+ browse notebook#current_term.messages#default_route#add_string library_url#get);
item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
~callback:(fun _ -> on_current_term (fun sn ->
- browse_keyword sn.messages#add_string (get_current_word sn)));
+ browse_keyword sn.messages#default_route#add_string (get_current_word sn)));
item "Help for μPG mode" ~label:"Help for μPG mode"
~callback:(fun _ -> on_current_term (fun sn ->
- sn.messages#clear;
- sn.messages#add_string (NanoPG.get_documentation ())));
+ sn.messages#default_route#clear;
+ sn.messages#default_route#add_string (NanoPG.get_documentation ())));
item "About Coq" ~label:"_About" ~stock:`ABOUT
~callback:MiscMenu.about
];
@@ -1207,9 +1198,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 *)
@@ -1274,8 +1270,8 @@ let build_ui () =
if b then toolbar#misc#show () else toolbar#misc#hide ()
in
stick show_toolbar toolbar refresh_toolbar;
- let _ = source_style#connect#changed refresh_style in
- let _ = source_language#connect#changed refresh_language in
+ let _ = source_style#connect#changed ~callback:refresh_style in
+ let _ = source_language#connect#changed ~callback:refresh_language in
(* Color configuration *)
Tags.Script.incomplete#set_property
@@ -1311,25 +1307,6 @@ let main files =
Minilib.log "End of Coqide.main"
-(** {2 Geoproof } *)
-
-(** This function check every tenth of second if GeoProof has send
- something on his private clipboard *)
-
-let check_for_geoproof_input () =
- let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in
- let handler () = match cb_Dr#text with
- |None -> true
- |Some "Ack" -> true
- |Some s ->
- on_current_term (fun sn -> sn.buffer#insert (s ^ "\n"));
- (* cb_Dr#clear does not work so i use : *)
- cb_Dr#set_text "Ack";
- true
- in
- ignore (GMain.Timeout.add ~ms:100 ~callback:handler)
-
-
(** {2 Argument parsing } *)
(** By default, the coqtop we try to launch is exactly the current coqide
@@ -1345,9 +1322,11 @@ let read_coqide_args argv =
if coqtop = None then filter_coqtop (Some prog) project_files out args
else (output_string stderr "Error: multiple -coqtop options"; exit 1)
|"-f" :: file :: args ->
+ if project_files <> None then
+ (output_string stderr "Error: multiple -f options"; exit 1);
let d = CUnix.canonical_path_name (Filename.dirname file) in
- let p = Project_file.read_project_file file in
- filter_coqtop coqtop ((d,p) :: project_files) out args
+ let p = CoqProject_file.read_project_file file in
+ filter_coqtop coqtop (Some (d,p)) out args
|"-f" :: [] ->
output_string stderr "Error: missing project file name"; exit 1
|"-coqtop" :: [] ->
@@ -1358,17 +1337,17 @@ let read_coqide_args argv =
Backtrace.record_backtrace true;
filter_coqtop coqtop project_files ("-debug"::out) args
|"-coqtop-flags" :: flags :: args->
- Flags.ideslave_coqtop_flags := Some flags;
+ Coq.ideslave_coqtop_flags := Some flags;
filter_coqtop coqtop project_files out args
|arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg ->
(* argument added by MacOS during .app launch *)
filter_coqtop coqtop project_files out args
|arg::args -> filter_coqtop coqtop project_files (arg::out) args
- |[] -> (coqtop,List.rev project_files,List.rev out)
+ |[] -> (coqtop,project_files,List.rev out)
in
- let coqtop,project_files,argv = filter_coqtop None [] [] argv in
+ let coqtop,project_files,argv = filter_coqtop None None [] argv in
Ideutils.custom_coqtop := coqtop;
- custom_project_files := project_files;
+ custom_project_file := project_files;
argv
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 20:57:47 +0000