From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- ide/coqide.ml | 209 ++++++++++++++++++++++++++-------------------------------- 1 file changed, 94 insertions(+), 115 deletions(-) (limited to 'ide/coqide.ml') 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 *) -(* " 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 -- cgit v1.2.3