summaryrefslogtreecommitdiff
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-01-25 14:42:51 +0100
commit7cfc4e5146be5666419451bdd516f1f3f264d24a (patch)
treee4197645da03dc3c7cc84e434cc31d0a0cca7056 /ide/coqide.ml
parent420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff)
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml4100
1 files changed, 1288 insertions, 2812 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index c7e14007..fa64defa 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,1418 +9,483 @@
open Preferences
open Gtk_parsing
open Ideutils
+open Session
-type ide_info = {
- start : GText.mark;
- stop : GText.mark;
-}
-
-(** Have we used admit or declarative mode's daimon ?
- If yes, we color differently *)
-
-type safety = Safe | Unsafe
-
-let safety_tag = function
- | Safe -> Tags.Script.processed
- | Unsafe -> Tags.Script.unjustified
-
-class type analyzed_views=
-object
- val mutable act_id : GtkSignal.id option
- val input_buffer : GText.buffer
- val input_view : Undo.undoable_view
- val last_array : string array
- val mutable last_index : bool
- val message_buffer : GText.buffer
- val message_view : GText.view
- val proof_buffer : GText.buffer
- val proof_view : GText.view
- val cmd_stack : ide_info Stack.t
- val mycoqtop : Coq.coqtop ref
- val mutable is_active : bool
- val mutable read_only : bool
- val mutable filename : string option
- val mutable stats : Unix.stats option
- method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b
- method set_auto_complete : bool -> unit
-
- method filename : string option
- method stats : Unix.stats option
- method update_stats : unit
- method revert : unit
- method auto_save : unit
- method save : string -> bool
- method save_as : string -> bool
- method read_only : bool
- method set_read_only : bool -> unit
- method is_active : bool
- method activate : unit -> unit
- method active_keypress_handler : GdkEvent.Key.t -> bool
- method backtrack_to : GText.iter -> unit
- method backtrack_to_no_lock : GText.iter -> unit
- method clear_message : unit
- method find_phrase_starting_at :
- GText.iter -> (GText.iter * GText.iter) option
- method get_insert : GText.iter
- method get_start_of_input : GText.iter
- method go_to_insert : unit
- method indent_current_line : unit
- method go_to_next_occ_of_cur_word : unit
- method go_to_prev_occ_of_cur_word : unit
- method insert_command : string -> string -> unit
- method tactic_wizard : string list -> unit
- method insert_message : string -> unit
- method process_next_phrase : bool -> unit
- method process_until_iter_or_error : GText.iter -> unit
- method process_until_end_or_error : unit
- method recenter_insert : unit
- method reset_initial : unit
- method force_reset_initial : unit
- method set_message : string -> unit
- method raw_coq_query : string -> unit
- method show_goals : unit
- method show_goals_full : unit
- method undo_last_step : unit
- method help_for_keyword : unit -> unit
- method complete_at_offset : int -> bool
-end
+(** Note concerning GtkTextBuffer
+ Be careful with gtk calls on text buffers, since many are non-atomic :
+ they emit a gtk signal and the handlers for this signal are run
+ immediately, before returning to the current function.
+ Here's a partial list of these signals and the methods that
+ trigger them (cf. documentation of GtkTextBuffer, signal section)
-type viewable_script =
- {script : Undo.undoable_view;
- tab_label : GMisc.label;
- mutable filename : string;
- mutable encoding : string;
- proof_view : GText.view;
- message_view : GText.view;
- analyzed_view : analyzed_views;
- toplvl : Coq.coqtop ref;
- command : Command_windows.command_window;
- }
-
-let kill_session s =
- (* To close the detached views of this script, we call manually
- [destroy] on it, triggering some callbacks in [detach_view].
- In a more modern lablgtk, rather use the page-removed signal ? *)
- s.script#destroy ();
- Coq.kill_coqtop !(s.toplvl)
-
-let build_session s =
- let session_paned = GPack.paned `VERTICAL () in
- let eval_paned = GPack.paned `HORIZONTAL ~border_width:5
- ~packing:(session_paned#pack1 ~shrink:false ~resize:true) () in
- let script_frame = GBin.frame ~shadow_type:`IN
- ~packing:eval_paned#add1 () in
- let script_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC
- ~packing:script_frame#add () in
- let state_paned = GPack.paned `VERTICAL
- ~packing:eval_paned#add2 () in
- let proof_frame = GBin.frame ~shadow_type:`IN
- ~packing:state_paned#add1 () in
- let proof_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC
- ~packing:proof_frame#add () in
- let message_frame = GBin.frame ~shadow_type:`IN
- ~packing:state_paned#add2 () in
- let message_scroll = GBin.scrolled_window ~vpolicy:`AUTOMATIC ~hpolicy:`AUTOMATIC
- ~packing:message_frame#add () in
- let session_tab = GPack.hbox ~homogeneous:false () in
- let img = GMisc.image ~icon_size:`SMALL_TOOLBAR
- ~packing:session_tab#pack () in
- let _ =
- s.script#buffer#connect#modified_changed
- ~callback:(fun () -> if s.script#buffer#modified
- then img#set_stock `SAVE
- else img#set_stock `YES) in
- let _ =
- eval_paned#misc#connect#size_allocate
- ~callback:
- (let old_paned_width = ref 2 in
- let old_paned_height = ref 2 in
- (fun {Gtk.width=paned_width;Gtk.height=paned_height} ->
- if !old_paned_width <> paned_width || !old_paned_height <> paned_height then (
- eval_paned#set_position (eval_paned#position * paned_width / !old_paned_width);
- state_paned#set_position (state_paned#position * paned_height / !old_paned_height);
- old_paned_width := paned_width;
- old_paned_height := paned_height;
- )))
- in
- session_paned#pack2 ~shrink:false ~resize:false (s.command#frame#coerce);
- script_scroll#add s.script#coerce;
- proof_scroll#add s.proof_view#coerce;
- message_scroll#add s.message_view#coerce;
- session_tab#pack s.tab_label#coerce;
- img#set_stock `YES;
- eval_paned#set_position 1;
- state_paned#set_position 1;
- (Some session_tab#coerce,None,session_paned#coerce)
-
-let session_notebook =
- Typed_notebook.create build_session kill_session
- ~border_width:2 ~show_border:false ~scrollable:true ()
+ begin_user_action : #begin_user_action, #insert_interactive,
+ #insert_range_interactive, #delete_interactive, #delete_selection
+ end_user_action : #end_user_action, #insert_interactive,
+ #insert_range_interactive, #delete_interactive, #delete_selection
-let cb = GData.clipboard Gdk.Atom.primary
+ insert_text : #insert (and variants)
+ delete_range : #delete (and variants)
-let last_cb_content = ref ""
+ apply_tag : #apply_tag, (and some #insert)
+ remove_tag : #remove_tag
-let update_notebook_pos () =
- let pos =
- match !current.vertical_tabs, !current.opposite_tabs with
- | false, false -> `TOP
- | false, true -> `BOTTOM
- | true , false -> `LEFT
- | true , true -> `RIGHT
- in
- session_notebook#set_tab_pos pos
+ mark_deleted : #delete_mark
+ mark_set : #create_mark, #move_mark
-let to_do_on_page_switch = ref []
+ changed : ... (whenever a buffer has changed)
+ modified_changed : #set_modified (and whenever the modified bit flips)
+ Caveat : when the buffer is modified, all iterators on it become
+ invalid and shouldn't be used (nasty errors otherwise). There are
+ some special cases : boundaries given to #insert and #delete are
+ revalidated by the default signal handler.
+*)
-(** * Coqide's handling of signals *)
+(** {2 Some static elements } *)
-(** We ignore Ctrl-C, and for most of the other catchable signals
- we launch an emergency save of opened files and then exit *)
+let prefs = Preferences.current
-let signals_to_crash = [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
- Sys.sigill; Sys.sigpipe; Sys.sigquit;
- (* Sys.sigsegv; Sys.sigterm;*) Sys.sigusr2]
+(** 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 sup_args = ref []
-let crash_save i =
- (* ignore (Unix.sigprocmask Unix.SIG_BLOCK signals_to_crash);*)
- Minilib.safe_prerr_endline "Trying to save all buffers in .crashcoqide files";
- let count = ref 0 in
- List.iter
- (function {script=view; analyzed_view = av } ->
- (let filename = match av#filename with
- | None ->
- incr count;
- "Unnamed_coqscript_"^(string_of_int !count)^".crashcoqide"
- | Some f -> f^".crashcoqide"
- in
- try
- if try_export filename (view#buffer#get_text ()) then
- Minilib.safe_prerr_endline ("Saved "^filename)
- else Minilib.safe_prerr_endline ("Could not save "^filename)
- with _ -> Minilib.safe_prerr_endline ("Could not save "^filename))
- )
- session_notebook#pages;
- Minilib.safe_prerr_endline "Done. Please report.";
- if i <> 127 then exit i
-
-let ignore_break () =
- List.iter
- (fun i ->
- try Sys.set_signal i (Sys.Signal_handle crash_save)
- with _ -> prerr_endline "Signal ignored (normal if Win32)")
- signals_to_crash;
- (* We ignore the Ctrl-C, this is required for the Stop button to work,
- since we will actually send Ctrl-C to all processes sharing
- our console (including us) *)
- Sys.set_signal Sys.sigint Sys.Signal_ignore
-
-
-(** * Locks *)
-
-(* Locking machinery for Coq kernel *)
-let coq_computing = Mutex.create ()
-
-(* To prevent Coq from interrupting during undoing...*)
-let coq_may_stop = Mutex.create ()
-
-(* To prevent a force_reset_initial during a force_reset_initial *)
-let resetting = Mutex.create ()
-
-exception RestartCoqtop
-exception Unsuccessful
-
-let force_reset_initial () =
- prerr_endline "Reset Initial";
- session_notebook#current_term.analyzed_view#force_reset_initial
-
-let break () =
- prerr_endline "User break received";
- Coq.break_coqtop !(session_notebook#current_term.toplvl)
-
-let do_if_not_computing text f x =
- let threaded_task () =
- if Mutex.try_lock coq_computing then
- begin
- prerr_endline "Getting lock";
- List.iter
- (fun elt -> try f elt with
- | RestartCoqtop -> elt.analyzed_view#reset_initial
- | Sys_error str ->
- elt.analyzed_view#reset_initial;
- elt.analyzed_view#set_message
- ("Unable to communicate with coqtop, restarting coqtop.\n"^
- "Error was: "^str)
- | e ->
- Mutex.unlock coq_computing;
- elt.analyzed_view#set_message
- ("Unknown error, please report:\n"^(Printexc.to_string e)))
- x;
- prerr_endline "Releasing lock";
- Mutex.unlock coq_computing;
- end
- else
- prerr_endline "Discarded order (computations are ongoing)"
- in
- prerr_endline ("Launching thread " ^ text);
- ignore (Glib.Timeout.add ~ms:300 ~callback:
- (fun () -> if Mutex.try_lock coq_computing
- then (Mutex.unlock coq_computing; false)
- else (pbar#pulse (); true)));
- ignore (Thread.create threaded_task ())
-
-let warning msg =
- GToolbox.message_box ~title:"Warning"
- ~icon:(let img = GMisc.image () in
- img#set_stock `DIALOG_WARNING;
- img#set_icon_size `DIALOG;
- img#coerce)
- msg
-
-let remove_current_view_page () =
- let do_remove () =
- let c = session_notebook#current_page in
- session_notebook#remove_page c
- in
- let current = session_notebook#current_term in
- if not current.script#buffer#modified then do_remove ()
- else
- match GToolbox.question_box ~title:"Close"
- ~buttons:["Save Buffer and Close";
- "Close without Saving";
- "Don't Close"]
- ~default:0
- ~icon:(let img = GMisc.image () in
- img#set_stock `DIALOG_WARNING;
- img#set_icon_size `DIALOG;
- img#coerce)
- "This buffer has unsaved modifications"
- with
- | 1 ->
- begin match current.analyzed_view#filename with
- | None ->
- begin match select_file_for_save ~title:"Save file" () with
- | None -> ()
- | Some f ->
- if current.analyzed_view#save_as f then begin
- flash_info ("File " ^ f ^ " saved") ;
- do_remove ()
- end else
- warning ("Save Failed (check if " ^ f ^ " is writable)")
- end
- | Some f ->
- if current.analyzed_view#save f then begin
- flash_info ("File " ^ f ^ " saved") ;
- do_remove ()
- end else
- warning ("Save Failed (check if " ^ f ^ " is writable)")
- end
- | 2 -> do_remove ()
- | _ -> ()
+let logfile = ref None
-module Opt = Coq.PrintOpt
+(** {2 Notebook of sessions } *)
-let print_items = [
- ([Opt.implicit],"Display implicit arguments","Display _implicit arguments",
- "i",false);
- ([Opt.coercions],"Display coercions","Display _coercions","c",false);
- ([Opt.raw_matching],"Display raw matching expressions",
- "Display raw _matching expressions","m",true);
- ([Opt.notations],"Display notations","Display _notations","n",true);
- ([Opt.all_basic],"Display all basic low-level contents",
- "Display _all basic low-level contents","a",false);
- ([Opt.existential],"Display existential variable instances",
- "Display _existential variable instances","e",false);
- ([Opt.universes],"Display universe levels","Display _universe levels",
- "u",false);
- ([Opt.all_basic;Opt.existential;Opt.universes], "Display all low-level contents",
- "Display all _low-level contents","l",false)
-]
+(** The main element of coqide is a notebook of session views *)
-let setopts ct opts v =
- let opts = List.map (fun o -> (o, v)) opts in
- Coq.PrintOpt.set ct opts
-
-(* Reset this to None on page change ! *)
-let (last_completion:(string*int*int*bool) option ref) = ref None
-
-let () = to_do_on_page_switch :=
- (fun i -> last_completion := None)::!to_do_on_page_switch
-
-let rec complete input_buffer w (offset:int) =
- match !last_completion with
- | Some (lw,loffset,lpos,backward)
- when lw=w && loffset=offset ->
- begin
- let iter = input_buffer#get_iter (`OFFSET lpos) in
- if backward then
- match complete_backward w iter with
- | None ->
- last_completion :=
- Some (lw,loffset,
- (find_word_end
- (input_buffer#get_iter (`OFFSET loffset)))#offset ,
- false);
- None
- | Some (ss,start,stop) as result ->
- last_completion :=
- Some (w,offset,ss#offset,true);
- result
- else
- match complete_forward w iter with
- | None ->
- last_completion := None;
- None
- | Some (ss,start,stop) as result ->
- last_completion :=
- Some (w,offset,ss#offset,false);
- result
- end
- | _ -> begin
- match complete_backward w (input_buffer#get_iter (`OFFSET offset)) with
- | None ->
- last_completion :=
- Some (w,offset,(find_word_end (input_buffer#get_iter
- (`OFFSET offset)))#offset,false);
- complete input_buffer w offset
- | Some (ss,start,stop) as result ->
- last_completion := Some (w,offset,ss#offset,true);
- result
- end
+let notebook =
+ Wg_Notebook.create Session.build_layout Session.kill
+ ~border_width:2 ~show_border:false ~scrollable:true ()
-let get_current_word () =
- match session_notebook#current_term,cb#text with
- | {script=script; analyzed_view=av;},None ->
- prerr_endline "None selected";
- let it = av#get_insert in
- let start = find_word_start it in
- let stop = find_word_end start in
- script#buffer#move_mark `SEL_BOUND ~where:start;
- script#buffer#move_mark `INSERT ~where:stop;
- script#buffer#get_text ~slice:true ~start ~stop ()
- | _,Some t ->
- prerr_endline "Some selected";
- prerr_endline t;
- t
-
-
-let input_channel b ic =
- let buf = String.create 1024 and len = ref 0 in
- while len := input ic buf 0 1024; !len > 0 do
- Buffer.add_substring b buf 0 !len
- done
-
-let with_file handler name ~f =
- try
- let ic = open_in_gen [Open_rdonly;Open_creat] 0o644 name in
- try f ic; close_in ic with e -> close_in ic; raise e
- with Sys_error s -> handler s
-
-(* For find_phrase_starting_at *)
-exception Stop of int
-
-let tag_of_sort = function
- | Coq_lex.Comment -> Tags.Script.comment
- | Coq_lex.Keyword -> Tags.Script.kwd
- | Coq_lex.Declaration -> Tags.Script.decl
- | Coq_lex.ProofDeclaration -> Tags.Script.proof_decl
- | Coq_lex.Qed -> Tags.Script.qed
- | Coq_lex.String -> failwith "No tag"
-
-let apply_tag (buffer:GText.buffer) orig off_conv from upto sort =
- try
- let tag = tag_of_sort sort in
- let start = orig#forward_chars (off_conv from) in
- let stop = orig#forward_chars (off_conv upto) in
- buffer#apply_tag ~start ~stop tag
- with _ -> ()
-
-let remove_tags (buffer:GText.buffer) from upto =
- List.iter (buffer#remove_tag ~start:from ~stop:upto)
- [ Tags.Script.comment; Tags.Script.kwd; Tags.Script.decl;
- Tags.Script.proof_decl; Tags.Script.qed ]
-
-(** Cut a part of the buffer in sentences and tag them.
- Invariant: either this slice ends the buffer, or it ends with ".".
- May raise [Coq_lex.Unterminated] when the zone ends with
- an unterminated sentence. *)
-
-let split_slice_lax (buffer:GText.buffer) from upto =
- remove_tags buffer from upto;
- buffer#remove_tag ~start:from ~stop:upto Tags.Script.sentence;
- let slice = buffer#get_text ~start:from ~stop:upto () in
- let rec split_substring str =
- let off_conv = byte_offset_to_char_offset str in
- let slice_len = String.length str in
- let end_off = Coq_lex.delimit_sentence (apply_tag buffer from off_conv) str
- in
- let start = from#forward_chars (off_conv end_off) in
- let stop = start#forward_char in
- buffer#apply_tag ~start ~stop Tags.Script.sentence;
- let next = end_off + 1 in
- if next < slice_len then begin
- ignore (from#nocopy#forward_chars (off_conv next));
- split_substring (String.sub str next (slice_len - next))
- end
- in
- split_substring slice
-(** Searching forward and backward a position fulfilling some condition *)
+(** {2 Callback functions for the user interface } *)
-let rec forward_search cond (iter:GText.iter) =
- if iter#is_end || cond iter then iter
- else forward_search cond iter#forward_char
+let on_current_term f =
+ let term = try Some notebook#current_term with Invalid_argument _ -> None in
+ match term with
+ | None -> ()
+ | Some t -> ignore (f t)
-let rec backward_search cond (iter:GText.iter) =
- if iter#is_start || cond iter then iter
- else backward_search cond iter#backward_char
+let cb_on_current_term f _ = on_current_term f
-let is_sentence_end s = s#has_tag Tags.Script.sentence
-let is_char s c = s#char = Char.code c
+(** Nota: using && here has the advantage of working both under win32 and unix.
+ If someday we want the main command to be tried even if the "cd" has failed,
+ then we should use " ; " under unix but " & " under win32 (cf. #2363). *)
-(** Search backward the first character of a sentence, starting at [iter]
- and going at most up to [soi] (meant to be the end of the locked zone).
- Raise [StartError] when no proper sentence start has been found.
- A character following a ending "." is considered as a sentence start
- only if this character is a blank. In particular, when a final "."
- at the end of the locked zone isn't followed by a blank, then this
- non-blank character will be signaled as erroneous in [tag_on_insert] below.
-*)
+let local_cd file =
+ "cd " ^ Filename.quote (Filename.dirname file) ^ " && "
-exception StartError
+let pr_exit_status = function
+ | Unix.WEXITED 0 -> " succeeded"
+ | _ -> " failed"
-let grab_sentence_start (iter:GText.iter) soi =
- let cond iter =
- if iter#compare soi < 0 then raise StartError;
- let prev = iter#backward_char in
- is_sentence_end prev &&
- (not (is_char prev '.') ||
- List.exists (is_char iter) [' ';'\n';'\r';'\t'])
- in
- backward_search cond iter
+let make_coqtop_args = function
+ |None -> !sup_args
+ |Some the_file ->
+ let get_args f = Project_file.args_from_project f
+ !custom_project_files prefs.project_file_name
+ in
+ match prefs.read_project with
+ |Ignore_args -> !sup_args
+ |Append_args -> get_args the_file @ !sup_args
+ |Subst_args -> get_args the_file
+
+(** Setting drag & drop on widgets *)
+
+let load_file_cb : (string -> unit) ref = ref ignore
+
+let drop_received context ~x ~y data ~info ~time =
+ if data#format = 8 then begin
+ let files = Str.split (Str.regexp "\r?\n") data#data in
+ let path = Str.regexp "^file://\\(.*\\)$" in
+ List.iter (fun f ->
+ if Str.string_match path f 0 then
+ !load_file_cb (Str.matched_group 1 f)
+ ) files;
+ context#finish ~success:true ~del:false ~time
+ end else context#finish ~success:false ~del:false ~time
+
+let drop_targets = [
+ { Gtk.target = "text/uri-list"; Gtk.flags = []; Gtk.info = 0}
+]
-(** Search forward the first character immediately after a sentence end *)
+let set_drag (w : GObj.drag_ops) =
+ w#dest_set drop_targets ~actions:[`COPY;`MOVE];
+ w#connect#data_received ~callback:drop_received
-let rec grab_sentence_stop (start:GText.iter) =
- (forward_search is_sentence_end start)#forward_char
+(** Session management *)
-(** Search forward the first character immediately after a "." sentence end
- (and not just a "{" or "}" or comment end *)
+let create_session f =
+ let ans = Session.create f (make_coqtop_args f) in
+ let _ = set_drag ans.script#drag in
+ ans
-let rec grab_ending_dot (start:GText.iter) =
- let is_ending_dot s = is_sentence_end s && s#char = Char.code '.' in
- (forward_search is_ending_dot start)#forward_char
+(** Auxiliary functions for the File operations *)
-(** Retag a zone that has been edited *)
+module FileAux = struct
-let tag_on_insert buffer =
- (* the start of the non-locked zone *)
- let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
- (* the inserted zone is between [prev_insert] and [insert] *)
- let insert = buffer#get_iter_at_mark `INSERT in
- let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
- (* [prev] is normally always before [insert] even when deleting.
- Let's check this nonetheless *)
- let prev, insert =
- if insert#compare prev < 0 then insert, prev else prev, insert
- in
+let load_file ?(maycreate=false) f =
+ let f = CUnix.correct_path f (Sys.getcwd ()) in
try
- let start = grab_sentence_start prev soi in
- (** The status of "{" "}" as sentence delimiters is too fragile.
- We retag up to the next "." instead. *)
- let stop = grab_ending_dot insert in
- try split_slice_lax buffer start stop
- with Coq_lex.Unterminated ->
- (* This shouldn't happen frequently. Either:
- - we are at eof, with indeed an unfinished sentence.
- - we have just inserted an opening of comment or string.
- - the inserted text ends with a "." that interacts with the "."
- found by [grab_ending_dot] to form a non-ending "..".
- In any case, we retag up to eof, since this isn't that costly. *)
- if not stop#is_end then
- try split_slice_lax buffer start buffer#end_iter
- with Coq_lex.Unterminated -> ()
- with StartError ->
- buffer#apply_tag Tags.Script.error ~start:soi ~stop:soi#forward_char
-
-let force_retag buffer =
- try split_slice_lax buffer buffer#start_iter buffer#end_iter
- with Coq_lex.Unterminated -> ()
-
-let toggle_proof_visibility (buffer:GText.buffer) (cursor:GText.iter) =
- (* move back twice if not into proof_decl,
- * once if into proof_decl and back_char into_proof_decl,
- * don't move if into proof_decl and back_char not into proof_decl *)
- if not (cursor#has_tag Tags.Script.proof_decl) then
- ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
- if cursor#backward_char#has_tag Tags.Script.proof_decl then
- ignore (cursor#nocopy#backward_to_tag_toggle (Some Tags.Script.proof_decl));
- let decl_start = cursor in
- let prf_end = decl_start#forward_to_tag_toggle (Some Tags.Script.qed) in
- let decl_end = grab_ending_dot decl_start in
- let prf_end = grab_ending_dot prf_end in
- let prf_end = prf_end#forward_char in
- if decl_start#has_tag Tags.Script.folded then (
- buffer#remove_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
- buffer#remove_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
- else (
- buffer#apply_tag ~start:decl_start ~stop:decl_end Tags.Script.folded;
- buffer#apply_tag ~start:decl_end ~stop:prf_end Tags.Script.hidden)
+ Minilib.log "Loading file starts";
+ let is_f = CUnix.same_file f in
+ let rec search_f i = function
+ | [] -> false
+ | sn :: sessions ->
+ match sn.fileops#filename with
+ | Some fn when is_f fn -> notebook#goto_page i; true
+ | _ -> search_f (i+1) sessions
+ in
+ if not (search_f 0 notebook#pages) then begin
+ Minilib.log "Loading: get raw content";
+ let b = Buffer.create 1024 in
+ if Sys.file_exists f then Ideutils.read_file f b
+ else if not maycreate then flash_info ("Load failed: no such file");
+ Minilib.log "Loading: convert content";
+ let s = do_convert (Buffer.contents b) in
+ Minilib.log "Loading: create view";
+ let session = create_session (Some f) in
+ let index = notebook#append_term session in
+ notebook#goto_page index;
+ Minilib.log "Loading: stats";
+ session.fileops#update_stats;
+ let input_buffer = session.buffer in
+ Minilib.log "Loading: fill buffer";
+ input_buffer#set_text s;
+ input_buffer#set_modified false;
+ input_buffer#place_cursor ~where:input_buffer#start_iter;
+ Sentence.tag_all input_buffer;
+ session.script#clear_undo ();
+ !refresh_editor_hook ();
+ Minilib.log "Loading: success";
+ end
+ with e -> flash_info ("Load failed: "^(Printexc.to_string e))
+
+let confirm_save ok =
+ if ok then flash_info "Saved" else warning "Save Failed"
+
+let select_and_save ~saveas ?filename sn =
+ let do_save = if saveas then sn.fileops#saveas else sn.fileops#save in
+ let title = if saveas then "Save file as" else "Save file" in
+ match select_file_for_save ~title ?filename () with
+ |None -> false
+ |Some f ->
+ let ok = do_save f in
+ confirm_save ok;
+ if ok then sn.tab_label#set_text (Filename.basename f);
+ ok
+
+let check_save ~saveas sn =
+ try match sn.fileops#filename with
+ |None -> select_and_save ~saveas sn
+ |Some f ->
+ let ok = sn.fileops#save f in
+ confirm_save ok;
+ ok
+ with _ -> warning "Save Failed"; false
+
+exception DontQuit
+
+let check_quit saveall =
+ (try save_pref () with _ -> flash_info "Cannot save preferences");
+ let is_modified sn = sn.buffer#modified in
+ if List.exists is_modified notebook#pages then begin
+ let answ = GToolbox.question_box ~title:"Quit"
+ ~buttons:["Save Named Buffers and Quit";
+ "Quit without Saving";
+ "Don't Quit"]
+ ~default:0
+ ~icon:(warn_image ())#coerce
+ "There are unsaved buffers"
+ in
+ match answ with
+ | 1 -> saveall ()
+ | 2 -> ()
+ | _ -> raise DontQuit
+ end;
+ List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages
+
+(* For MacOS, just to be sure, we close all coqtops (again?) *)
+let close_and_quit () =
+ List.iter (fun sn -> Coq.close_coqtop sn.coqtop) notebook#pages;
+ exit 0
+
+let crash_save exitcode =
+ Minilib.log "Starting emergency save of buffers in .crashcoqide files";
+ let idx =
+ let r = ref 0 in
+ fun () -> incr r; string_of_int !r
+ in
+ let save_session sn =
+ let filename = match sn.fileops#filename with
+ | None -> "Unnamed_coqscript_" ^ idx () ^ ".crashcoqide"
+ | Some f -> f^".crashcoqide"
+ in
+ try
+ if try_export filename (sn.buffer#get_text ()) then
+ Minilib.log ("Saved "^filename)
+ else Minilib.log ("Could not save "^filename)
+ with _ -> Minilib.log ("Could not save "^filename)
+ in
+ List.iter save_session notebook#pages;
+ Minilib.log "End emergency save";
+ exit exitcode
-(** 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 sup_args = ref []
+end
-class analyzed_view (_script:Undo.undoable_view) (_pv:GText.view) (_mv:GText.view) _cs _ct _fn =
-object(self)
- val input_view = _script
- val input_buffer = _script#buffer
- val proof_view = _pv
- val proof_buffer = _pv#buffer
- val message_view = _mv
- val message_buffer = _mv#buffer
- val cmd_stack = _cs
- val mycoqtop = _ct
- val mutable is_active = false
- val mutable read_only = false
- val mutable filename = _fn
- val mutable stats = None
- val mutable last_modification_time = 0.
- val mutable last_auto_save_time = 0.
- val mutable find_forward_instead_of_backward = false
-
- val mutable auto_complete_on = !current.auto_complete
- val hidden_proofs = Hashtbl.create 32
-
- method private toggle_auto_complete =
- auto_complete_on <- not auto_complete_on
- method set_auto_complete t = auto_complete_on <- t
- method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b = fun f x ->
- let old = auto_complete_on in
- self#set_auto_complete false;
- let y = f x in
- self#set_auto_complete old;
- y
-
- method filename = filename
- method stats = stats
- method update_stats =
- match filename with
- | Some f -> stats <- my_stat f
- | _ -> ()
+let () = load_file_cb := (fun s -> FileAux.load_file s)
- method revert =
- match filename with
- | Some f -> begin
- let do_revert () = begin
- push_info "Reverting buffer";
- try
- if is_active then self#force_reset_initial;
- let b = Buffer.create 1024 in
- with_file flash_info f ~f:(input_channel b);
- let s = try_convert (Buffer.contents b) in
- input_buffer#set_text s;
- self#update_stats;
- input_buffer#place_cursor ~where:input_buffer#start_iter;
- input_buffer#set_modified false;
- pop_info ();
- flash_info "Buffer reverted";
- force_retag input_buffer;
- with _ ->
- pop_info ();
- flash_info "Warning: could not revert buffer";
- end
- in
- if input_buffer#modified then
- match (GToolbox.question_box
- ~title:"Modified buffer changed on disk"
- ~buttons:["Revert from File";
- "Overwrite File";
- "Disable Auto Revert"]
- ~default:0
- ~icon:(stock_to_widget `DIALOG_WARNING)
- "Some unsaved buffers changed on disk"
- )
- with 1 -> do_revert ()
- | 2 -> if self#save f then flash_info "Overwritten" else
- flash_info "Could not overwrite file"
- | _ ->
- prerr_endline "Auto revert set to false";
- !current.global_auto_revert <- false;
- disconnect_revert_timer ()
- else do_revert ()
- end
- | None -> ()
+(** Callbacks for the File menu *)
- method save f =
- if try_export f (input_buffer#get_text ()) then begin
- filename <- Some f;
- input_buffer#set_modified false;
- stats <- my_stat f;
- (match self#auto_save_name with
- | None -> ()
- | Some fn -> try Sys.remove fn with _ -> ());
- true
- end
- else false
-
- method private auto_save_name =
- match filename with
- | None -> None
- | Some f ->
- let dir = Filename.dirname f in
- let base = (fst !current.auto_save_name) ^
- (Filename.basename f) ^
- (snd !current.auto_save_name)
- in Some (Filename.concat dir base)
-
- method private need_auto_save =
- input_buffer#modified &&
- last_modification_time > last_auto_save_time
-
- method auto_save =
- if self#need_auto_save then begin
- match self#auto_save_name with
- | None -> ()
- | Some fn ->
- try
- last_auto_save_time <- Unix.time();
- prerr_endline ("Autosave time : "^(string_of_float (Unix.time())));
- if try_export fn (input_buffer#get_text ()) then begin
- flash_info ~delay:1000 "Autosaved"
- end
- else warning
- ("Autosave failed (check if " ^ fn ^ " is writable)")
- with _ ->
- warning ("Autosave: unexpected error while writing "^fn)
- end
+module File = struct
- method save_as f =
- if Sys.file_exists f then
- match (GToolbox.question_box ~title:"File exists on disk"
- ~buttons:["Overwrite";
- "Cancel";]
- ~default:1
- ~icon:
- (let img = GMisc.image () in
- img#set_stock `DIALOG_WARNING;
- img#set_icon_size `DIALOG;
- img#coerce)
- ("File "^f^" already exists")
- )
- with 1 -> self#save f
- | _ -> false
- else self#save f
-
- method set_read_only b = read_only<-b
- method read_only = read_only
- method is_active = is_active
- method insert_message s =
- message_buffer#insert s;
- message_view#misc#draw None
-
- method set_message s =
- message_buffer#set_text s;
- message_view#misc#draw None
-
- method clear_message = message_buffer#set_text ""
- val mutable last_index = true
- val last_array = [|"";""|]
- method get_start_of_input = input_buffer#get_iter_at_mark (`NAME "start_of_input")
-
- method get_insert = get_insert input_buffer
-
- method recenter_insert =
- (* BUG : to investigate further:
- FIXED : Never call GMain.* in thread !
- PLUS : GTK BUG ??? Cannot be called from a thread...
- ADDITION: using sync instead of async causes deadlock...*)
- ignore (GtkThread.async (
- input_view#scroll_to_mark
- ~use_align:false
- ~yalign:0.75
- ~within_margin:0.25)
- `INSERT)
-
-
- method indent_current_line =
- let get_nb_space it =
- let it = it#copy in
- let nb_sep = ref 0 in
- let continue = ref true in
- while !continue do
- if it#char = space then begin
- incr nb_sep;
- if not it#nocopy#forward_char then continue := false;
- end else continue := false
- done;
- !nb_sep
- in
- let previous_line = self#get_insert in
- if previous_line#nocopy#backward_line then begin
- let previous_line_spaces = get_nb_space previous_line in
- let current_line_start = self#get_insert#set_line_offset 0 in
- let current_line_spaces = get_nb_space current_line_start in
- if input_buffer#delete_interactive
- ~start:current_line_start
- ~stop:(current_line_start#forward_chars current_line_spaces)
- ()
- then
- let current_line_start = self#get_insert#set_line_offset 0 in
- input_buffer#insert
- ~iter:current_line_start
- (String.make previous_line_spaces ' ')
- end
+let newfile _ =
+ let session = create_session None in
+ let index = notebook#append_term session in
+ !refresh_editor_hook ();
+ notebook#goto_page index
+let load _ =
+ match select_file_for_open ~title:"Load file" () with
+ | None -> ()
+ | Some f -> FileAux.load_file f
- method go_to_next_occ_of_cur_word =
- let cv = session_notebook#current_term in
- let av = cv.analyzed_view in
- let b = (cv.script)#buffer in
- let start = find_word_start (av#get_insert) in
- let stop = find_word_end start in
- let text = b#get_text ~start ~stop () in
- match stop#forward_search text with
- | None -> ()
- | Some(start, _) ->
- (b#place_cursor start;
- self#recenter_insert)
-
- method go_to_prev_occ_of_cur_word =
- let cv = session_notebook#current_term in
- let av = cv.analyzed_view in
- let b = (cv.script)#buffer in
- let start = find_word_start (av#get_insert) in
- let stop = find_word_end start in
- let text = b#get_text ~start ~stop () in
- match start#backward_search text with
+let save _ = on_current_term (FileAux.check_save ~saveas:false)
+
+let saveas sn =
+ try
+ let filename = sn.fileops#filename in
+ ignore (FileAux.select_and_save ~saveas:true ?filename sn)
+ with _ -> warning "Save Failed"
+
+let saveas = cb_on_current_term saveas
+
+let saveall _ =
+ List.iter
+ (fun sn -> match sn.fileops#filename with
| None -> ()
- | Some(start, _) ->
- (b#place_cursor start;
- self#recenter_insert)
-
- val mutable full_goal_done = true
-
- method show_goals_full =
- if not full_goal_done then
- proof_view#buffer#set_text "";
- begin
- let menu_callback = if !current.contextual_menus_on_goal then
- (fun s () -> ignore (self#insert_this_phrase_on_success
- true true false ("progress "^s) s))
- else
- (fun _ _ -> ()) in
- try
- begin match Coq.goals !mycoqtop with
- | Interface.Fail (l, str) ->
- self#set_message ("Error in coqtop :\n"^str)
- | Interface.Good goals ->
- begin match Coq.evars !mycoqtop with
- | Interface.Fail (l, str) ->
- self#set_message ("Error in coqtop :\n"^str)
- | Interface.Good evs ->
- let hints = match Coq.hints !mycoqtop with
- | Interface.Fail (_, _) -> None
- | Interface.Good hints -> hints
- in
- Ideproof.display
- (Ideproof.mode_tactic menu_callback)
- proof_view goals hints evs
- end
- end
- with
- | e -> prerr_endline (Printexc.to_string e)
- end
+ | Some f -> ignore (sn.fileops#save f))
+ notebook#pages
- method show_goals = self#show_goals_full
+let revert_all _ =
+ List.iter
+ (fun sn -> if sn.fileops#changed_on_disk then sn.fileops#revert)
+ notebook#pages
- method private send_to_coq ct verbose phrase show_output show_error localize =
- let display_output msg =
- self#insert_message (if show_output then msg else "") in
- let display_error (loc,s) =
- if show_error then begin
- if not (Glib.Utf8.validate s) then
- flash_info "This error is so nasty that I can't even display it."
- else begin
- self#insert_message s;
- message_view#misc#draw None;
- if localize then
- (match loc with
- | None -> ()
- | Some (start,stop) ->
- let convert_pos = byte_offset_to_char_offset phrase in
- let start = convert_pos start in
- let stop = convert_pos stop in
- let i = self#get_start_of_input in
- let starti = i#forward_chars start in
- let stopi = i#forward_chars stop in
- input_buffer#apply_tag Tags.Script.error
- ~start:starti
- ~stop:stopi;
- input_buffer#place_cursor ~where:starti)
- end
- end in
- try
- full_goal_done <- false;
- prerr_endline "Send_to_coq starting now";
- (* It's important here to work with [ct] and not [!mycoqtop], otherwise
- we could miss a restart of coqtop and continue sending it orders. *)
- match Coq.interp ct ~verbose 0 phrase with
- | Interface.Fail (l,str) -> sync display_error (l,str); None
- | Interface.Good msg -> sync display_output msg; Some Safe
- with
- | End_of_file -> (* Coqtop has died, let's trigger a reset_initial. *)
- raise RestartCoqtop
- | e -> sync display_error (None, Printexc.to_string e); None
-
- (* This method is intended to perform stateless commands *)
- method raw_coq_query phrase =
- let () = prerr_endline "raw_coq_query starting now" in
- let display_error s =
- if not (Glib.Utf8.validate s) then
- flash_info "This error is so nasty that I can't even display it."
- else begin
- self#insert_message s;
- message_view#misc#draw None
- end
+let quit _ =
+ try FileAux.check_quit saveall; exit 0
+ with FileAux.DontQuit -> ()
+
+let close_buffer sn =
+ let do_remove () = notebook#remove_page notebook#current_page in
+ if not sn.buffer#modified then do_remove ()
+ else
+ let answ = GToolbox.question_box ~title:"Close"
+ ~buttons:["Save Buffer and Close";
+ "Close without Saving";
+ "Don't Close"]
+ ~default:0
+ ~icon:(warn_image ())#coerce
+ "This buffer has unsaved modifications"
in
- try
- match Coq.interp !mycoqtop ~raw:true ~verbose:false 0 phrase with
- | Interface.Fail (_, err) -> sync display_error err
- | Interface.Good msg ->
- sync self#insert_message msg
- with
- | End_of_file -> raise RestartCoqtop
- | e -> sync display_error (Printexc.to_string e)
-
- method find_phrase_starting_at (start:GText.iter) =
- try
- let start = grab_sentence_start start self#get_start_of_input in
- let stop = grab_sentence_stop start in
- (* Is this phrase non-empty and complete ? *)
- if stop#compare start > 0 && is_sentence_end stop#backward_char
- then Some (start,stop)
- else None
- with StartError -> None
-
- method complete_at_offset (offset:int) =
- prerr_endline ("Completion at offset : " ^ string_of_int offset);
- let it () = input_buffer#get_iter (`OFFSET offset) in
- let iit = it () in
- let start = find_word_start iit in
- if ends_word iit then
- let w = input_buffer#get_text
- ~start
- ~stop:iit
- ()
+ match answ with
+ | 1 when FileAux.check_save ~saveas:true sn -> do_remove ()
+ | 2 -> do_remove ()
+ | _ -> ()
+
+let close_buffer = cb_on_current_term close_buffer
+
+let export kind sn =
+ match sn.fileops#filename with
+ |None -> flash_info "Cannot print: this buffer has no name"
+ |Some f ->
+ let basef = Filename.basename f in
+ let output =
+ let basef_we = try Filename.chop_extension basef with _ -> basef in
+ match kind with
+ | "latex" -> basef_we ^ ".tex"
+ | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind
+ | _ -> assert false
in
- if String.length w <> 0 then begin
- prerr_endline ("Completion of prefix : '" ^ w^"'");
- match complete input_buffer w start#offset with
- | None -> false
- | Some (ss,start,stop) ->
- let completion = input_buffer#get_text ~start ~stop () in
- ignore (input_buffer#delete_selection ());
- ignore (input_buffer#insert_interactive completion);
- input_buffer#move_mark `SEL_BOUND ~where:(it())#backward_char;
- true
- end else false
- else false
-
- method private process_one_phrase ct verbosely display_goals do_highlight =
- let get_next_phrase () =
- self#clear_message;
- prerr_endline "process_one_phrase starting now";
- if do_highlight then begin
- push_info "Coq is computing";
- input_view#set_editable false;
- end;
- match self#find_phrase_starting_at self#get_start_of_input with
- | None ->
- if do_highlight then begin
- input_view#set_editable true;
- pop_info ();
- end;
- None
- | Some(start,stop) ->
- prerr_endline "process_one_phrase : to_process highlight";
- if do_highlight then begin
- input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
- prerr_endline "process_one_phrase : to_process applied";
- end;
- prerr_endline "process_one_phrase : getting phrase";
- Some((start,stop),start#get_slice ~stop) in
- let remove_tag (start,stop) =
- if do_highlight then begin
- input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
- input_view#set_editable true;
- pop_info ();
- end in
- let mark_processed safe (start,stop) =
- let b = input_buffer in
- b#move_mark ~where:stop (`NAME "start_of_input");
- b#apply_tag (safety_tag safe) ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- begin
- b#place_cursor ~where:stop;
- self#recenter_insert
- end;
- let ide_payload = { start = `MARK (b#create_mark start);
- stop = `MARK (b#create_mark stop); } in
- Stack.push ide_payload cmd_stack;
- if display_goals then self#show_goals;
- remove_tag (start,stop)
- in
- match sync get_next_phrase () with
- | None -> raise Unsuccessful
- | Some ((_,stop) as loc,phrase) ->
- if stop#backward_char#has_tag Tags.Script.comment
- then sync mark_processed Safe loc
- else try match self#send_to_coq ct verbosely phrase true true true with
- | Some safe -> sync mark_processed safe loc
- | None -> sync remove_tag loc; raise Unsuccessful
- with
- | RestartCoqtop -> sync remove_tag loc; raise RestartCoqtop
-
- method process_next_phrase verbosely =
- try self#process_one_phrase !mycoqtop verbosely true true
- with Unsuccessful -> ()
-
- method private insert_this_phrase_on_success
- show_output show_msg localize coqphrase insertphrase =
- let mark_processed safe =
- let stop = self#get_start_of_input in
- if stop#starts_line then
- input_buffer#insert ~iter:stop insertphrase
- else input_buffer#insert ~iter:stop ("\n"^insertphrase);
- tag_on_insert input_buffer;
- let start = self#get_start_of_input in
- input_buffer#move_mark ~where:stop (`NAME "start_of_input");
- input_buffer#apply_tag (safety_tag safe) ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- input_buffer#place_cursor ~where:stop;
- let ide_payload = { start = `MARK (input_buffer#create_mark start);
- stop = `MARK (input_buffer#create_mark stop); } in
- Stack.push ide_payload cmd_stack;
- self#show_goals;
- (*Auto insert save on success...
- try (match Coq.get_current_goals () with
- | [] ->
- (match self#send_to_coq "Save.\n" true true true with
- | Some ast ->
- begin
- let stop = self#get_start_of_input in
- if stop#starts_line then
- input_buffer#insert ~iter:stop "Save.\n"
- else input_buffer#insert ~iter:stop "\nSave.\n";
- let start = self#get_start_of_input in
- input_buffer#move_mark ~where:stop (`NAME"start_of_input");
- input_buffer#apply_tag_by_name "processed" ~start ~stop;
- if (self#get_insert#compare) stop <= 0 then
- input_buffer#place_cursor stop;
- let start_of_phrase_mark =
- `MARK (input_buffer#create_mark start) in
- let end_of_phrase_mark =
- `MARK (input_buffer#create_mark stop) in
- push_phrase
- reset_info start_of_phrase_mark end_of_phrase_mark ast
- end
- | None -> ())
- | _ -> ())
- with _ -> ()*) in
- match self#send_to_coq !mycoqtop false coqphrase show_output show_msg localize with
- | Some safe -> sync mark_processed safe; true
- | None ->
- sync
- (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase))
- ();
- false
-
- method process_until_iter_or_error stop =
- let stop' = `OFFSET stop#offset in
- let start = self#get_start_of_input#copy in
- let start' = `OFFSET start#offset in
- sync (fun _ ->
- input_buffer#apply_tag Tags.Script.to_process ~start ~stop;
- input_view#set_editable false) ();
- push_info "Coq is computing";
- let get_current () =
- if !current.stop_before then
- match self#find_phrase_starting_at self#get_start_of_input with
- | None -> self#get_start_of_input
- | Some (_, stop2) -> stop2
- else begin
- self#get_start_of_input
- end
- in
- let unlock () =
- sync (fun _ ->
- self#show_goals;
- (* Start and stop might be invalid if an eol was added at eof *)
- let start = input_buffer#get_iter start' in
- let stop = input_buffer#get_iter stop' in
- input_buffer#remove_tag Tags.Script.to_process ~start ~stop;
- input_view#set_editable true) ()
- in
- (* All the [process_one_phrase] below should be done with the same [ct]
- instead of accessing multiple time [mycoqtop]. Otherwise a restart of
- coqtop could go unnoticed, and the new coqtop could receive strange
- things. *)
- let ct = !mycoqtop in
- (try
- while stop#compare (get_current()) >= 0
- do self#process_one_phrase ct false false false done
- with
- | Unsuccessful -> ()
- | RestartCoqtop -> unlock (); raise RestartCoqtop);
- unlock ();
- pop_info()
-
- method process_until_end_or_error =
- self#process_until_iter_or_error input_buffer#end_iter
-
- method reset_initial =
- mycoqtop := Coq.respawn_coqtop !mycoqtop;
- sync (fun () ->
- Stack.iter
- (function inf ->
- let start = input_buffer#get_iter_at_mark inf.start in
- let stop = input_buffer#get_iter_at_mark inf.stop in
- input_buffer#move_mark ~where:start (`NAME "start_of_input");
- input_buffer#remove_tag Tags.Script.processed ~start ~stop;
- input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
- input_buffer#delete_mark inf.start;
- input_buffer#delete_mark inf.stop;
- )
- cmd_stack;
- Stack.clear cmd_stack;
- self#clear_message) ()
-
- method force_reset_initial =
- (* Do nothing if a force_reset_initial is already ongoing *)
- if Mutex.try_lock resetting then begin
- Coq.kill_coqtop !mycoqtop;
- (* If a computation is ongoing, an exception will trigger
- the reset_initial in do_if_not_computing, not here. *)
- if Mutex.try_lock coq_computing then begin
- self#reset_initial;
- Mutex.unlock coq_computing
- end;
- Mutex.unlock resetting
- end
+ let cmd =
+ local_cd f ^ prefs.cmd_coqdoc ^ " --" ^ kind ^ " -o " ^
+ (Filename.quote output) ^ " " ^ (Filename.quote basef) ^ " 2>&1"
+ in
+ sn.messages#set ("Running: "^cmd);
+ let finally st = flash_info (cmd ^ pr_exit_status st)
+ in
+ run_command sn.messages#add finally cmd
- (* Internal method for dialoging with coqtop about a backtrack.
- The ide's cmd_stack has already been cleared up to the desired point.
- The [finish] function is used to handle minor differences between
- [go_to_insert] and [undo_last_step] *)
-
- method private do_backtrack finish n =
- (* pop n more commands if coqtop has said so (e.g. for undoing a proof) *)
- let rec n_pop n =
- if n = 0 then ()
- else
- let phrase = Stack.pop cmd_stack in
- let stop = input_buffer#get_iter_at_mark phrase.stop in
- if stop#backward_char#has_tag Tags.Script.comment
- then n_pop n
- else n_pop (pred n)
- in
- match Coq.rewind !mycoqtop n with
- | Interface.Good n ->
- n_pop n;
- sync (fun _ ->
- let start =
- if Stack.is_empty cmd_stack then input_buffer#start_iter
- else input_buffer#get_iter_at_mark (Stack.top cmd_stack).stop in
- let stop = self#get_start_of_input in
- input_buffer#remove_tag Tags.Script.processed ~start ~stop;
- input_buffer#remove_tag Tags.Script.unjustified ~start ~stop;
- input_buffer#move_mark ~where:start (`NAME "start_of_input");
- self#show_goals;
- self#clear_message;
- finish start) ()
- | Interface.Fail (l,str) ->
- sync self#set_message
- ("Error while backtracking :\n" ^ str ^ "\n" ^
- "CoqIDE and coqtop may be out of sync, you may want to use Restart.")
-
- (* backtrack Coq to the phrase preceding iterator [i] *)
- method backtrack_to_no_lock i =
- prerr_endline "Backtracking_to iter starts now.";
- full_goal_done <- false;
- (* pop Coq commands until we reach iterator [i] *)
- let rec n_step n =
- if Stack.is_empty cmd_stack then n else
- let phrase = Stack.top cmd_stack in
- let stop = input_buffer#get_iter_at_mark phrase.stop in
- if i#compare stop >= 0 then n
- else begin
- ignore (Stack.pop cmd_stack);
- if stop#backward_char#has_tag Tags.Script.comment
- then n_step n
- else n_step (succ n)
- end
- in
- begin
- try
- self#do_backtrack (fun _ -> ()) (n_step 0);
- (* We may have backtracked too much: let's replay *)
- self#process_until_iter_or_error i
- with _ ->
- push_info
- ("WARNING: undo failed badly.\n" ^
- "Coq might be in an inconsistent state.\n" ^
- "Please restart and report.");
- end
+let export kind = cb_on_current_term (export kind)
- method backtrack_to i =
- if Mutex.try_lock coq_may_stop then
- (push_info "Undoing...";
- self#backtrack_to_no_lock i; Mutex.unlock coq_may_stop;
- pop_info ())
- else prerr_endline "backtrack_to : discarded (lock is busy)"
-
- method go_to_insert =
- let point = self#get_insert in
- if point#compare self#get_start_of_input>=0
- then self#process_until_iter_or_error point
- else self#backtrack_to point
-
- method undo_last_step =
- full_goal_done <- false;
- if Mutex.try_lock coq_may_stop then
- (push_info "Undoing last step...";
- (try
- let phrase = Stack.pop cmd_stack in
- let stop = input_buffer#get_iter_at_mark phrase.stop in
- let count =
- if stop#backward_char#has_tag Tags.Script.comment then 0 else 1
- in
- let finish where =
- input_buffer#place_cursor ~where;
- self#recenter_insert;
- in
- self#do_backtrack finish count
- with Stack.Empty -> ()
- );
- pop_info ();
- Mutex.unlock coq_may_stop)
- else prerr_endline "undo_last_step discarded"
-
-
- method insert_command cp ip =
- async(fun _ -> self#clear_message)();
- ignore (self#insert_this_phrase_on_success true false false cp ip)
-
- method tactic_wizard l =
- async(fun _ -> self#clear_message)();
- ignore
- (List.exists
- (fun p ->
- self#insert_this_phrase_on_success true false false
- ("progress "^p^".") (p^".")) l)
-
- method active_keypress_handler k =
- let state = GdkEvent.Key.state k in
- begin
- match state with
- | l ->
- if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
- prerr_endline "active_kp_handler for Tab";
- self#indent_current_line;
- true
- end else false
- end
+let print sn =
+ match sn.fileops#filename with
+ |None -> flash_info "Cannot print: this buffer has no name"
+ |Some f_name ->
+ let cmd =
+ local_cd f_name ^ prefs.cmd_coqdoc ^ " -ps " ^
+ Filename.quote (Filename.basename f_name) ^ " | " ^ prefs.cmd_print
+ in
+ let w = GWindow.window ~title:"Print" ~modal:true
+ ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" ()
+ in
+ let v = GPack.vbox ~spacing:10 ~border_width:10 ~packing:w#add ()
+ in
+ let _ = GMisc.label ~text:"Print using the following command:"
+ ~justify:`LEFT ~packing:v#add ()
+ in
+ let e = GEdit.entry ~text:cmd ~editable:true ~width_chars:80
+ ~packing:v#add ()
+ in
+ let h = GPack.hbox ~spacing:10 ~packing:v#add ()
+ in
+ let ko = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:h#add ()
+ in
+ let ok = GButton.button ~stock:`PRINT ~label:"Print" ~packing:h#add ()
+ in
+ let callback_print () =
+ w#destroy ();
+ let cmd = e#text in
+ let finally st = flash_info (cmd ^ pr_exit_status st) in
+ run_command ignore finally cmd
+ in
+ let _ = ko#connect#clicked ~callback:w#destroy in
+ let _ = ok#connect#clicked ~callback:callback_print in
+ w#misc#show ()
- val mutable act_id = None
+let print = cb_on_current_term print
+
+let highlight sn =
+ Sentence.tag_all sn.buffer;
+ sn.script#recenter_insert
+
+let highlight = cb_on_current_term highlight
- method activate () = if not is_active then begin
- is_active <- true;
- act_id <- Some
- (input_view#event#connect#key_press ~callback:self#active_keypress_handler);
- prerr_endline "CONNECTED active : ";
- print_id (match act_id with Some x -> x | None -> assert false);
- match filename with
- | None -> ()
- | Some f ->
- let dir = Filename.dirname f in
- let ct = !mycoqtop in
- match Coq.inloadpath ct dir with
- | Interface.Fail (_,str) ->
- self#set_message
- ("Could not determine lodpath, this might lead to problems:\n"^str)
- | Interface.Good true -> ()
- | Interface.Good false ->
- let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in
- match Coq.interp ct 0 cmd with
- | Interface.Fail (l,str) ->
- self#set_message ("Couln't add loadpath:\n"^str)
- | Interface.Good _ -> ()
- end
-
- method private electric_paren tag =
- let oparen_code = Glib.Utf8.to_unichar "(" ~pos:(ref 0) in
- let cparen_code = Glib.Utf8.to_unichar ")" ~pos:(ref 0) in
- ignore (input_buffer#connect#insert_text ~callback:
- (fun it x ->
- input_buffer#remove_tag
- ~start:input_buffer#start_iter
- ~stop:input_buffer#end_iter
- tag;
- if x = "" then () else
- match x.[String.length x - 1] with
- | ')' ->
- let hit = self#get_insert in
- let count = ref 0 in
- if hit#nocopy#backward_find_char
- (fun c ->
- if c = oparen_code && !count = 0 then true
- else if c = cparen_code then
- (incr count;false)
- else if c = oparen_code then
- (decr count;false)
- else false
- )
- then
- begin
- prerr_endline "Found matching parenthesis";
- input_buffer#apply_tag tag ~start:hit ~stop:hit#forward_char
- end
- else ()
- | _ -> ())
- )
-
- method help_for_keyword () =
- browse_keyword (self#insert_message) (get_current_word ())
-
-(** NB: Events during text edition:
-
- - [begin_user_action]
- - [insert_text] (or [delete_range] when deleting)
- - [changed]
- - [end_user_action]
-
- When pasting a text containing tags (e.g. the sentence terminators),
- there is actually many [insert_text] and [changed]. For instance,
- for "a. b.":
-
- - [begin_user_action]
- - [insert_text] (for "a")
- - [changed]
- - [insert_text] (for ".")
- - [changed]
- - [apply_tag] (for the tag of ".")
- - [insert_text] (for " b")
- - [changed]
- - [insert_text] (for ".")
- - [changed]
- - [apply_tag] (for the tag of ".")
- - [end_user_action]
-
- Since these copy-pasted tags may interact badly with the retag mechanism,
- we now don't monitor the "changed" event, but rather the "begin_user_action"
- and "end_user_action". We begin by setting a mark at the initial cursor
- point. At the end, the zone between the mark and the cursor is to be
- untagged and then retagged. *)
-
- initializer
- ignore (message_buffer#connect#insert_text
- ~callback:(fun it s -> ignore
- (message_view#scroll_to_mark
- ~use_align:false
- ~within_margin:0.49
- `INSERT)));
- ignore (input_buffer#connect#insert_text
- ~callback:(fun it s ->
- if (it#compare self#get_start_of_input)<0
- then GtkSignal.stop_emit ();
- if String.length s > 1 then
- (prerr_endline "insert_text: Placing cursor";input_buffer#place_cursor ~where:it)));
- ignore (input_buffer#connect#after#apply_tag
- ~callback:(fun tag ~start ~stop ->
- if (start#compare self#get_start_of_input)>=0
- then
- begin
- input_buffer#remove_tag
- Tags.Script.processed
- ~start
- ~stop;
- input_buffer#remove_tag
- Tags.Script.unjustified
- ~start
- ~stop
- end
- )
- );
- ignore (input_buffer#connect#after#insert_text
- ~callback:(fun it s ->
- if auto_complete_on &&
- String.length s = 1 && s <> " " && s <> "\n"
- then
- let v = session_notebook#current_term.analyzed_view
- in
- let has_completed =
- v#complete_at_offset
- ((input_view#buffer#get_iter `SEL_BOUND)#offset)
- in
- if has_completed then
- input_buffer#move_mark `SEL_BOUND ~where:(input_buffer#get_iter `SEL_BOUND)#forward_char;
- )
- );
- ignore (input_buffer#connect#begin_user_action
- ~callback:(fun () ->
- let where = self#get_insert in
- input_buffer#move_mark (`NAME "prev_insert") ~where;
- let start = self#get_start_of_input in
- let stop = input_buffer#end_iter in
- input_buffer#remove_tag Tags.Script.error ~start ~stop)
- );
- ignore (input_buffer#connect#end_user_action
- ~callback:(fun () ->
- last_modification_time <- Unix.time ();
- tag_on_insert input_buffer
- )
- );
- ignore (input_buffer#add_selection_clipboard cb);
- ignore (proof_buffer#add_selection_clipboard cb);
- ignore (message_buffer#add_selection_clipboard cb);
- self#electric_paren Tags.Script.paren;
- ignore (input_buffer#connect#after#mark_set
- ~callback:(fun it (m:Gtk.text_mark) ->
- !set_location
- (Printf.sprintf
- "Line: %5d Char: %3d" (self#get_insert#line + 1)
- (self#get_insert#line_offset + 1));
- match GtkText.Mark.get_name m with
- | Some "insert" ->
- input_buffer#remove_tag
- ~start:input_buffer#start_iter
- ~stop:input_buffer#end_iter
- Tags.Script.paren;
- | Some s ->
- prerr_endline (s^" moved")
- | None -> () )
- );
- ignore (input_buffer#connect#insert_text
- ~callback:(fun it s ->
- prerr_endline "Should recenter ?";
- if String.contains s '\n' then begin
- prerr_endline "Should recenter : yes";
- self#recenter_insert
- end));
end
-let last_make = ref "";;
-let last_make_index = ref 0;;
+(** Timers *)
+
+let reset_revert_timer () =
+ FileOps.revert_timer.kill ();
+ if prefs.global_auto_revert then
+ FileOps.revert_timer.run
+ ~ms:prefs.global_auto_revert_delay
+ ~callback:(fun () -> File.revert_all (); true)
+
+let reset_autosave_timer () =
+ let autosave sn = try sn.fileops#auto_save with _ -> () in
+ let autosave_all () = List.iter autosave notebook#pages; true in
+ FileOps.autosave_timer.kill ();
+ if prefs.auto_save then
+ FileOps.autosave_timer.run ~ms:prefs.auto_save_delay ~callback:autosave_all
+
+(** Export of functions used in [coqide_main] : *)
+
+let forbid_quit () =
+ try FileAux.check_quit File.saveall; false
+ with FileAux.DontQuit -> true
+
+let close_and_quit = FileAux.close_and_quit
+let crash_save = FileAux.crash_save
+let do_load f = FileAux.load_file f
+
+(** Callbacks for external commands *)
+
+module External = struct
+
+let coq_makefile sn =
+ match sn.fileops#filename with
+ |None -> flash_info "Cannot make makefile: this buffer has no name"
+ |Some f ->
+ let cmd = local_cd f ^ prefs.cmd_coqmakefile in
+ let finally st = flash_info (current.cmd_coqmakefile ^ pr_exit_status st)
+ in
+ run_command ignore finally cmd
+
+let coq_makefile = cb_on_current_term coq_makefile
+
+let editor sn =
+ match sn.fileops#filename with
+ |None -> warning "Call to external editor available only on named files"
+ |Some f ->
+ File.save ();
+ let f = Filename.quote f in
+ let cmd = Util.subst_command_placeholder prefs.cmd_editor f in
+ run_command ignore (fun _ -> sn.fileops#revert) cmd
+
+let editor = cb_on_current_term editor
+
+let compile sn =
+ File.save ();
+ match sn.fileops#filename with
+ |None -> flash_info "Active buffer has no name"
+ |Some f ->
+ let cmd = prefs.cmd_coqc ^ " -I " ^ (Filename.quote (Filename.dirname f))
+ ^ " " ^ (Filename.quote f) ^ " 2>&1"
+ in
+ let buf = Buffer.create 1024 in
+ sn.messages#set ("Running: "^cmd);
+ let display s =
+ sn.messages#add s;
+ Buffer.add_string buf s
+ in
+ let finally st =
+ if st = Unix.WEXITED 0 then
+ flash_info (f ^ " successfully compiled")
+ else begin
+ flash_info (f ^ " failed to compile");
+ sn.messages#set "Compilation output:\n";
+ sn.messages#add (Buffer.contents buf);
+ end
+ in
+ run_command display finally cmd
+
+let compile = cb_on_current_term compile
+
+(** [last_make_buf] contains the output of the last make compilation.
+ [last_make] is the same, but as a string, refreshed only when searching
+ the next error. *)
+
+let last_make_buf = Buffer.create 1024
+let last_make = ref ""
+let last_make_index = ref 0
+let last_make_dir = ref ""
+
+let make sn =
+ match sn.fileops#filename with
+ |None -> flash_info "Cannot make: this buffer has no name"
+ |Some f ->
+ File.saveall ();
+ let cmd = local_cd f ^ prefs.cmd_make ^ " 2>&1" in
+ sn.messages#set "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 s;
+ Buffer.add_string last_make_buf s
+ in
+ let finally st = flash_info (current.cmd_make ^ pr_exit_status st)
+ in
+ run_command display finally cmd
+
+let make = cb_on_current_term make
+
let search_compile_error_regexp =
Str.regexp
- "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)";;
+ "File \"\\([^\"]+\\)\", line \\([0-9]+\\), characters \\([0-9]+\\)-\\([0-9]+\\)"
let search_next_error () =
- let _ = Str.search_forward search_compile_error_regexp !last_make !last_make_index in
+ if String.length !last_make <> Buffer.length last_make_buf
+ then last_make := Buffer.contents last_make_buf;
+ let _ =
+ Str.search_forward search_compile_error_regexp !last_make !last_make_index
+ in
let f = Str.matched_group 1 !last_make
and l = int_of_string (Str.matched_group 2 !last_make)
and b = int_of_string (Str.matched_group 3 !last_make)
@@ -1428,1527 +493,938 @@ let search_next_error () =
and msg_index = Str.match_beginning ()
in
last_make_index := Str.group_end 4;
- (f,l,b,e,
+ (Filename.concat !last_make_dir f, l, b, e,
String.sub !last_make msg_index (String.length !last_make - msg_index))
+let next_error sn =
+ try
+ let file,line,start,stop,error_msg = search_next_error () in
+ FileAux.load_file file;
+ let b = sn.buffer in
+ let starti = b#get_iter_at_byte ~line:(line-1) start in
+ 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 error_msg;
+ sn.script#misc#grab_focus ()
+ with Not_found ->
+ last_make_index := 0;
+ sn.messages#set "No more errors.\n"
+
+let next_error = cb_on_current_term next_error
+end
-(**********************************************************************)
-(* session creation and primitive handling *)
-(**********************************************************************)
-
-let create_session file =
- let script =
- Undo.undoable_view
- ~buffer:(GText.buffer ~tag_table:Tags.Script.table ())
- ~wrap_mode:`NONE () in
- let proof =
- GText.view
- ~buffer:(GText.buffer ~tag_table:Tags.Proof.table ())
- ~editable:false ~wrap_mode:`CHAR () in
- let message =
- GText.view
- ~buffer:(GText.buffer ~tag_table:Tags.Message.table ())
- ~editable:false ~wrap_mode:`WORD () in
- let basename = GMisc.label ~text:(match file with
- |None -> "*scratch*"
- |Some f -> (Glib.Convert.filename_to_utf8 (Filename.basename f))
- ) () in
- let stack = Stack.create () in
- let coqtop_args = match file with
- |None -> !sup_args
- |Some the_file -> match !current.read_project with
- |Ignore_args -> !sup_args
- |Append_args -> (Project_file.args_from_project the_file !custom_project_files !current.project_file_name)
- @(!sup_args)
- |Subst_args -> Project_file.args_from_project the_file !custom_project_files !current.project_file_name
- in
- let ct = ref (Coq.spawn_coqtop coqtop_args) in
- let command = new Command_windows.command_window ct current in
- let legacy_av = new analyzed_view script proof message stack ct file in
- let () = legacy_av#update_stats in
- let _ =
- script#buffer#create_mark ~name:"start_of_input" script#buffer#start_iter in
- let _ =
- script#buffer#create_mark ~name:"prev_insert" script#buffer#start_iter in
- let _ =
- proof#buffer#create_mark ~name:"end_of_conclusion" proof#buffer#start_iter in
- let _ =
- GtkBase.Widget.add_events proof#as_widget [`ENTER_NOTIFY;`POINTER_MOTION] in
- let () =
- List.iter (fun (opts,_,_,_,dflt) -> setopts !ct opts dflt) print_items in
- let _ = legacy_av#activate () in
- let _ =
- proof#event#connect#motion_notify ~callback:
- (fun e ->
- let win = match proof#get_window `WIDGET with
- | None -> assert false
- | Some w -> w in
- let x,y = Gdk.Window.get_pointer_location win in
- let b_x,b_y = proof#window_to_buffer_coords ~tag:`WIDGET ~x ~y in
- let it = proof#get_iter_at_location ~x:b_x ~y:b_y in
- let tags = it#tags in
- List.iter
- (fun t ->
- ignore (GtkText.Tag.event t#as_tag proof#as_widget e it#as_iter))
- tags;
- false) in
- script#misc#set_name "ScriptWindow";
- script#buffer#place_cursor ~where:(script#buffer#start_iter);
- proof#misc#set_can_focus true;
- message#misc#set_can_focus true;
- (* setting fonts *)
- script#misc#modify_font !current.text_font;
- proof#misc#modify_font !current.text_font;
- message#misc#modify_font !current.text_font;
- (* setting colors *)
- script#misc#modify_base [`NORMAL, `NAME !current.background_color];
- proof#misc#modify_base [`NORMAL, `NAME !current.background_color];
- message#misc#modify_base [`NORMAL, `NAME !current.background_color];
-
- { tab_label=basename;
- filename=begin match file with None -> "" |Some f -> f end;
- script=script;
- proof_view=proof;
- message_view=message;
- analyzed_view=legacy_av;
- encoding="";
- toplvl=ct;
- command=command
- }
-
-(* XXX - to be used later
- let load_session session filename encs =
- session.encoding <- List.find (IdeIO.load filename session.script#buffer) encs;
- session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename));
- session.filename <- filename;
- session.script#buffer#set_modified false
-
-
- let save_session session filename encs =
- session.encoding <- List.find (IdeIO.save session.script#buffer filename) encs;
- session.tab_label#set_text (Glib.Convert.filename_to_utf8 (Filename.basename filename));
- session.filename <- filename;
- session.script#buffer#set_modified false
-
-
- let init_session session =
- session.script#buffer#set_modified false;
- session.script#clear_undo;
- session.script#buffer#place_cursor session.script#buffer#start_iter
-*)
-
+(** Callbacks for the Navigation menu *)
+let update_status sn =
+ let display msg = pop_info (); push_info msg in
+ let next = function
+ | Interface.Fail x -> sn.coqops#handle_failure x
+ | Interface.Good status ->
+ let path = match status.Interface.status_path with
+ | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
+ | _ :: l -> " in " ^ String.concat "." l
+ in
+ let name = match status.Interface.status_proofname with
+ | None -> ""
+ | Some n -> ", proving " ^ n
+ in
+ display ("Ready"^ if current.nanoPG then ", [μPG]" else "" ^ path ^ name);
+ Coq.return ()
+ in
+ Coq.bind (Coq.status ~logger:sn.messages#push false) next
+
+let find_next_occurrence ~backward sn =
+ (** go to the next occurrence of the current word, forward or backward *)
+ let b = sn.buffer in
+ let start = find_word_start (b#get_iter_at_mark `INSERT) in
+ let stop = find_word_end start in
+ let text = b#get_text ~start ~stop () in
+ let search = if backward then start#backward_search else stop#forward_search
+ in
+ match search text with
+ |None -> ()
+ |Some(where, _) -> b#place_cursor ~where; sn.script#recenter_insert
+
+let send_to_coq_aux f sn =
+ let info () = Minilib.log ("Coq busy, discarding query") in
+ let f = Coq.seq (f sn) (update_status sn) in
+ Coq.try_grab sn.coqtop f info
+
+let send_to_coq f = on_current_term (send_to_coq_aux f)
+
+module Nav = struct
+ let forward_one _ = send_to_coq (fun sn -> sn.coqops#process_next_phrase)
+ let backward_one _ = send_to_coq (fun sn -> sn.coqops#backtrack_last_phrase)
+ let goto _ = send_to_coq (fun sn -> sn.coqops#go_to_insert)
+ let goto_end _ = send_to_coq (fun sn -> sn.coqops#process_until_end_or_error)
+ let previous_occ = cb_on_current_term (find_next_occurrence ~backward:true)
+ let next_occ = cb_on_current_term (find_next_occurrence ~backward:false)
+ let restart sn =
+ Minilib.log "Reset Initial";
+ Coq.reset_coqtop sn.coqtop
+ let restart _ = on_current_term restart
+ let interrupt sn =
+ Minilib.log "User break received";
+ Coq.break_coqtop sn.coqtop
+ let interrupt = cb_on_current_term interrupt
+ let join_document _ = send_to_coq (fun sn -> sn.coqops#join_document)
+end
+let tactic_wizard_callback l _ =
+ send_to_coq (fun sn -> sn.coqops#tactic_wizard l)
+
+let printopts_callback opts v =
+ let b = v#get_active in
+ let () = List.iter (fun o -> Coq.PrintOpt.set o b) opts in
+ send_to_coq (fun sn -> sn.coqops#show_goals)
+
+(** Templates menu *)
+
+let get_current_word term =
+ (** First look to find if autocompleting *)
+ match term.script#complete_popup#proposal with
+ | Some p -> p
+ | None ->
+ (** Then look at the current selected word *)
+ if term.script#buffer#has_selection then
+ let (start, stop) = term.script#buffer#selection_bounds in
+ term.script#buffer#get_text ~slice:true ~start ~stop ()
+ (** Otherwise try to recover the clipboard *)
+ else match Ideutils.cb#text with
+ | Some t -> t
+ | None -> ""
+
+let print_branch c l =
+ Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
+ (Minilib.print_list (fun c s -> Format.fprintf c "%s@ " s)) l
+
+let print_branches c cases =
+ Format.fprintf c "@[match var with@\n%aend@]@."
+ (Minilib.print_list print_branch) cases
+
+let display_match sn = function
+ |Interface.Fail _ ->
+ flash_info "Not an inductive type"; Coq.return ()
+ |Interface.Good cases ->
+ let text =
+ let buf = Buffer.create 1024 in
+ let () = print_branches (Format.formatter_of_buffer buf) cases in
+ Buffer.contents buf
+ in
+ Minilib.log ("match template :\n" ^ text);
+ let b = sn.buffer in
+ let _ = b#delete_selection () in
+ let m = b#create_mark (b#get_iter_at_mark `INSERT) in
+ if b#insert_interactive text then begin
+ let i = b#get_iter (`MARK m) in
+ let _ = i#nocopy#forward_chars 9 in
+ let _ = b#place_cursor ~where:i in
+ b#move_mark ~where:(i#backward_chars 3) `SEL_BOUND
+ end;
+ b#delete_mark (`MARK m);
+ Coq.return ()
+
+let match_callback sn =
+ let w = get_current_word sn in
+ let coqtop = sn.coqtop in
+ let query = Coq.bind (Coq.mkcases w) (display_match sn) in
+ Coq.try_grab coqtop query ignore
+
+let match_callback = cb_on_current_term match_callback
+
+(** Queries *)
+
+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
-(*********************************************************************)
-(* functions called by the user interface *)
-(*********************************************************************)
-(* XXX - to be used later
- let do_open session filename =
- try
- load_session session filename ["UTF-8";"ISO-8859-1";"ISO-8859-15"];
- init_session session;
- ignore (session_notebook#append_term session)
- with _ -> ()
-
-
- let do_save session =
- try
- if session.script#buffer#modified then
- save_session session session.filename [session.encoding]
- with _ -> ()
-
-
- let choose_open =
- let last_filename = ref "" in fun session ->
- let open_dialog = GWindow.file_chooser_dialog ~action:`OPEN ~title:"Open file" ~modal:true () in
- let enc_frame = GBin.frame ~label:"File encoding" ~packing:(open_dialog#vbox#pack ~fill:false) () in
- let enc_entry = GEdit.entry ~text:(String.concat " " ["UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in
- let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok
- ~message:"Invalid encoding, please indicate the encoding to use." () in
- let open_response = function
- | `OPEN -> begin
- match open_dialog#filename with
- | Some fn -> begin
- try
- load_session session fn (Util.split_string_at ' ' enc_entry#text);
- session.analyzed_view <- Some (new analyzed_view session);
- init_session session;
- session_notebook#goto_page (session_notebook#append_term session);
- last_filename := fn
- with
- | Not_found -> open_dialog#misc#hide (); error_dialog#show ()
- | _ ->
- error_dialog#set_markup "Unknown error while loading file, aborting.";
- open_dialog#destroy (); error_dialog#destroy ()
- end
- | None -> ()
- end
- | `DELETE_EVENT -> open_dialog#destroy (); error_dialog#destroy ()
- in
- let _ = open_dialog#connect#response open_response in
- let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); open_dialog#show ()) in
- let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in
- let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in
- open_dialog#add_select_button_stock `OPEN `OPEN;
- open_dialog#add_button_stock `CANCEL `DELETE_EVENT;
- open_dialog#add_filter filter_any;
- open_dialog#add_filter filter_coq;
- ignore(open_dialog#set_filename !last_filename);
- open_dialog#show ()
-
-
- let choose_save session =
- let save_dialog = GWindow.file_chooser_dialog ~action:`SAVE ~title:"Save file" ~modal:true () in
- let enc_frame = GBin.frame ~label:"File encoding" ~packing:(save_dialog#vbox#pack ~fill:false) () in
- let enc_entry = GEdit.entry ~text:(String.concat " " [session.encoding;"UTF-8";"ISO-8859-1";"ISO-8859-15"]) ~packing:enc_frame#add () in
- let error_dialog = GWindow.message_dialog ~message_type:`ERROR ~modal:true ~buttons:GWindow.Buttons.ok
- ~message:"Invalid encoding, please indicate the encoding to use." () in
- let save_response = function
- | `SAVE -> begin
- match save_dialog#filename with
- | Some fn -> begin
- try
- save_session session fn (Util.split_string_at ' ' enc_entry#text)
- with
- | Not_found -> save_dialog#misc#hide (); error_dialog#show ()
- | _ ->
- error_dialog#set_markup "Unknown error while saving file, aborting.";
- save_dialog#destroy (); error_dialog#destroy ()
- end
- | None -> ()
- end
- | `DELETE_EVENT -> save_dialog#destroy (); error_dialog#destroy ()
- in
- let _ = save_dialog#connect#response save_response in
- let _ = error_dialog#connect#response (fun x -> error_dialog#misc#hide (); save_dialog#show ()) in
- let filter_any = GFile.filter ~name:"Any" ~patterns:["*"] () in
- let filter_coq = GFile.filter ~name:"Coq source" ~patterns:["*.v"] () in
- save_dialog#add_select_button_stock `SAVE `SAVE;
- save_dialog#add_button_stock `CANCEL `DELETE_EVENT;
- save_dialog#add_filter filter_any;
- save_dialog#add_filter filter_coq;
- ignore(save_dialog#set_filename session.filename);
- save_dialog#show ()
-*)
+let searchabout () = on_current_term searchabout
-(* Nota: using && here has the advantage of working both under win32 and unix.
- If someday we want the main command to be tried even if the "cd" has failed,
- then we should use " ; " under unix but " & " under win32 (cf. #2363).
-*)
+let otherquery command sn =
+ let word = get_current_word sn in
+ if word <> "" then
+ let query = command ^ " " ^ word ^ "." in
+ sn.messages#clear;
+ Coq.try_grab sn.coqtop (sn.coqops#raw_coq_query query) ignore
-let local_cd file =
- "cd " ^ Filename.quote (Filename.dirname file) ^ " && "
+let otherquery command = cb_on_current_term (otherquery command)
-let do_print session =
- let av = session.analyzed_view in
- match av#filename with
- |None -> flash_info "Cannot print: this buffer has no name"
- |Some f_name -> begin
- let cmd =
- local_cd f_name ^
- !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f_name) ^
- " | " ^ !current.cmd_print
- in
- let print_window = GWindow.window ~title:"Print" ~modal:true ~position:`CENTER ~wm_class:"CoqIDE" ~wm_name: "CoqIDE" () in
- let vbox_print = GPack.vbox ~spacing:10 ~border_width:10 ~packing:print_window#add () in
- let _ = GMisc.label ~justify:`LEFT ~text:"Print using the following command:" ~packing:vbox_print#add () in
- let print_entry = GEdit.entry ~text:cmd ~editable:true ~width_chars:80 ~packing:vbox_print#add () in
- let hbox_print = GPack.hbox ~spacing:10 ~packing:vbox_print#add () in
- let print_cancel_button = GButton.button ~stock:`CANCEL ~label:"Cancel" ~packing:hbox_print#add () in
- let print_button = GButton.button ~stock:`PRINT ~label:"Print" ~packing:hbox_print#add () in
- let callback_print () =
- let cmd = print_entry#text in
- let s,_ = run_command av#insert_message cmd in
- flash_info (cmd ^ if s = Unix.WEXITED 0 then " succeeded" else " failed");
- print_window#destroy ()
- in
- ignore (print_cancel_button#connect#clicked ~callback:print_window#destroy) ;
- ignore (print_button#connect#clicked ~callback:callback_print);
- print_window#misc#show ()
- end
+let query command _ =
+ if command = "Search" || command = "SearchAbout"
+ then searchabout ()
+ else otherquery command ()
-let load_file handler f =
- let f = absolute_filename f in
- try
- prerr_endline "Loading file starts";
- let is_f = Minilib.same_file f in
- if not (Minilib.list_fold_left_i
- (fun i found x -> if found then found else
- let {analyzed_view=av} = x in
- (match av#filename with
- | None -> false
- | Some fn ->
- if is_f fn
- then (session_notebook#goto_page i; true)
- else false))
- 0 false session_notebook#pages)
- then begin
- prerr_endline "Loading: must open";
- let b = Buffer.create 1024 in
- prerr_endline "Loading: get raw content";
- with_file handler f ~f:(input_channel b);
- prerr_endline "Loading: convert content";
- let s = do_convert (Buffer.contents b) in
- prerr_endline "Loading: create view";
- let session = create_session (Some f) in
- prerr_endline "Loading: adding view";
- let index = session_notebook#append_term session in
- let av = session.analyzed_view in
- prerr_endline "Loading: stats";
- av#update_stats;
- let input_buffer = session.script#buffer in
- prerr_endline "Loading: fill buffer";
- input_buffer#set_text s;
- input_buffer#place_cursor ~where:input_buffer#start_iter;
- force_retag input_buffer;
- prerr_endline ("Loading: switch to view "^ string_of_int index);
- session_notebook#goto_page index;
- prerr_endline "Loading: highlight";
- input_buffer#set_modified false;
- prerr_endline "Loading: clear undo";
- session.script#clear_undo;
- prerr_endline "Loading: success"
- end
- with
- | e -> handler ("Load failed: "^(Printexc.to_string e))
-
-let do_load = load_file flash_info
-
-let saveall_f () =
- List.iter
- (function
- | {script = view ; analyzed_view = av} ->
- begin match av#filename with
- | None -> ()
- | Some f ->
- ignore (av#save f)
- end
- ) session_notebook#pages
-
-let forbid_quit_to_save () =
- begin try save_pref() with e -> flash_info "Cannot save preferences" end;
- (if List.exists
- (function
- | {script=view} -> view#buffer#modified
- )
- session_notebook#pages then
- match (GToolbox.question_box ~title:"Quit"
- ~buttons:["Save Named Buffers and Quit";
- "Quit without Saving";
- "Don't Quit"]
- ~default:0
- ~icon:
- (let img = GMisc.image () in
- img#set_stock `DIALOG_WARNING;
- img#set_icon_size `DIALOG;
- img#coerce)
- "There are unsaved buffers"
- )
- with 1 -> saveall_f () ; false
- | 2 -> false
- | _ -> true
- else false)||
- (let wait_window =
- GWindow.window ~modal:true ~wm_class:"CoqIde" ~wm_name:"CoqIde" ~kind:`POPUP
- ~title:"Terminating coqtops" () in
- let _ =
- GMisc.label ~text:"Terminating coqtops processes, please wait ..."
- ~packing:wait_window#add () in
- let warning_window =
- GWindow.message_dialog ~message_type:`WARNING ~buttons:GWindow.Buttons.yes_no
- ~message:
- ("Some coqtops processes are still running.\n" ^
- "If you quit CoqIDE right now, you may have to kill them manually.\n" ^
- "Do you want to wait for those processes to terminate ?") () in
- let () = List.iter (fun _ -> session_notebook#remove_page 0) session_notebook#pages in
- let nb_try=ref (0) in
- let () = wait_window#show () in
- let () = while (Coq.coqtop_zombies () <> 0)&&(!nb_try <= 50) do
- incr nb_try;
- Thread.delay 0.1 ;
- done in
- if (!nb_try = 50) then begin
- wait_window#misc#hide ();
- match warning_window#run () with
- | `YES -> warning_window#misc#hide (); true
- | `NO | `DELETE_EVENT -> false
- end
- else false)
+end
-let logfile = ref None
+(** Misc *)
-let main files =
+module MiscMenu = struct
- (* Main window *)
- let w = GWindow.window
- ~wm_class:"CoqIde" ~wm_name:"CoqIde"
- ~allow_grow:true ~allow_shrink:true
- ~width:!current.window_width ~height:!current.window_height
- ~title:"CoqIde" ()
- in
- (try
- let icon_image = Filename.concat (List.find
- (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
- Minilib.xdg_data_dirs) "coq.png" in
- let icon = GdkPixbuf.from_file icon_image in
- w#set_icon (Some icon)
- with _ -> ());
+let detach_view sn = sn.control#detach ()
- let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
+let detach_view = cb_on_current_term detach_view
- let new_f _ =
- let session = create_session None in
- let index = session_notebook#append_term session in
- session_notebook#goto_page index
- in
- let load_f _ =
- match select_file_for_open ~title:"Load file" () with
- | None -> ()
- | Some f -> do_load f
- in
- let save_f _ =
- let current = session_notebook#current_term in
- try
- (match current.analyzed_view#filename with
- | None ->
- begin match select_file_for_save ~title:"Save file" ()
- with
- | None -> ()
- | Some f ->
- if current.analyzed_view#save_as f then begin
- current.tab_label#set_text (Filename.basename f);
- flash_info ("File " ^ f ^ " saved")
- end
- else warning ("Save Failed (check if " ^ f ^ " is writable)")
- end
- | Some f ->
- if current.analyzed_view#save f then
- flash_info ("File " ^ f ^ " saved")
- else warning ("Save Failed (check if " ^ f ^ " is writable)")
-
- )
- with
- | e -> warning "Save: unexpected error"
- in
- let saveas_f _ =
- let current = session_notebook#current_term in
- try (match current.analyzed_view#filename with
- | None ->
- begin match select_file_for_save ~title:"Save file as" ()
- with
- | None -> ()
- | Some f ->
- if current.analyzed_view#save_as f then begin
- current.tab_label#set_text (Filename.basename f);
- flash_info "Saved"
- end
- else flash_info "Save Failed"
- end
- | Some f ->
- begin match select_file_for_save
- ~dir:(ref (Filename.dirname f))
- ~filename:(Filename.basename f)
- ~title:"Save file as" ()
- with
- | None -> ()
- | Some f ->
- if current.analyzed_view#save_as f then begin
- current.tab_label#set_text (Filename.basename f);
- flash_info "Saved"
- end else flash_info "Save Failed"
- end);
- with e -> flash_info "Save Failed"
- in
- let revert_f {analyzed_view = av} =
- (try
- match av#filename,av#stats with
- | Some f,Some stats ->
- let new_stats = Unix.stat f in
- if new_stats.Unix.st_mtime > stats.Unix.st_mtime
- then av#revert
- | Some _, None -> av#revert
- | _ -> ()
- with _ -> av#revert)
- in
- let export_f kind _ =
- let v = session_notebook#current_term in
- let av = v.analyzed_view in
- match av#filename with
- | None ->
- flash_info "Cannot print: this buffer has no name"
- | Some f ->
- let basef = Filename.basename f in
- let output =
- let basef_we = try Filename.chop_extension basef with _ -> basef in
- match kind with
- | "latex" -> basef_we ^ ".tex"
- | "dvi" | "ps" | "pdf" | "html" -> basef_we ^ "." ^ kind
- | _ -> assert false
- in
- let cmd =
- local_cd f ^ !current.cmd_coqdoc ^ " --" ^ kind ^
- " -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
- in
- let s,_ = run_command av#insert_message cmd in
- flash_info (cmd ^
- if s = Unix.WEXITED 0
- then " succeeded"
- else " failed")
- in
- let quit_f _ = if not (forbid_quit_to_save ()) then exit 0 in
- let get_active_view_for_cp () =
- let has_sel (i0,i1) = i0#compare i1 <> 0 in
- let current = session_notebook#current_term in
- if has_sel current.script#buffer#selection_bounds
- then current.script#as_view
- else if has_sel current.proof_view#buffer#selection_bounds
- then current.proof_view#as_view
- else current.message_view#as_view
- in
- (*
- let toggle_auto_complete_i =
- edit_f#add_check_item "_Auto Completion"
- ~active:!current.auto_complete
- ~callback:
- in
- *)
- (*
- auto_complete :=
- (fun b -> match session_notebook#current_term.analyzed_view with
- | Some av -> av#set_auto_complete b
- | None -> ());
- *)
-
-(* begin of find/replace mechanism *)
- let last_found = ref None in
- let search_backward = ref false in
- let find_w = GWindow.window
- (* ~wm_class:"CoqIde" ~wm_name:"CoqIde" *)
- (* ~allow_grow:true ~allow_shrink:true *)
- (* ~width:!current.window_width ~height:!current.window_height *)
- ~position:`CENTER
- ~title:"CoqIde search/replace" ()
- in
- let find_box = GPack.table
- ~columns:3 ~rows:5
- ~col_spacings:10 ~row_spacings:10 ~border_width:10
- ~homogeneous:false ~packing:find_w#add () in
+let log_file_message () =
+ if !Minilib.debug then
+ let file = match !logfile with None -> "stderr" | Some f -> f in
+ "\nDebug mode is on, log file is "^file
+ else ""
- let _ =
- GMisc.label ~text:"Find:"
- ~xalign:1.0
- ~packing:(find_box#attach ~left:0 ~top:0 ~fill:`X) ()
+let initial_about () =
+ let initial_string =
+ "Welcome to CoqIDE, an Integrated Development Environment for Coq"
in
- let find_entry = GEdit.entry
- ~editable: true
- ~packing: (find_box#attach ~left:1 ~top:0 ~expand:`X)
- ()
+ let coq_version = Coq.short_version () in
+ let version_info =
+ if Glib.Utf8.validate coq_version then
+ "\nYou are running " ^ coq_version
+ else ""
in
+ let msg = initial_string ^ version_info ^ log_file_message () in
+ on_current_term (fun term -> term.messages#add msg)
+
+let coq_icon () =
+ (* May raise Nof_found *)
+ let name = "coq.png" in
+ let chk d = Sys.file_exists (Filename.concat d name) in
+ let dir = List.find chk (Minilib.coqide_data_dirs ()) in
+ Filename.concat dir name
+
+let about _ =
+ let dialog = GWindow.about_dialog () in
+ let _ = dialog#connect#response ~callback:(fun _ -> dialog#destroy ()) in
let _ =
- GMisc.label ~text:"Replace with:"
- ~xalign:1.0
- ~packing:(find_box#attach ~left:0 ~top:1 ~fill:`X) ()
- in
- let replace_entry = GEdit.entry
- ~editable: true
- ~packing: (find_box#attach ~left:1 ~top:1 ~expand:`X)
- ()
- in
- (* let _ =
- GButton.check_button
- ~label:"case sensitive"
- ~active:true
- ~packing: (find_box#attach ~left:1 ~top:2)
- ()
- in
- *)
- let find_backwards_check =
- GButton.check_button
- ~label:"search backwards"
- ~active:!search_backward
- ~packing: (find_box#attach ~left:1 ~top:3)
- ()
- in
- let close_find_button =
- GButton.button
- ~label:"Close"
- ~packing: (find_box#attach ~left:2 ~top:2)
- ()
- in
- let replace_find_button =
- GButton.button
- ~label:"Replace and find"
- ~packing: (find_box#attach ~left:2 ~top:1)
- ()
- in
- let find_again_button =
- GButton.button
- ~label:"_Find again"
- ~packing: (find_box#attach ~left:2 ~top:0)
- ()
- in
- let last_find () =
- let v = session_notebook#current_term.script in
- let b = v#buffer in
- let start,stop =
- match !last_found with
- | None -> let i = b#get_iter_at_mark `INSERT in (i,i)
- | Some(start,stop) ->
- let start = b#get_iter_at_mark start
- and stop = b#get_iter_at_mark stop
- in
- b#remove_tag Tags.Script.found ~start ~stop;
- last_found:=None;
- start,stop
- in
- (v,b,start,stop)
+ try dialog#set_logo (GdkPixbuf.from_file (coq_icon ()))
+ with _ -> ()
in
- let do_replace () =
- let v = session_notebook#current_term.script in
- let b = v#buffer in
- match !last_found with
- | None -> ()
- | Some(start,stop) ->
- let start = b#get_iter_at_mark start
- and stop = b#get_iter_at_mark stop
- in
- b#delete ~start ~stop;
- b#insert ~iter:start replace_entry#text;
- last_found:=None
+ let copyright =
+ "Coq is developed by the Coq Development Team\n\
+ (INRIA - CNRS - LIX - LRI - PPS)"
in
- let find_from (v : Undo.undoable_view)
- (b : GText.buffer) (starti : GText.iter) text =
- prerr_endline ("Searching for " ^ text);
- match (if !search_backward then starti#backward_search text
- else starti#forward_search text)
- with
- | None -> ()
- | Some(start,stop) ->
- b#apply_tag Tags.Script.found ~start ~stop;
- let start = `MARK (b#create_mark start)
- and stop = `MARK (b#create_mark stop)
- in
- v#scroll_to_mark ~use_align:false ~yalign:0.75 ~within_margin:0.25
- stop;
- last_found := Some(start,stop)
+ let authors = [
+ "Benjamin Monate";
+ "Jean-Christophe Filliâtre";
+ "Pierre Letouzey";
+ "Claude Marché";
+ "Bruno Barras";
+ "Pierre Corbineau";
+ "Julien Narboux";
+ "Hugo Herbelin";
+ "Enrico Tassi";
+ ]
in
- let do_find () =
- let (v,b,starti,_) = last_find () in
- find_from v b starti find_entry#text
+ dialog#set_name "CoqIDE";
+ dialog#set_comments "The Coq Integrated Development Environment";
+ dialog#set_website Coq_config.wwwcoq;
+ dialog#set_version Coq_config.version;
+ dialog#set_copyright copyright;
+ dialog#set_authors authors;
+ dialog#show ()
+
+let comment = cb_on_current_term (fun t -> t.script#comment ())
+let uncomment = cb_on_current_term (fun t -> t.script#uncomment ())
+
+let coqtop_arguments sn =
+ let dialog = GWindow.dialog ~title:"Coqtop arguments" () in
+ let coqtop = sn.coqtop in
+ (** Text entry *)
+ let args = Coq.get_arguments coqtop in
+ let text = String.concat " " args in
+ let entry = GEdit.entry ~text ~packing:dialog#vbox#add () in
+ (** Buttons *)
+ let box = dialog#action_area in
+ let ok = GButton.button ~stock:`OK ~packing:box#add () in
+ let ok_cb () =
+ let nargs = CString.split ' ' entry#text in
+ if nargs <> args then
+ let failed = Coq.filter_coq_opts nargs in
+ match failed with
+ | [] ->
+ let () = Coq.set_arguments coqtop nargs in
+ dialog#destroy ()
+ | args ->
+ let args = String.concat " " args in
+ let msg = Printf.sprintf "Invalid arguments: %s" args in
+ let () = sn.messages#clear in
+ sn.messages#push Pp.Error msg
+ else dialog#destroy ()
in
- let do_replace_find () =
- do_replace();
- do_find()
+ let _ = entry#connect#activate ok_cb in
+ let _ = ok#connect#clicked 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
+ dialog#show ()
+
+let coqtop_arguments = cb_on_current_term coqtop_arguments
+
+let show_hide_query_pane sn =
+ let ccw = sn.command in
+ if ccw#visible then ccw#hide else ccw#show
+
+let zoom_fit sn =
+ let script = sn.script in
+ let space = script#misc#allocation.Gtk.width in
+ let cols = script#right_margin_position in
+ let pango_ctx = script#misc#pango_context in
+ let layout = pango_ctx#create_layout in
+ let fsize = Pango.Font.get_size current.text_font in
+ Pango.Layout.set_text layout (String.make cols 'X');
+ let tlen = fst (Pango.Layout.get_pixel_size layout) in
+ Pango.Font.set_size current.text_font
+ (fsize * space / tlen / Pango.scale * Pango.scale);
+ save_pref ();
+ !refresh_editor_hook ()
+
+end
+
+(** Refresh functions *)
+
+let refresh_editor_prefs () =
+ let wrap_mode = if prefs.dynamic_word_wrap then `WORD else `NONE in
+ let show_spaces =
+ if prefs.show_spaces then 0b1001011 (* SPACE, TAB, NBSP, TRAILING *)
+ else 0
in
- let close_find () =
- let (v,b,_,stop) = last_find () in
- b#place_cursor ~where:stop;
- find_w#misc#hide();
- v#coerce#misc#grab_focus()
+ let fd = prefs.text_font in
+ let clr = Tags.color_of_string prefs.background_color
in
- to_do_on_page_switch :=
- (fun i -> if find_w#misc#visible then close_find())::
- !to_do_on_page_switch;
- let find_again () =
- let (v,b,start,_) = last_find () in
- let start =
- if !search_backward
- then start#backward_chars 1
- else start#forward_chars 1
+ let iter_session sn =
+ (* Editor settings *)
+ sn.script#set_wrap_mode wrap_mode;
+ sn.script#set_show_line_numbers prefs.show_line_number;
+ sn.script#set_auto_indent prefs.auto_indent;
+ sn.script#set_highlight_current_line prefs.highlight_current_line;
+
+ (* Hack to handle missing binding in lablgtk *)
+ let conv = { Gobject.name = "draw-spaces"; Gobject.conv = Gobject.Data.int }
in
- find_from v b start find_entry#text
+ Gobject.set conv sn.script#as_widget show_spaces;
+
+ sn.script#set_show_right_margin prefs.show_right_margin;
+ if prefs.show_progress_bar then sn.segment#misc#show () else sn.segment#misc#hide ();
+ sn.script#set_insert_spaces_instead_of_tabs
+ prefs.spaces_instead_of_tabs;
+ sn.script#set_tab_width prefs.tab_length;
+ sn.script#set_auto_complete prefs.auto_complete;
+
+ (* Fonts *)
+ sn.script#misc#modify_font fd;
+ sn.proof#misc#modify_font fd;
+ sn.messages#modify_font fd;
+ sn.command#refresh_font ();
+
+ (* Colors *)
+ sn.script#misc#modify_base [`NORMAL, `COLOR clr];
+ sn.proof#misc#modify_base [`NORMAL, `COLOR clr];
+ sn.messages#misc#modify_base [`NORMAL, `COLOR clr];
+ sn.command#refresh_color ()
+
in
- let click_on_backward () =
- search_backward := not !search_backward
+ List.iter iter_session notebook#pages
+
+let refresh_notebook_pos () =
+ let pos = match prefs.vertical_tabs, prefs.opposite_tabs with
+ | false, false -> `TOP
+ | false, true -> `BOTTOM
+ | true , false -> `LEFT
+ | true , true -> `RIGHT
in
- let key_find ev =
- let s = GdkEvent.Key.state ev and k = GdkEvent.Key.keyval ev in
- if k = GdkKeysyms._Escape then
- begin
- let (v,b,_,stop) = last_find () in
- find_w#misc#hide();
- v#coerce#misc#grab_focus();
- true
- end
- else if k = GdkKeysyms._Escape then
- begin
- close_find();
- true
- end
- else if k = GdkKeysyms._Return ||
- List.mem `CONTROL s && k = GdkKeysyms._f then
- begin
- find_again ();
- true
- end
- else if List.mem `CONTROL s && k = GdkKeysyms._b then
- begin
- find_backwards_check#set_active (not !search_backward);
- true
- end
- else false (* to let default callback execute *)
+ notebook#set_tab_pos pos
+
+(** Wrappers around GAction functions for creating menus *)
+
+let menu = GAction.add_actions
+let item = GAction.add_action
+
+(** Toggle items in menus for printing options *)
+
+let toggle_item = GAction.add_toggle_action
+
+(** Search the first '_' in a label string and return the following
+ character as shortcut, plus the string without the '_' *)
+
+let get_shortcut s =
+ try
+ let n = String.length s in
+ let i = String.index s '_' in
+ let k = String.make 1 s.[i+1] in
+ let s' = (String.sub s 0 i) ^ (String.sub s (i+1) (n-i-1)) in
+ Some k, s'
+ with _ -> None,s
+
+module Opt = Coq.PrintOpt
+
+let toggle_items menu_name l =
+ let f d =
+ let label = d.Opt.label in
+ let k, name = get_shortcut label in
+ let accel = Option.map ((^) prefs.modifier_for_display) k in
+ toggle_item name ~label ?accel ~active:d.Opt.init
+ ~callback:(printopts_callback d.Opt.opts)
+ menu_name
in
- let find_f ~backward () =
- let save_dir = !search_backward in
- search_backward := backward;
- find_w#show ();
- find_w#present ();
- find_entry#misc#grab_focus ();
- search_backward := save_dir
+ List.iter f l
+
+(** Create alphabetical menu items with elements in sub-items.
+ [l] is a list of lists, one per initial letter *)
+
+let alpha_items menu_name item_name l =
+ let no_under = Util.String.map (fun x -> if x = '_' then '-' else x)
in
- let _ = find_again_button#connect#clicked find_again in
- let _ = close_find_button#connect#clicked close_find in
- let _ = replace_find_button#connect#clicked do_replace_find in
- let _ = find_backwards_check#connect#clicked click_on_backward in
- let _ = find_entry#connect#changed do_find in
- let _ = find_entry#event#connect#key_press ~callback:key_find in
- let _ = find_w#event#connect#delete ~callback:(fun _ -> find_w#misc#hide(); true) in
- (*
- let search_if = edit_f#add_item "Search _forward"
- ~key:GdkKeysyms._greater
- in
- let search_ib = edit_f#add_item "Search _backward"
- ~key:GdkKeysyms._less
+ let mk_item text =
+ let text' =
+ let last = String.length text - 1 in
+ if text.[last] = '.'
+ then text ^"\n"
+ else text ^" "
in
- *)
- (*
- let complete_i = edit_f#add_item "_Complete"
- ~key:GdkKeysyms._comma
- ~callback:
- (do_if_not_computing
- (fun b ->
- let v = session_notebook#current_term.analyzed_view
-
- in v#complete_at_offset
- ((v#view#buffer#get_iter `SEL_BOUND)#offset)
- ))
+ let callback _ =
+ on_current_term (fun sn -> sn.buffer#insert_interactive text')
in
- complete_i#misc#set_state `INSENSITIVE;
- *)
-(* end of find/replace mechanism *)
-(* begin Preferences *)
- let reset_revert_timer () =
- disconnect_revert_timer ();
- if !current.global_auto_revert then
- revert_timer := Some
- (GMain.Timeout.add ~ms:!current.global_auto_revert_delay
- ~callback:
- (fun () ->
- do_if_not_computing "revert" (sync revert_f) session_notebook#pages;
- true))
- in reset_revert_timer (); (* to enable statup preferences timer *)
- (* XXX *)
- let auto_save_f {analyzed_view = av} =
- (try
- av#auto_save
- with _ -> ())
- in
-
- let reset_auto_save_timer () =
- disconnect_auto_save_timer ();
- if !current.auto_save then
- auto_save_timer := Some
- (GMain.Timeout.add ~ms:!current.auto_save_delay
- ~callback:
- (fun () ->
- do_if_not_computing "autosave" (sync auto_save_f) session_notebook#pages;
- true))
- in reset_auto_save_timer (); (* to enable statup preferences timer *)
-(* end Preferences *)
-
- let do_or_activate f () =
- do_if_not_computing "do_or_activate"
- (fun current ->
- let av = current.analyzed_view in
- ignore (f av);
- pop_info ();
- let msg = match Coq.status !(current.toplvl) with
- | Interface.Fail (l, str) ->
- "Oops, problem while fetching coq status."
- | Interface.Good status ->
- let path = match status.Interface.status_path with
- | [] | _ :: [] -> "" (* Drop the topmost level, usually "Top" *)
- | _ :: l -> " in " ^ String.concat "." l
- in
- let name = match status.Interface.status_proofname with
- | None -> ""
- | Some n -> ", proving " ^ n
- in
- "Ready" ^ path ^ name
- in
- push_info msg
- )
- [session_notebook#current_term]
- in
- let do_if_active f _ =
- do_if_not_computing "do_if_active"
- (fun sess -> ignore (f sess.analyzed_view))
- [session_notebook#current_term] in
- let match_callback _ =
- let w = get_current_word () in
- let cur_ct = !(session_notebook#current_term.toplvl) in
- try
- match Coq.mkcases cur_ct w with
- | Interface.Fail _ -> raise Not_found
- | Interface.Good cases ->
- let print_branch c l =
- Format.fprintf c " | @[<hov 1>%a@]=> _@\n"
- (print_list (fun c s -> Format.fprintf c "%s@ " s)) l
- in
- let b = Buffer.create 1024 in
- let fmt = Format.formatter_of_buffer b in
- Format.fprintf fmt "@[match var with@\n%aend@]@."
- (print_list print_branch) cases;
- let s = Buffer.contents b in
- prerr_endline s;
- let {script = view } = session_notebook#current_term in
- ignore (view#buffer#delete_selection ());
- let m = view#buffer#create_mark
- (view#buffer#get_iter `INSERT)
- in
- if view#buffer#insert_interactive s then
- let i = view#buffer#get_iter (`MARK m) in
- let _ = i#nocopy#forward_chars 9 in
- view#buffer#place_cursor ~where:i;
- view#buffer#move_mark ~where:(i#backward_chars 3)
- `SEL_BOUND
- with Not_found -> flash_info "Not an inductive type"
- in
-(* External command callback *)
- let compile_f _ =
- let v = session_notebook#current_term in
- let av = v.analyzed_view in
- save_f ();
- match av#filename with
- | None ->
- flash_info "Active buffer has no name"
- | Some f ->
- let cmd = !current.cmd_coqc ^ " -I "
- ^ (Filename.quote (Filename.dirname f))
- ^ " " ^ (Filename.quote f) in
- let s,res = run_command av#insert_message cmd in
- if s = Unix.WEXITED 0 then
- flash_info (f ^ " successfully compiled")
- else begin
- flash_info (f ^ " failed to compile");
- av#process_until_end_or_error;
- av#insert_message "Compilation output:\n";
- av#insert_message res
- end
- in
- let make_f _ =
- let v = session_notebook#current_term in
- let av = v.analyzed_view in
- match av#filename with
- | None ->
- flash_info "Cannot make: this buffer has no name"
- | Some f ->
- let cmd = local_cd f ^ !current.cmd_make in
-
- (*
- save_f ();
- *)
- av#insert_message "Command output:\n";
- let s,res = run_command av#insert_message cmd in
- last_make := res;
- last_make_index := 0;
- flash_info (!current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
+ item (item_name^" "^(no_under text)) ~label:text ~callback menu_name
in
- let next_error _ =
- try
- let file,line,start,stop,error_msg = search_next_error () in
- do_load file;
- let v = session_notebook#current_term in
- let av = v.analyzed_view in
- let input_buffer = v.script#buffer in
- (*
- let init = input_buffer#start_iter in
- let i = init#forward_lines (line-1) in
- *)
- (*
- let convert_pos = byte_offset_to_char_offset phrase in
- let start = convert_pos start in
- let stop = convert_pos stop in
- *)
- (*
- let starti = i#forward_chars start in
- let stopi = i#forward_chars stop in
- *)
- let starti = input_buffer#get_iter_at_byte ~line:(line-1) start in
- let stopi = input_buffer#get_iter_at_byte ~line:(line-1) stop in
- input_buffer#apply_tag Tags.Script.error
- ~start:starti
- ~stop:stopi;
- input_buffer#place_cursor ~where:starti;
- av#set_message error_msg;
- v.script#misc#grab_focus ()
- with Not_found ->
- last_make_index := 0;
- let v = session_notebook#current_term in
- let av = v.analyzed_view in
- av#set_message "No more errors.\n"
+ let mk_items = function
+ | [] -> ()
+ | [s] -> mk_item s
+ | s::_ as ll ->
+ let name = item_name^" "^(String.make 1 s.[0]) in
+ let label = "_@..." in label.[1] <- s.[0];
+ item name ~label menu_name;
+ List.iter mk_item ll
in
- let coq_makefile_f _ =
- let v = session_notebook#current_term in
- let av = v.analyzed_view in
- match av#filename with
- | None ->
- flash_info "Cannot make makefile: this buffer has no name"
- | Some f ->
- let cmd = local_cd f ^ !current.cmd_coqmakefile in
- let s,res = run_command av#insert_message cmd in
- flash_info
- (!current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
+ List.iter mk_items l
+
+(** Create a menu item that will insert a given text,
+ and select the zone given by (offset,len).
+ The first word in the text is used as item keyword.
+ Caveat: the offset is now from the start of the text. *)
+
+let template_item (text, offset, len, key) =
+ let modifier = prefs.modifier_for_templates in
+ let idx = String.index text ' ' in
+ let name = String.sub text 0 idx in
+ let label = "_"^name^" __" in
+ let negoffset = String.length text - offset - len in
+ let callback sn =
+ let b = sn.buffer in
+ if b#insert_interactive text then begin
+ let iter = b#get_iter_at_mark `INSERT in
+ ignore (iter#nocopy#backward_chars negoffset);
+ b#move_mark `INSERT ~where:iter;
+ ignore (iter#nocopy#backward_chars len);
+ b#move_mark `SEL_BOUND ~where:iter;
+ end
in
+ item name ~label ~callback:(cb_on_current_term callback) ~accel:(modifier^key)
- let file_actions = GAction.action_group ~name:"File" () in
- let edit_actions = GAction.action_group ~name:"Edit" () in
- let view_actions = GAction.action_group ~name:"View" () in
- let export_actions = GAction.action_group ~name:"Export" () in
- let navigation_actions = GAction.action_group ~name:"Navigation" () in
- let tactics_actions = GAction.action_group ~name:"Tactics" () in
- let templates_actions = GAction.action_group ~name:"Templates" () in
- let queries_actions = GAction.action_group ~name:"Queries" () in
- let compile_actions = GAction.action_group ~name:"Compile" () in
- let windows_actions = GAction.action_group ~name:"Windows" () in
- let help_actions = GAction.action_group ~name:"Help" () in
- let add_gen_actions menu_name act_grp l =
- let no_under = Minilib.string_map (fun x -> if x = '_' then '-' else x) in
- let add_simple_template menu_name act_grp text =
- let text' =
- let l = String.length text - 1 in
- if String.get text l = '.'
- then text ^"\n"
- else text ^" "
- in
- GAction.add_action (menu_name^" "^(no_under text)) ~label:text
- ~callback:(fun _ -> let {script = view } = session_notebook#current_term in
- ignore (view#buffer#insert_interactive text')) act_grp
- in
- List.iter (function
- | [] -> ()
- | [s] -> add_simple_template menu_name act_grp s
- | s::_ as ll -> let label = "_@..." in label.[1] <- s.[0];
- GAction.add_action (menu_name^" "^(String.make 1 s.[0])) ~label act_grp;
- List.iter (add_simple_template menu_name act_grp) ll
- ) l
- in
- let tactic_shortcut s sc = GAction.add_action s ~label:("_"^s)
- ~accel:(!current.modifier_for_tactics^sc)
- ~callback:(do_if_active (fun a -> a#insert_command
- ("progress "^s^".") (s^"."))) in
- let query_callback command _ =
- let word = get_current_word () in
- if not (word = "") then
- let term = session_notebook#current_term in
- let query = command ^ " " ^ word ^ "." in
- term.message_view#buffer#set_text "";
- term.analyzed_view#raw_coq_query query
- in
- let query_shortcut s accel =
- GAction.add_action s ~label:("_"^s) ?accel ~callback:(query_callback s)
- in
- let add_complex_template (name, label, text, offset, len, key) =
- (* Templates/Lemma *)
- let callback _ =
- let {script = view } = session_notebook#current_term in
- if view#buffer#insert_interactive text then begin
- let iter = view#buffer#get_iter_at_mark `INSERT in
- ignore (iter#nocopy#backward_chars offset);
- view#buffer#move_mark `INSERT ~where:iter;
- ignore (iter#nocopy#backward_chars len);
- view#buffer#move_mark `SEL_BOUND ~where:iter;
- end in
- match key with
- |Some ac -> GAction.add_action name ~label ~callback ~accel:(!current.modifier_for_templates^ac)
- |None -> GAction.add_action name ~label ~callback ?accel:None
+let emit_to_focus window sgn =
+ let focussed_widget = GtkWindow.Window.get_focus window#as_window in
+ let obj = Gobject.unsafe_cast focussed_widget in
+ try GtkSignal.emit_unit obj ~sgn with _ -> ()
+
+(** {2 Creation of the main coqide window } *)
+
+let build_ui () =
+ let w = GWindow.window
+ ~wm_class:"CoqIde" ~wm_name:"CoqIde"
+ ~allow_grow:true ~allow_shrink:true
+ ~width:prefs.window_width ~height:prefs.window_height
+ ~title:"CoqIde" ()
in
- let detach_view _ =
- (* Open a separate window containing the current buffer *)
- let trm = session_notebook#current_term in
- let w = GWindow.window ~show:true
- ~width:(!current.window_width*2/3)
- ~height:(!current.window_height*2/3)
- ~position:`CENTER
- ~title:(if trm.filename = "" then "*scratch*" else trm.filename)
- ()
- in
- let sb = GBin.scrolled_window ~packing:w#add ()
- in
- let nv = GText.view ~buffer:trm.script#buffer ~packing:sb#add ()
- in
- nv#misc#modify_font !current.text_font;
- (* If the buffer in the main window is closed, destroy this detached view *)
- ignore (trm.script#connect#destroy ~callback:w#destroy)
+ let () =
+ try w#set_icon (Some (GdkPixbuf.from_file (MiscMenu.coq_icon ())))
+ with _ -> ()
in
- GAction.add_actions file_actions [
- GAction.add_action "File" ~label:"_File";
- GAction.add_action "New" ~callback:new_f ~stock:`NEW;
- GAction.add_action "Open" ~callback:load_f ~stock:`OPEN;
- GAction.add_action "Save" ~callback:save_f ~stock:`SAVE ~tooltip:"Save current buffer";
- GAction.add_action "Save as" ~label:"S_ave as" ~callback:saveas_f ~stock:`SAVE_AS;
- GAction.add_action "Save all" ~label:"Sa_ve all" ~callback:(fun _ -> saveall_f ());
- GAction.add_action "Revert all buffers" ~label:"_Revert all buffers" ~callback:(fun _ -> List.iter revert_f session_notebook#pages) ~stock:`REVERT_TO_SAVED;
- GAction.add_action "Close buffer" ~label:"_Close buffer" ~callback:(fun _ -> remove_current_view_page ()) ~stock:`CLOSE ~tooltip:"Close current buffer";
- GAction.add_action "Print..." ~label:"_Print..." ~callback:(fun _ -> do_print session_notebook#current_term) ~stock:`PRINT ~accel:"<Ctrl>p";
- GAction.add_action "Rehighlight" ~label:"Reh_ighlight" ~accel:"<Ctrl>l"
- ~callback:(fun _ -> force_retag
- session_notebook#current_term.script#buffer;
- session_notebook#current_term.analyzed_view#recenter_insert)
- ~stock:`REFRESH;
- GAction.add_action "Quit" ~callback:quit_f ~stock:`QUIT;
- ];
- GAction.add_actions export_actions [
- GAction.add_action "Export to" ~label:"E_xport to";
- GAction.add_action "Html" ~label:"_Html" ~callback:(export_f "html");
- GAction.add_action "Latex" ~label:"_LaTeX" ~callback:(export_f "latex");
- GAction.add_action "Dvi" ~label:"_Dvi" ~callback:(export_f "dvi");
- GAction.add_action "Pdf" ~label:"_Pdf" ~callback:(export_f "pdf");
- GAction.add_action "Ps" ~label:"_Ps" ~callback:(export_f "ps");
- ];
- GAction.add_actions edit_actions [
- GAction.add_action "Edit" ~label:"_Edit";
- GAction.add_action "Undo" ~accel:"<Ctrl>u"
- ~callback:(fun _ -> do_if_not_computing "undo"
- (fun sess ->
- ignore (sess.analyzed_view#without_auto_complete
- (fun () -> session_notebook#current_term.script#undo) ()))
- [session_notebook#current_term]) ~stock:`UNDO;
- GAction.add_action "Clear Undo Stack" ~label:"_Clear Undo Stack"
- ~callback:(fun _ -> ignore session_notebook#current_term.script#clear_undo);
- GAction.add_action "Cut" ~callback:(fun _ -> GtkSignal.emit_unit
- (get_active_view_for_cp ())
- ~sgn:GtkText.View.S.cut_clipboard
- ) ~stock:`CUT;
- GAction.add_action "Copy" ~callback:(fun _ -> GtkSignal.emit_unit
- (get_active_view_for_cp ())
- ~sgn:GtkText.View.S.copy_clipboard) ~stock:`COPY;
- GAction.add_action "Paste" ~callback:(fun _ ->
- try GtkSignal.emit_unit
- session_notebook#current_term.script#as_view
- ~sgn:GtkText.View.S.paste_clipboard
- with _ -> prerr_endline "EMIT PASTE FAILED") ~stock:`PASTE;
- GAction.add_action "Find in buffer" ~label:"_Find in buffer" ~callback:(fun _ -> find_f ~backward:false ()) ~stock:`FIND;
- GAction.add_action "Find backwards" ~label:"Find _backwards" ~callback:(fun _ -> find_f ~backward:true ()) ~accel:"<Ctrl>b";
- GAction.add_action "Complete Word" ~label:"Complete Word" ~callback:(fun _ ->
- ignore (
- let av = session_notebook#current_term.analyzed_view in
- av#complete_at_offset (av#get_insert)#offset
- )) ~accel:"<Ctrl>slash";
- GAction.add_action "External editor" ~label:"External editor" ~callback:(fun _ ->
- let av = session_notebook#current_term.analyzed_view in
- match av#filename with
- | None -> warning "Call to external editor available only on named files"
- | Some f ->
- save_f ();
- let com = Minilib.subst_command_placeholder !current.cmd_editor (Filename.quote f) in
- let _ = run_command av#insert_message com in
- av#revert) ~stock:`EDIT;
- GAction.add_action "Preferences" ~callback:(fun _ ->
- begin
- try configure ~apply:update_notebook_pos ()
+ let _ = w#event#connect#delete ~callback:(fun _ -> File.quit (); true) in
+ let _ = set_drag w#drag in
+
+ let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
+
+ let file_menu = GAction.action_group ~name:"File" () in
+ let edit_menu = GAction.action_group ~name:"Edit" () in
+ let view_menu = GAction.action_group ~name:"View" () in
+ let export_menu = GAction.action_group ~name:"Export" () in
+ let navigation_menu = GAction.action_group ~name:"Navigation" () in
+ let tactics_menu = GAction.action_group ~name:"Tactics" () in
+ let templates_menu = GAction.action_group ~name:"Templates" () in
+ let tools_menu = GAction.action_group ~name:"Tools" () in
+ let queries_menu = GAction.action_group ~name:"Queries" () in
+ let compile_menu = GAction.action_group ~name:"Compile" () in
+ let windows_menu = GAction.action_group ~name:"Windows" () in
+ let help_menu = GAction.action_group ~name:"Help" () in
+ let all_menus = [
+ file_menu; edit_menu; view_menu; export_menu; navigation_menu; tactics_menu;
+ templates_menu; tools_menu; queries_menu; compile_menu; windows_menu;
+ help_menu; ] in
+
+ menu file_menu [
+ item "File" ~label:"_File";
+ item "New" ~callback:File.newfile ~stock:`NEW;
+ item "Open" ~callback:File.load ~stock:`OPEN;
+ item "Save" ~callback:File.save ~stock:`SAVE ~tooltip:"Save current buffer";
+ item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:File.saveas;
+ item "Save all" ~label:"Sa_ve all" ~callback:File.saveall;
+ item "Revert all buffers" ~label:"_Revert all buffers"
+ ~callback:File.revert_all ~stock:`REVERT_TO_SAVED;
+ item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE
+ ~callback:File.close_buffer ~tooltip:"Close current buffer";
+ item "Print..." ~label:"_Print..."
+ ~callback:File.print ~stock:`PRINT ~accel:"<Ctrl>p";
+ item "Rehighlight" ~label:"Reh_ighlight" ~accel:"<Ctrl>l"
+ ~callback:File.highlight ~stock:`REFRESH;
+ item "Quit" ~stock:`QUIT ~callback:File.quit;
+ ];
+
+ menu export_menu [
+ item "Export to" ~label:"E_xport to";
+ item "Html" ~label:"_Html" ~callback:(File.export "html");
+ item "Latex" ~label:"_LaTeX" ~callback:(File.export "latex");
+ item "Dvi" ~label:"_Dvi" ~callback:(File.export "dvi");
+ item "Pdf" ~label:"_Pdf" ~callback:(File.export "pdf");
+ item "Ps" ~label:"_Ps" ~callback:(File.export "ps");
+ ];
+
+ menu edit_menu [
+ item "Edit" ~label:"_Edit";
+ item "Undo" ~accel:"<Ctrl>u" ~stock:`UNDO
+ ~callback:(cb_on_current_term (fun t -> t.script#undo ()));
+ item "Redo" ~stock:`REDO
+ ~callback:(cb_on_current_term (fun t -> t.script#redo ()));
+ item "Cut" ~stock:`CUT
+ ~callback:(fun _ -> emit_to_focus w GtkText.View.S.cut_clipboard);
+ item "Copy" ~stock:`COPY
+ ~callback:(fun _ -> emit_to_focus w GtkText.View.S.copy_clipboard);
+ item "Paste" ~stock:`PASTE
+ ~callback:(fun _ -> emit_to_focus w GtkText.View.S.paste_clipboard);
+ item "Find" ~stock:`FIND ~label:"Find / Replace"
+ ~callback:(cb_on_current_term (fun t -> t.finder#show ()));
+ item "Find Next" ~label:"Find _Next" ~stock:`GO_DOWN ~accel:"F3"
+ ~callback:(cb_on_current_term (fun t -> t.finder#find_forward ()));
+ item "Find Previous" ~label:"Find _Previous" ~stock:`GO_UP
+ ~accel:"<Shift>F3"
+ ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ()));
+ item "Complete Word" ~label:"Complete Word" ~accel:"<Ctrl>slash"
+ ~callback:(fun _ -> ());
+ item "External editor" ~label:"External editor" ~stock:`EDIT
+ ~callback:External.editor;
+ item "Preferences" ~accel:"<Ctrl>comma" ~stock:`PREFERENCES
+ ~callback:(fun _ ->
+ begin
+ try Preferences.configure ~apply:refresh_notebook_pos ()
with _ -> flash_info "Cannot save preferences"
- end;
- reset_revert_timer ()) ~accel:"<Ctrl>comma" ~stock:`PREFERENCES;
- (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
- GAction.add_actions view_actions [
- GAction.add_action "View" ~label:"_View";
- GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<ALT>Left") ~stock:`GO_BACK
- ~callback:(fun _ -> session_notebook#previous_page ());
- GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<ALT>Right") ~stock:`GO_FORWARD
- ~callback:(fun _ -> session_notebook#next_page ());
- GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar"
- ~active:(!current.show_toolbar) ~callback:
- (fun _ -> !current.show_toolbar <- not !current.show_toolbar;
- !refresh_toolbar_hook ());
- GAction.add_toggle_action "Show Query Pane" ~label:"Show _Query Pane"
- ~callback:(fun _ -> let ccw = session_notebook#current_term.command in
- if ccw#frame#misc#visible
- then ccw#frame#misc#hide ()
- else ccw#frame#misc#show ())
- ~accel:"Escape";
- ];
- List.iter
- (fun (opts,name,label,key,dflt) ->
- GAction.add_toggle_action name ~active:dflt ~label
- ~accel:(!current.modifier_for_display^key)
- ~callback:(fun v -> do_or_activate (fun a ->
- let () = setopts !(session_notebook#current_term.toplvl) opts v#get_active in
- a#show_goals) ()) view_actions)
- print_items;
- GAction.add_actions navigation_actions [
- GAction.add_action "Navigation" ~label:"_Navigation";
- GAction.add_action "Forward" ~label:"_Forward" ~stock:`GO_DOWN
- ~callback:(fun _ -> do_or_activate (fun a -> a#process_next_phrase true) ())
- ~tooltip:"Forward one command" ~accel:(!current.modifier_for_navigation^"Down");
- GAction.add_action "Backward" ~label:"_Backward" ~stock:`GO_UP
- ~callback:(fun _ -> do_or_activate (fun a -> a#undo_last_step) ())
- ~tooltip:"Backward one command" ~accel:(!current.modifier_for_navigation^"Up");
- GAction.add_action "Go to" ~label:"_Go to" ~stock:`JUMP_TO
- ~callback:(fun _ -> do_or_activate (fun a -> a#go_to_insert) ())
- ~tooltip:"Go to cursor" ~accel:(!current.modifier_for_navigation^"Right");
- GAction.add_action "Start" ~label:"_Start" ~stock:`GOTO_TOP
- ~callback:(fun _ -> force_reset_initial ())
- ~tooltip:"Restart coq" ~accel:(!current.modifier_for_navigation^"Home");
- GAction.add_action "End" ~label:"_End" ~stock:`GOTO_BOTTOM
- ~callback:(fun _ -> do_or_activate (fun a -> a#process_until_end_or_error) ())
- ~tooltip:"Go to end" ~accel:(!current.modifier_for_navigation^"End");
- GAction.add_action "Interrupt" ~label:"_Interrupt" ~stock:`STOP
- ~callback:(fun _ -> break ()) ~tooltip:"Interrupt computations"
- ~accel:(!current.modifier_for_navigation^"Break");
- GAction.add_action "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE
- ~callback:(fun _ -> let sess = session_notebook#current_term in
- toggle_proof_visibility sess.script#buffer
+ end;
+ reset_revert_timer ());
+ ];
+
+ menu view_menu [
+ item "View" ~label:"_View";
+ item "Previous tab" ~label:"_Previous tab" ~accel:"<Alt>Left"
+ ~stock:`GO_BACK
+ ~callback:(fun _ -> notebook#previous_page ());
+ item "Next tab" ~label:"_Next tab" ~accel:"<Alt>Right"
+ ~stock:`GO_FORWARD
+ ~callback:(fun _ -> notebook#next_page ());
+ item "Zoom in" ~label:"_Zoom in" ~accel:("<Control>plus")
+ ~stock:`ZOOM_IN ~callback:(fun _ ->
+ Pango.Font.set_size current.text_font
+ (Pango.Font.get_size current.text_font + Pango.scale);
+ save_pref ();
+ !refresh_editor_hook ());
+ item "Zoom out" ~label:"_Zoom out" ~accel:("<Control>minus")
+ ~stock:`ZOOM_OUT ~callback:(fun _ ->
+ Pango.Font.set_size current.text_font
+ (Pango.Font.get_size current.text_font - Pango.scale);
+ save_pref ();
+ !refresh_editor_hook ());
+ item "Zoom fit" ~label:"_Zoom fit" ~accel:("<Control>0")
+ ~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit);
+ toggle_item "Show Toolbar" ~label:"Show _Toolbar"
+ ~active:(prefs.show_toolbar)
+ ~callback:(fun _ ->
+ prefs.show_toolbar <- not prefs.show_toolbar;
+ !refresh_toolbar_hook ());
+ item "Query Pane" ~label:"_Query Pane"
+ ~accel:"F1"
+ ~callback:(cb_on_current_term MiscMenu.show_hide_query_pane)
+ ];
+ toggle_items view_menu Coq.PrintOpt.bool_items;
+
+ menu navigation_menu [
+ item "Navigation" ~label:"_Navigation";
+ item "Forward" ~label:"_Forward" ~stock:`GO_DOWN ~callback:Nav.forward_one
+ ~tooltip:"Forward one command"
+ ~accel:(prefs.modifier_for_navigation^"Down");
+ item "Backward" ~label:"_Backward" ~stock:`GO_UP ~callback:Nav.backward_one
+ ~tooltip:"Backward one command"
+ ~accel:(prefs.modifier_for_navigation^"Up");
+ item "Go to" ~label:"_Go to" ~stock:`JUMP_TO ~callback:Nav.goto
+ ~tooltip:"Go to cursor"
+ ~accel:(prefs.modifier_for_navigation^"Right");
+ item "Start" ~label:"_Start" ~stock:`GOTO_TOP ~callback:Nav.restart
+ ~tooltip:"Restart coq"
+ ~accel:(prefs.modifier_for_navigation^"Home");
+ item "End" ~label:"_End" ~stock:`GOTO_BOTTOM ~callback:Nav.goto_end
+ ~tooltip:"Go to end"
+ ~accel:(prefs.modifier_for_navigation^"End");
+ item "Interrupt" ~label:"_Interrupt" ~stock:`STOP ~callback:Nav.interrupt
+ ~tooltip:"Interrupt computations"
+ ~accel:(prefs.modifier_for_navigation^"Break");
+(* wait for this available in GtkSourceView !
+ item "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE
+ ~callback:(fun _ -> let sess = notebook#current_term in
+ toggle_proof_visibility sess.buffer
sess.analyzed_view#get_insert) ~tooltip:"Hide proof"
- ~accel:(!current.modifier_for_navigation^"h");
- GAction.add_action "Previous" ~label:"_Previous" ~stock:`GO_BACK
- ~callback:(fun _ -> do_or_activate (fun a -> a#go_to_prev_occ_of_cur_word) ())
- ~tooltip:"Previous occurence" ~accel:(!current.modifier_for_navigation^"less");
- GAction.add_action "Next" ~label:"_Next" ~stock:`GO_FORWARD
- ~callback:(fun _ -> do_or_activate (fun a -> a#go_to_next_occ_of_cur_word) ())
- ~tooltip:"Next occurence" ~accel:(!current.modifier_for_navigation^"greater");
- ];
- GAction.add_actions tactics_actions [
- GAction.add_action "Try Tactics" ~label:"_Try Tactics";
- GAction.add_action "Wizard" ~tooltip:"Proof Wizard" ~label:"<Proof Wizard>"
- ~stock:`DIALOG_INFO ~callback:(do_if_active (fun a -> a#tactic_wizard
- !current.automatic_tactics))
- ~accel:(!current.modifier_for_tactics^"dollar");
- tactic_shortcut "auto" "a";
- tactic_shortcut "auto with *" "asterisk";
- tactic_shortcut "eauto" "e";
- tactic_shortcut "eauto with *" "ampersand";
- tactic_shortcut "intuition" "i";
- tactic_shortcut "omega" "o";
- tactic_shortcut "simpl" "s";
- tactic_shortcut "tauto" "p";
- tactic_shortcut "trivial" "v";
- ];
- add_gen_actions "Tactic" tactics_actions Coq_commands.tactics;
- GAction.add_actions templates_actions [
- GAction.add_action "Templates" ~label:"Te_mplates";
- add_complex_template
- ("Lemma", "_Lemma __", "Lemma new_lemma : .\nIdeproof.\n\nSave.\n",
- 19, 9, Some "L");
- add_complex_template
- ("Theorem", "_Theorem __", "Theorem new_theorem : .\nIdeproof.\n\nSave.\n",
- 19, 11, Some "T");
- add_complex_template
- ("Definition", "_Definition __", "Definition ident := .\n",
- 6, 5, Some "D");
- add_complex_template
- ("Inductive", "_Inductive __", "Inductive ident : :=\n | : .\n",
- 14, 5, Some "I");
- add_complex_template
- ("Fixpoint", "_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n",
- 29, 5, Some "F");
- add_complex_template ("Scheme", "_Scheme __",
- "Scheme new_scheme := Induction for _ Sort _\
-\nwith _ := Induction for _ Sort _.\n",61,10, Some "S");
- GAction.add_action "match" ~label:"match ..." ~callback:match_callback
- ~accel:(!current.modifier_for_templates^"C");
- ];
- add_gen_actions "Template" templates_actions Coq_commands.commands;
- GAction.add_actions queries_actions [
- GAction.add_action "Queries" ~label:"_Queries";
- query_shortcut "SearchAbout" (Some "F2");
- query_shortcut "Check" (Some "F3");
- query_shortcut "Print" (Some "F4");
- query_shortcut "About" (Some "F5");
- query_shortcut "Locate" None;
- query_shortcut "Whelp Locate" None;
- ];
- GAction.add_actions compile_actions [
- GAction.add_action "Compile" ~label:"_Compile";
- GAction.add_action "Compile buffer" ~label:"_Compile buffer" ~callback:compile_f;
- GAction.add_action "Make" ~label:"_Make" ~callback:make_f ~accel:"F6";
- GAction.add_action "Next error" ~label:"_Next error" ~callback:next_error
- ~accel:"F7";
- GAction.add_action "Make makefile" ~label:"Make makefile" ~callback:coq_makefile_f;
- ];
- GAction.add_actions windows_actions [
- GAction.add_action "Windows" ~label:"_Windows";
- GAction.add_action "Detach View" ~label:"Detach _View" ~callback:detach_view
- ];
- GAction.add_actions help_actions [
- GAction.add_action "Help" ~label:"_Help";
- GAction.add_action "Browse Coq Manual" ~label:"Browse Coq _Manual"
- ~callback:(fun _ ->
- let av = session_notebook#current_term.analyzed_view in
- browse av#insert_message (doc_url ()));
- GAction.add_action "Browse Coq Library" ~label:"Browse Coq _Library"
- ~callback:(fun _ ->
- let av = session_notebook#current_term.analyzed_view in
- browse av#insert_message !current.library_url);
- GAction.add_action "Help for keyword" ~label:"Help for _keyword"
- ~callback:(fun _ -> let av = session_notebook#current_term.analyzed_view in
- av#help_for_keyword ()) ~stock:`HELP;
- GAction.add_action "About Coq" ~label:"_About" ~stock:`ABOUT;
- ];
- Coqide_ui.init ();
- Coqide_ui.ui_m#insert_action_group file_actions 0;
- Coqide_ui.ui_m#insert_action_group export_actions 0;
- Coqide_ui.ui_m#insert_action_group edit_actions 0;
- Coqide_ui.ui_m#insert_action_group view_actions 0;
- Coqide_ui.ui_m#insert_action_group navigation_actions 0;
- Coqide_ui.ui_m#insert_action_group tactics_actions 0;
- Coqide_ui.ui_m#insert_action_group templates_actions 0;
- Coqide_ui.ui_m#insert_action_group queries_actions 0;
- Coqide_ui.ui_m#insert_action_group compile_actions 0;
- Coqide_ui.ui_m#insert_action_group windows_actions 0;
- Coqide_ui.ui_m#insert_action_group help_actions 0;
- w#add_accel_group Coqide_ui.ui_m#get_accel_group ;
- GtkMain.Rc.parse_string "gtk-can-change-accels = 1";
- if Coq_config.gtk_platform <> `QUARTZ
- then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar");
- let tbar = GtkButton.Toolbar.cast ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
- in let () = GtkButton.Toolbar.set ~orientation:`HORIZONTAL ~style:`ICONS
- ~tooltips:true tbar in
- let toolbar = new GObj.widget tbar in
- vbox#pack toolbar;
-
- ignore (w#event#connect#delete ~callback:(fun _ -> quit_f (); true));
-
- (* The vertical Separator between Scripts and Goals *)
- vbox#pack ~expand:true session_notebook#coerce;
- update_notebook_pos ();
- let nb = session_notebook in
- let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
- lower_hbox#pack ~expand:true status#coerce;
- let search_lbl = GMisc.label ~text:"Search:"
- ~show:false
- ~packing:(lower_hbox#pack ~expand:false) ()
+ ~accel:(prefs.modifier_for_navigation^"h");*)
+ item "Previous" ~label:"_Previous" ~stock:`GO_BACK
+ ~callback:Nav.previous_occ
+ ~tooltip:"Previous occurence"
+ ~accel:(prefs.modifier_for_navigation^"less");
+ item "Next" ~label:"_Next" ~stock:`GO_FORWARD ~callback:Nav.next_occ
+ ~tooltip:"Next occurence"
+ ~accel:(prefs.modifier_for_navigation^"greater");
+ item "Force" ~label:"_Force" ~stock:`EXECUTE ~callback:Nav.join_document
+ ~tooltip:"Fully check the document"
+ ~accel:(current.modifier_for_navigation^"f");
+ ];
+
+ let tacitem s sc =
+ item s ~label:("_"^s)
+ ~accel:(prefs.modifier_for_tactics^sc)
+ ~callback:(tactic_wizard_callback [s])
+ in
+ menu tactics_menu [
+ item "Try Tactics" ~label:"_Try Tactics";
+ item "Wizard" ~label:"<Proof Wizard>" ~stock:`DIALOG_INFO
+ ~tooltip:"Proof Wizard" ~accel:(prefs.modifier_for_tactics^"dollar")
+ ~callback:(tactic_wizard_callback prefs.automatic_tactics);
+ tacitem "auto" "a";
+ tacitem "auto with *" "asterisk";
+ tacitem "eauto" "e";
+ tacitem "eauto with *" "ampersand";
+ tacitem "intuition" "i";
+ tacitem "omega" "o";
+ tacitem "simpl" "s";
+ tacitem "tauto" "p";
+ tacitem "trivial" "v";
+ ];
+ alpha_items tactics_menu "Tactic" Coq_commands.tactics;
+
+ menu templates_menu [
+ item "Templates" ~label:"Te_mplates";
+ template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "L");
+ template_item ("Theorem new_theorem : .\nProof.\n\nSave.\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");
+ template_item ("Scheme new_scheme := Induction for _ Sort _\n" ^
+ "with _ := Induction for _ Sort _.\n", 7,10, "S");
+ item "match" ~label:"match ..." ~accel:(prefs.modifier_for_templates^"C")
+ ~callback:match_callback
+ ];
+ alpha_items templates_menu "Template" Coq_commands.commands;
+
+ let qitem s accel = item s ~label:("_"^s) ?accel ~callback:(Query.query s) in
+ menu queries_menu [
+ item "Queries" ~label:"_Queries";
+ qitem "Search" (Some "F2");
+ qitem "Check" (Some "F3");
+ qitem "Print" (Some "F4");
+ qitem "About" (Some "F5");
+ qitem "Locate" None;
+ qitem "Print Assumptions" None;
+ qitem "Whelp Locate" None;
+ ];
+
+ menu tools_menu [
+ item "Tools" ~label:"_Tools";
+ item "Comment" ~label:"_Comment" ~accel:"<CTRL>D"
+ ~callback:MiscMenu.comment;
+ item "Uncomment" ~label:"_Uncomment" ~accel:"<CTRL><SHIFT>D"
+ ~callback:MiscMenu.uncomment;
+ item "Coqtop arguments" ~label:"Coqtop _arguments"
+ ~callback:MiscMenu.coqtop_arguments;
+ ];
+
+ menu compile_menu [
+ item "Compile" ~label:"_Compile";
+ item "Compile buffer" ~label:"_Compile buffer" ~callback:External.compile;
+ item "Make" ~label:"_Make" ~accel:"F6"
+ ~callback:External.make;
+ item "Next error" ~label:"_Next error" ~accel:"F7"
+ ~callback:External.next_error;
+ item "Make makefile" ~label:"Make makefile" ~callback:External.coq_makefile;
+ ];
+
+ menu windows_menu [
+ item "Windows" ~label:"_Windows";
+ item "Detach View" ~label:"Detach _View" ~callback:MiscMenu.detach_view
+ ];
+
+ menu help_menu [
+ item "Help" ~label:"_Help";
+ item "Browse Coq Manual" ~label:"Browse Coq _Manual"
+ ~callback:(fun _ ->
+ browse notebook#current_term.messages#add (doc_url ()));
+ item "Browse Coq Library" ~label:"Browse Coq _Library"
+ ~callback:(fun _ ->
+ browse notebook#current_term.messages#add prefs.library_url);
+ item "Help for keyword" ~label:"Help for _keyword" ~stock:`HELP
+ ~callback:(fun _ -> on_current_term (fun sn ->
+ browse_keyword sn.messages#add (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 (NanoPG.get_documentation ())));
+ item "About Coq" ~label:"_About" ~stock:`ABOUT
+ ~callback:MiscMenu.about
+ ];
+
+ Coqide_ui.init ();
+ Coqide_ui.ui_m#insert_action_group file_menu 0;
+ Coqide_ui.ui_m#insert_action_group export_menu 0;
+ Coqide_ui.ui_m#insert_action_group edit_menu 0;
+ Coqide_ui.ui_m#insert_action_group view_menu 0;
+ Coqide_ui.ui_m#insert_action_group navigation_menu 0;
+ Coqide_ui.ui_m#insert_action_group tactics_menu 0;
+ Coqide_ui.ui_m#insert_action_group templates_menu 0;
+ Coqide_ui.ui_m#insert_action_group tools_menu 0;
+ Coqide_ui.ui_m#insert_action_group queries_menu 0;
+ Coqide_ui.ui_m#insert_action_group compile_menu 0;
+ Coqide_ui.ui_m#insert_action_group windows_menu 0;
+ Coqide_ui.ui_m#insert_action_group help_menu 0;
+ w#add_accel_group Coqide_ui.ui_m#get_accel_group ;
+ GtkMain.Rc.parse_string "gtk-can-change-accels = 1";
+ if Coq_config.gtk_platform <> `QUARTZ
+ then vbox#pack (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar");
+
+ (* Toolbar *)
+ let tbar = GtkButton.Toolbar.cast
+ ((Coqide_ui.ui_m#get_widget "/CoqIde ToolBar")#as_widget)
in
- let search_history = ref [] in
- let (search_input,_) = GEdit.combo_box_entry_text ~strings:!search_history ~show:false
- ~packing:(lower_hbox#pack ~expand:false) ()
+ let () = GtkButton.Toolbar.set
+ ~orientation:`HORIZONTAL ~style:`ICONS ~tooltips:true tbar
in
- let ready_to_wrap_search = ref false in
+ let toolbar = new GObj.widget tbar in
+ let () = vbox#pack toolbar in
- let start_of_search = ref None in
- let start_of_found = ref None in
- let end_of_found = ref None in
- let search_forward = ref true in
- let matched_word = ref None in
+ (* Emacs/PG mode *)
+ NanoPG.init w notebook all_menus;
- let memo_search () =
- matched_word := Some search_input#entry#text
+ (* Reset on tab switch *)
+ let _ = notebook#connect#switch_page ~callback:(fun _ ->
+ if prefs.reset_on_tab_switch then Nav.restart ())
in
- let end_search () =
- prerr_endline "End Search";
- memo_search ();
- let v = session_notebook#current_term.script in
- v#buffer#move_mark `SEL_BOUND ~where:(v#buffer#get_iter_at_mark `INSERT);
- v#coerce#misc#grab_focus ();
- search_input#entry#set_text "";
- search_lbl#misc#hide ();
- search_input#misc#hide ()
- in
- let end_search_focus_out () =
- prerr_endline "End Search(focus out)";
- memo_search ();
- let v = session_notebook#current_term.script in
- v#buffer#move_mark `SEL_BOUND ~where:(v#buffer#get_iter_at_mark `INSERT);
- search_input#entry#set_text "";
- search_lbl#misc#hide ();
- search_input#misc#hide ()
- in
- ignore (search_input#entry#connect#activate ~callback:end_search);
- ignore (search_input#entry#event#connect#key_press
- ~callback:(fun k -> let kv = GdkEvent.Key.keyval k in
- if
- kv = GdkKeysyms._Right
- || kv = GdkKeysyms._Up
- || kv = GdkKeysyms._Left
- || (kv = GdkKeysyms._g
- && (List.mem `CONTROL (GdkEvent.Key.state k)))
- then end_search ();
- false));
- ignore (search_input#entry#event#connect#focus_out
- ~callback:(fun _ -> end_search_focus_out (); false));
- to_do_on_page_switch :=
- (fun i ->
- start_of_search := None;
- ready_to_wrap_search:=false)::!to_do_on_page_switch;
-
- (* TODO : make it work !!! *)
- let rec search_f () =
- search_lbl#misc#show ();
- search_input#misc#show ();
-
- prerr_endline "search_f called";
- if !start_of_search = None then begin
- (* A full new search is starting *)
- start_of_search :=
- Some (session_notebook#current_term.script#buffer#create_mark
- (session_notebook#current_term.script#buffer#get_iter_at_mark `INSERT));
- start_of_found := !start_of_search;
- end_of_found := !start_of_search;
- matched_word := Some "";
- end;
- let txt = search_input#entry#text in
- let v = session_notebook#current_term.script in
- let iit = v#buffer#get_iter_at_mark `SEL_BOUND
- and insert_iter = v#buffer#get_iter_at_mark `INSERT
- in
- prerr_endline ("SELBOUND="^(string_of_int iit#offset));
- prerr_endline ("INSERT="^(string_of_int insert_iter#offset));
-
- (match
- if !search_forward then iit#forward_search txt
- else let npi = iit#forward_chars (Glib.Utf8.length txt) in
- match
- (npi#offset = (v#buffer#get_iter_at_mark `INSERT)#offset),
- (let t = iit#get_text ~stop:npi in
- flash_info (t^"\n"^txt);
- t = txt)
- with
- | true,true ->
- (flash_info "T,T";iit#backward_search txt)
- | false,true -> flash_info "F,T";Some (iit,npi)
- | _,false ->
- (iit#backward_search txt)
-
- with
- | None ->
- if !ready_to_wrap_search then begin
- ready_to_wrap_search := false;
- flash_info "Search wrapped";
- v#buffer#place_cursor
- ~where:(if !search_forward then v#buffer#start_iter else
- v#buffer#end_iter);
- search_f ()
- end else begin
- if !search_forward then flash_info "Search at end"
- else flash_info "Search at start";
- ready_to_wrap_search := true
- end
- | Some (start,stop) ->
- prerr_endline "search: before moving marks";
- prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
- prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
-
- v#buffer#move_mark `SEL_BOUND ~where:start;
- v#buffer#move_mark `INSERT ~where:stop;
- prerr_endline "search: after moving marks";
- prerr_endline ("SELBOUND="^(string_of_int (v#buffer#get_iter_at_mark `SEL_BOUND)#offset));
- prerr_endline ("INSERT="^(string_of_int (v#buffer#get_iter_at_mark `INSERT)#offset));
- v#scroll_to_mark `SEL_BOUND
- )
- in
- ignore (search_input#entry#event#connect#key_release
- ~callback:
- (fun ev ->
- if GdkEvent.Key.keyval ev = GdkKeysyms._Escape then begin
- let v = session_notebook#current_term.script in
- (match !start_of_search with
- | None ->
- prerr_endline "search_key_rel: Placing sel_bound";
- v#buffer#move_mark
- `SEL_BOUND
- ~where:(v#buffer#get_iter_at_mark `INSERT)
- | Some mk -> let it = v#buffer#get_iter_at_mark
- (`MARK mk) in
- prerr_endline "search_key_rel: Placing cursor";
- v#buffer#place_cursor ~where:it;
- start_of_search := None
- );
- search_input#entry#set_text "";
- v#coerce#misc#grab_focus ();
- end;
- false
- ));
- ignore (search_input#entry#connect#changed ~callback:search_f);
- push_info "Ready";
+
+ (* Vertical Separator between Scripts and Goals *)
+ let () = vbox#pack ~expand:true notebook#coerce in
+ let () = refresh_notebook_pos () in
+ let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
+ let () = lower_hbox#pack ~expand:true status#coerce in
+ let () = push_info ("Ready"^ if current.nanoPG then ", [μPG]" else "") in
+
(* Location display *)
let l = GMisc.label
~text:"Line: 1 Char: 1"
- ~packing:lower_hbox#pack () in
- l#coerce#misc#set_name "location";
- set_location := l#set_text;
+ ~packing:lower_hbox#pack ()
+ in
+ let () = l#coerce#misc#set_name "location" in
+ let () = set_location := l#set_text in
+
(* Progress Bar *)
- lower_hbox#pack pbar#coerce;
- pbar#set_text "CoqIde started";
+ let pbar = GRange.progress_bar ~pulse_step:0.1 () in
+ let () = lower_hbox#pack pbar#coerce in
+ let ready () = pbar#set_fraction 0.0; pbar#set_text "Coq is ready" in
+ let pulse sn =
+ if Coq.is_computing sn.coqtop then
+ (pbar#set_text "Coq is computing"; pbar#pulse ())
+ else ready () in
+ let callback () = on_current_term pulse; true in
+ let _ = Glib.Timeout.add ~ms:300 ~callback in
+
+ (* Pending proofs. It should be with a GtkSpinner... not bound *)
+ let slaveinfo = GMisc.label ~xalign:0.5 ~width:50 () in
+ let () = lower_hbox#pack slaveinfo#coerce in
+ let () = slaveinfo#misc#set_has_tooltip true in
+ let () = slaveinfo#misc#set_tooltip_markup
+ "Proofs to be checked / Errors" in
+ let update sn =
+ let processed, to_process, jobs = sn.coqops#get_slaves_status in
+ let missing = to_process - processed in
+ let n_err = sn.coqops#get_n_errors in
+ if n_err > 0 then
+ slaveinfo#set_text (Printf.sprintf
+ "%d / <span foreground=\"#FF0000\">%d</span>" missing n_err)
+ else
+ slaveinfo#set_text (Printf.sprintf "%d / %d" missing n_err);
+ slaveinfo#set_use_markup true;
+ sn.errpage#update sn.coqops#get_errors;
+ sn.jobpage#update (Util.pi3 sn.coqops#get_slaves_status) in
+ let callback () = on_current_term update; true in
+ let _ = Glib.Timeout.add ~ms:300 ~callback in
(* Initializing hooks *)
-
- refresh_toolbar_hook :=
- (fun () -> if !current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ());
- refresh_font_hook :=
- (fun () ->
- let fd = !current.text_font in
- let iter_page p =
- p.script#misc#modify_font fd;
- p.proof_view#misc#modify_font fd;
- p.message_view#misc#modify_font fd;
- p.command#refresh_font ()
- in
- List.iter iter_page session_notebook#pages;
- );
- refresh_background_color_hook :=
- (fun () ->
- let clr = Tags.color_of_string !current.background_color in
- let iter_page p =
- p.script#misc#modify_base [`NORMAL, `COLOR clr];
- p.proof_view#misc#modify_base [`NORMAL, `COLOR clr];
- p.message_view#misc#modify_base [`NORMAL, `COLOR clr];
- p.command#refresh_color ()
- in
- List.iter iter_page session_notebook#pages;
- );
- resize_window_hook := (fun () ->
- w#resize
- ~width:!current.window_width
- ~height:!current.window_height);
- refresh_tabs_hook := update_notebook_pos;
-
- let about_full_string =
- "\nCoq is developed by the Coq Development Team\
- \n(INRIA - CNRS - LIX - LRI - PPS)\
- \nWeb site: " ^ Coq_config.wwwcoq ^
- "\nFeature wish or bug report: http://coq.inria.fr/bugs/\
- \n\
- \nCredits for CoqIDE, the Integrated Development Environment for Coq:\
- \n\
- \nMain author : Benjamin Monate\
- \nContributors : Jean-Christophe Filliâtre\
- \n Pierre Letouzey, Claude Marché\
- \n Bruno Barras, Pierre Corbineau\
- \n Julien Narboux, Hugo Herbelin, ... \
- \n\
- \nVersion information\
- \n-------------------\
- \n"
+ let refresh_toolbar () =
+ if prefs.show_toolbar
+ then toolbar#misc#show ()
+ else toolbar#misc#hide ()
in
- let display_log_file (b:GText.buffer) =
- if !debug then
- let file = match !logfile with None -> "stderr" | Some f -> f in
- b#insert ("Debug mode is on, log file is "^file)
+ let refresh_style () =
+ let style = style_manager#style_scheme prefs.source_style in
+ let iter_session v = v.script#source_buffer#set_style_scheme style in
+ List.iter iter_session notebook#pages
in
- let initial_about (b:GText.buffer) =
- let initial_string =
- "Welcome to CoqIDE, an Integrated Development Environment for Coq\n"
- in
- let coq_version = Coq.short_version () in
- display_log_file b;
- if Glib.Utf8.validate ("You are running " ^ coq_version) then
- b#insert ~iter:b#start_iter ("You are running " ^ coq_version);
- if Glib.Utf8.validate initial_string then
- b#insert ~iter:b#start_iter initial_string;
- (try
- let image = Filename.concat (List.find
- (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
- Minilib.xdg_data_dirs) "coq.png" in
- let startup_image = GdkPixbuf.from_file image in
- b#insert ~iter:b#start_iter "\n\n";
- b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image;
- b#insert ~iter:b#start_iter "\n\n\t\t "
- with _ -> ())
+ let refresh_language () =
+ let lang = lang_manager#language prefs.source_language in
+ let iter_session v = v.script#source_buffer#set_language lang in
+ List.iter iter_session notebook#pages
in
-
- let about (b:GText.buffer) =
- (try
- let image = Filename.concat (List.find
- (fun x -> Sys.file_exists (Filename.concat x "coq.png"))
- Minilib.xdg_data_dirs) "coq.png" in
- let startup_image = GdkPixbuf.from_file image in
- b#insert ~iter:b#start_iter "\n\n";
- b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image;
- b#insert ~iter:b#start_iter "\n\n\t\t "
- with _ -> ());
- if Glib.Utf8.validate about_full_string
- then b#insert about_full_string;
- let coq_version = Coq.version () in
- if Glib.Utf8.validate coq_version
- then b#insert coq_version;
- display_log_file b;
+ let resize_window () =
+ w#resize ~width:prefs.window_width ~height:prefs.window_height
in
- (* Remove default pango menu for textviews *)
- w#show ();
- ignore ((help_actions#get_action "About Coq")#connect#activate
- ~callback:(fun _ -> let prf_v = session_notebook#current_term.proof_view in
- prf_v#buffer#set_text ""; about prf_v#buffer));
- (*
-
- *)
-(* Begin Color configuration *)
-
- Tags.set_processing_color (Tags.color_of_string !current.processing_color);
- Tags.set_processed_color (Tags.color_of_string !current.processed_color);
-
-(* End of color configuration *)
- ignore(nb#connect#switch_page
- ~callback:
- (fun i ->
- prerr_endline ("switch_page: starts " ^ string_of_int i);
- List.iter (function f -> f i) !to_do_on_page_switch;
- prerr_endline "switch_page: success")
- );
- if List.length files >=1 then
- begin
- List.iter (fun f ->
- if Sys.file_exists f then do_load f else
- let f = if Filename.check_suffix f ".v" then f else f^".v" in
- load_file (fun s -> print_endline s; exit 1) f)
- files;
- session_notebook#goto_page 0;
- end
- else
- begin
- let session = create_session None in
- let index = session_notebook#append_term session in
- session_notebook#goto_page index;
- end;
- initial_about session_notebook#current_term.proof_view#buffer;
- !refresh_toolbar_hook ();
- session_notebook#current_term.script#misc#grab_focus ();;
+ refresh_toolbar ();
+ refresh_toolbar_hook := refresh_toolbar;
+ refresh_style_hook := refresh_style;
+ refresh_language_hook := refresh_language;
+ refresh_editor_hook := refresh_editor_prefs;
+ resize_window_hook := resize_window;
+ refresh_tabs_hook := refresh_notebook_pos;
+
+ (* Color configuration *)
+ Tags.set_processing_color (Tags.color_of_string prefs.processing_color);
+ Tags.set_processed_color (Tags.color_of_string prefs.processed_color);
+ Tags.Script.incomplete#set_property
+ (`BACKGROUND_STIPPLE
+ (Gdk.Bitmap.create_from_data ~width:2 ~height:2 "\x01\x02"));
+ Tags.Script.incomplete#set_property
+ (`BACKGROUND_GDK (Tags.get_processed_color ()));
+
+ (* Showtime ! *)
+ w#show ()
+
+
+(** {2 Coqide main function } *)
+
+let make_file_buffer f =
+ let f = if Filename.check_suffix f ".v" then f else f^".v" in
+ FileAux.load_file ~maycreate:true f
+
+let make_scratch_buffer () =
+ let session = create_session None in
+ let _ = notebook#append_term session in
+ !refresh_editor_hook ()
+
+let main files =
+ build_ui ();
+ reset_revert_timer ();
+ reset_autosave_timer ();
+ (match files with
+ | [] -> make_scratch_buffer ()
+ | _ -> List.iter make_file_buffer files);
+ notebook#goto_page 0;
+ MiscMenu.initial_about ();
+ on_current_term (fun t -> t.script#misc#grab_focus ());
+ Minilib.log "End of Coqide.main"
+
+
+(** {2 Geoproof } *)
-(* This function check every half of second if GeoProof has send
- something on his private clipboard *)
+(** This function check every tenth of second if GeoProof has send
+ something on his private clipboard *)
-let rec check_for_geoproof_input () =
+let check_for_geoproof_input () =
let cb_Dr = GData.clipboard (Gdk.Atom.intern "_GeoProof") in
- while true do
- Thread.delay 0.1;
- let s = cb_Dr#text in
- (match s with
- Some s ->
- if s <> "Ack" then
- session_notebook#current_term.script#buffer#insert (s^"\n");
- cb_Dr#set_text "Ack"
- | None -> ()
- );
- (* cb_Dr#clear does not work so i use : *)
- (* cb_Dr#set_text "Ack" *)
- done
+ 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
full name, with the last occurrence of "coqide" replaced by "coqtop".
This should correctly handle the ".opt", ".byte", ".exe" situations.
If the replacement fails, we default to "coqtop", hoping it's somewhere
- in the path. Note that the -coqtop option to coqide allows to override
+ in the path. Note that the -coqtop option to coqide overrides
this default coqtop path *)
let read_coqide_args argv =
let rec filter_coqtop coqtop project_files out = function
- | "-coqtop" :: prog :: args ->
+ |"-coqtop" :: prog :: args ->
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 ->
- filter_coqtop coqtop
- ((Minilib.canonical_path_name (Filename.dirname file),
- Project_file.read_project_file file) :: project_files) out args
- | "-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1
- | "-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1
- | "-debug"::args -> Ideutils.debug := true;
+ else (output_string stderr "Error: multiple -coqtop options"; exit 1)
+ |"-f" :: file :: args ->
+ 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
+ |"-f" :: [] ->
+ output_string stderr "Error: missing project file name"; exit 1
+ |"-coqtop" :: [] ->
+ output_string stderr "Error: missing argument after -coqtop"; exit 1
+ |"-debug"::args ->
+ Minilib.debug := true;
+ Flags.debug := true;
+ Backtrace.record_backtrace true;
filter_coqtop coqtop project_files ("-debug"::out) args
- | arg::args -> filter_coqtop coqtop project_files (arg::out) args
- | [] -> (coqtop,List.rev project_files,List.rev out)
+ |"-coqtop-flags" :: flags :: args->
+ Flags.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)
in
let coqtop,project_files,argv = filter_coqtop None [] [] argv in
- Ideutils.custom_coqtop := coqtop;
- custom_project_files := project_files;
+ Ideutils.custom_coqtop := coqtop;
+ custom_project_files := project_files;
argv
+
+
+(** {2 Signal handling } *)
+
+(** The Ctrl-C (sigint) is handled as a interactive quit.
+ For most of the other catchable signals we launch
+ an emergency save of opened files and then exit. *)
+
+let signals_to_crash =
+ [Sys.sigabrt; Sys.sigalrm; Sys.sigfpe; Sys.sighup;
+ Sys.sigill; Sys.sigpipe; Sys.sigquit; Sys.sigusr1; Sys.sigusr2]
+
+let set_signal_handlers () =
+ try
+ Sys.set_signal Sys.sigint (Sys.Signal_handle File.quit);
+ List.iter
+ (fun i -> Sys.set_signal i (Sys.Signal_handle FileAux.crash_save))
+ signals_to_crash
+ with _ -> Minilib.log "Signal ignored (normal if Win32)"
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 04:09:39 +0000