diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /ide | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'ide')
-rw-r--r-- | ide/command_windows.ml | 24 | ||||
-rw-r--r-- | ide/command_windows.mli | 2 | ||||
-rw-r--r-- | ide/coq.ml | 120 | ||||
-rw-r--r-- | ide/coq.mli | 14 | ||||
-rw-r--r-- | ide/coq_commands.ml | 1 | ||||
-rw-r--r-- | ide/coq_lex.mll | 28 | ||||
-rw-r--r-- | ide/coqide-gtk2rc | 10 | ||||
-rw-r--r-- | ide/coqide.ml | 231 | ||||
-rw-r--r-- | ide/coqide.mli | 3 | ||||
-rw-r--r-- | ide/coqide_main.ml4 | 24 | ||||
-rw-r--r-- | ide/coqide_ui.ml | 28 | ||||
-rw-r--r-- | ide/ideproof.ml | 16 | ||||
-rw-r--r-- | ide/ideutils.ml | 99 | ||||
-rw-r--r-- | ide/ideutils.mli | 13 | ||||
-rw-r--r-- | ide/minilib.ml | 47 | ||||
-rw-r--r-- | ide/preferences.ml | 210 | ||||
-rw-r--r-- | ide/preferences.mli | 21 | ||||
-rw-r--r-- | ide/tags.ml | 33 | ||||
-rw-r--r-- | ide/tags.mli | 50 | ||||
-rw-r--r-- | ide/utils/configwin.ml | 4 | ||||
-rw-r--r-- | ide/utils/configwin_ihm.ml | 6 |
21 files changed, 651 insertions, 333 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 939238d3..a34e5ebe 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -13,6 +13,7 @@ class command_window coqtop current = ~position:`CENTER ~title:"CoqIde queries" ~show:false () in *) + let views = ref [] in let frame = GBin.frame ~label:"Command Pane" ~shadow_type:`IN () in let _ = frame#misc#hide () in let _ = GtkData.AccelGroup.create () in @@ -49,12 +50,17 @@ class command_window coqtop current = () in + let remove_cb () = + let index = notebook#current_page in + let () = notebook#remove_page index in + views := Minilib.list_filter_i (fun i x -> i <> index) !views + in let _ = toolbar#insert_button ~tooltip:"Delete Page" ~text:"Delete Page" ~icon:(Ideutils.stock_to_widget `DELETE) - ~callback:(fun () -> notebook#remove_page notebook#current_page) + ~callback:remove_cb () in object(self) @@ -63,14 +69,14 @@ object(self) val new_page_menu = new_page_menu val notebook = notebook + method frame = frame method new_command ?command ?term () = - let appendp x = ignore (notebook#append_page x) in let frame = GBin.frame ~shadow_type:`ETCHED_OUT - ~packing:appendp () in + let _ = notebook#append_page frame#coerce in notebook#goto_page (notebook#page_num frame#coerce); let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in @@ -91,7 +97,10 @@ object(self) ~packing:(vbox#pack ~fill:true ~expand:true) () in let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in let result = GText.view ~packing:r_bin#add () in + let () = views := !views @ [result] in result#misc#modify_font !current.Preferences.text_font; + let clr = Tags.color_of_string !current.Preferences.background_color in + result#misc#modify_base [`NORMAL, `COLOR clr]; result#misc#set_can_focus true; (* false causes problems for selection *) result#set_editable false; let callback () = @@ -134,6 +143,15 @@ object(self) ignore (combo#entry#connect#activate ~callback); self#frame#misc#show () + method refresh_font () = + let iter view = view#misc#modify_font !current.Preferences.text_font in + List.iter iter !views + + method refresh_color () = + let clr = Tags.color_of_string !current.Preferences.background_color in + let iter view = view#misc#modify_base [`NORMAL, `COLOR clr] in + List.iter iter !views + initializer ignore (new_page_menu#connect#clicked ~callback:self#new_command); (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*) diff --git a/ide/command_windows.mli b/ide/command_windows.mli index 8c7319aa..c34b6cf6 100644 --- a/ide/command_windows.mli +++ b/ide/command_windows.mli @@ -11,4 +11,6 @@ class command_window : object method new_command : ?command:string -> ?term:string -> unit -> unit method frame : GBin.frame + method refresh_font : unit -> unit + method refresh_color : unit -> unit end @@ -54,36 +54,106 @@ let rec read_all_lines in_chan = arg::(read_all_lines in_chan) with End_of_file -> [] -let filter_coq_opts args = +let fatal_error_popup msg = + let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok + ~message_type:`ERROR ~message:msg () + in ignore (popup#run ()); exit 1 + +let final_info_popup small msg = + if small then + let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok + ~message_type:`INFO ~message:msg () + in + let _ = popup#run () in + exit 0 + else + let popup = GWindow.dialog () in + let button = GButton.button ~label:"ok" ~packing:popup#action_area#add () + in + let scroll = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC + ~packing:popup#vbox#add ~height:500 () + in + let _ = GMisc.label ~text:msg ~packing:scroll#add_with_viewport () in + let _ = popup#connect#destroy ~callback:(fun _ -> exit 0) in + let _ = button#connect#clicked ~callback:(fun _ -> exit 0) in + let _ = popup#run () in + exit 0 + +let connection_error cmd lines exn = + fatal_error_popup + ("Connection with coqtop failed!\n"^ + "Command was: "^cmd^"\n"^ + "Answer was: "^(String.concat "\n " lines)^"\n"^ + "Exception was: "^Printexc.to_string exn) + +let display_coqtop_answer cmd lines = + final_info_popup (List.length lines < 30) + ("Coqtop exited\n"^ + "Command was: "^cmd^"\n"^ + "Answer was: "^(String.concat "\n " lines)) + +let check_remaining_opt arg = + if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg) + +let rec filter_coq_opts args = let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote !Minilib.coqtop_path ^" -nois -filteropts " ^ argstr in - let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in - let filtered_args = read_all_lines oc in - let message = read_all_lines ec in - match Unix.close_process_full (oc,ic,ec) with - | Unix.WEXITED 0 -> true,filtered_args - | Unix.WEXITED 2 -> false,filtered_args - | _ -> false,message - -exception Coqtop_output of string list + let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in + let cmd = requote cmd in + let filtered_args = ref [] in + let errlines = ref [] in + try + let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in + filtered_args := read_all_lines oc; + errlines := read_all_lines ec; + match Unix.close_process_full (oc,ic,ec) with + | Unix.WEXITED 0 -> + List.iter check_remaining_opt !filtered_args; !filtered_args + | Unix.WEXITED 127 -> asks_for_coqtop args + | _ -> display_coqtop_answer cmd (!filtered_args @ !errlines) + with Sys_error _ -> asks_for_coqtop args + | e -> connection_error cmd (!filtered_args @ !errlines) e + +and asks_for_coqtop args = + let pb_mes = GWindow.message_dialog + ~message:"Failed to load coqtop. Reset the preference to default ?" + ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in + match pb_mes#run () with + | `YES -> + let () = !Preferences.current.Preferences.cmd_coqtop <- None in + let () = custom_coqtop := None in + let () = pb_mes#destroy () in + filter_coq_opts args + | `DELETE_EVENT | `NO -> + let () = pb_mes#destroy () in + let cmd_sel = GWindow.file_selection + ~title:"Coqtop to execute (edit your preference then)" + ~filename:(coqtop_path ()) ~urgency_hint:true () in + match cmd_sel#run () with + | `OK -> + let () = custom_coqtop := (Some cmd_sel#filename) in + let () = cmd_sel#destroy () in + filter_coq_opts args + | `CANCEL | `DELETE_EVENT | `HELP -> exit 0 + +exception WrongExitStatus of string + +let print_status = function + | Unix.WEXITED n -> "WEXITED "^string_of_int n + | Unix.WSIGNALED n -> "WSIGNALED "^string_of_int n + | Unix.WSTOPPED n -> "WSTOPPED "^string_of_int n let check_connection args = + let lines = ref [] in + let argstr = String.concat " " (List.map Filename.quote args) in + let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in + let cmd = requote cmd in try - let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote !Minilib.coqtop_path ^ " -batch " ^ argstr in let ic = Unix.open_process_in cmd in - let lines = read_all_lines ic in + lines := read_all_lines ic; match Unix.close_process_in ic with - | Unix.WEXITED 0 -> prerr_endline "coqtop seems ok" - | _ -> raise (Coqtop_output lines) - with - | End_of_file -> - Minilib.safe_prerr_endline "Cannot start connection with coqtop"; - exit 1 - | Coqtop_output lines -> - Minilib.safe_prerr_endline "Connection with coqtop failed:"; - List.iter Minilib.safe_prerr_endline lines; - exit 1 + | Unix.WEXITED 0 -> () (* coqtop seems ok *) + | st -> raise (WrongExitStatus (print_status st)) + with e -> connection_error cmd !lines e (** * The structure describing a coqtop sub-process *) @@ -139,7 +209,7 @@ let open_process_pid prog args = let spawn_coqtop sup_args = Mutex.lock toplvl_ctr_mtx; try - let prog = !Minilib.coqtop_path in + let prog = coqtop_path () in let args = Array.of_list (prog :: "-ideslave" :: sup_args) in let (pid,ic,oc) = open_process_pid prog args in incr toplvl_ctr; diff --git a/ide/coq.mli b/ide/coq.mli index 9d64da6c..7f61521e 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -13,11 +13,15 @@ val short_version : unit -> string val version : unit -> string -(** * Initial checks by launching test coqtop processes *) - -val filter_coq_opts : string list -> bool * string list - -(** A mock coqtop launch, checking in particular that initial.coq is found *) +(** * Launch a test coqtop processes, ask for a correct coqtop if it fails. + @return the list of arguments that coqtop did not understand + (the files probably ..). This command may terminate coqide in + case of trouble. *) +val filter_coq_opts : string list -> string list + +(** Launch a coqtop with the user args in order to be sure that it works, + checking in particular that initial.coq is found. This command + may terminate coqide in case of trouble *) val check_connection : string list -> unit (** * The structure describing a coqtop sub-process *) diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index b9e14145..256426d2 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -127,7 +127,6 @@ let commands = [ "Show Script"; "Show Tree";*) "Structure"; - (* "Suspend"; *) "Syntactic Definition"; "Syntax";]; [ diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll index f0f1afb7..c9a9a826 100644 --- a/ide/coq_lex.mll +++ b/ide/coq_lex.mll @@ -24,7 +24,7 @@ let one_word_commands = [ "Add" ; "Check"; "Eval"; "Extraction" ; "Load" ; "Undo"; "Goal"; - "Proof" ; "Print";"Save" ; + "Proof" ; "Print";"Save" ; "Restart"; "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ] in let one_word_declarations = @@ -37,7 +37,8 @@ (* Inductive *) "Inductive" ; "CoInductive" ; "Record" ; "Structure" ; (* Other *) - "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class" ] + "Ltac" ; "Instance"; "Include"; "Context"; "Class" ; + "Arguments" ] in let proof_declarations = [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ; @@ -85,33 +86,28 @@ let multiword_declaration = | "Existing" space+ "Instance" "s"? | "Canonical" space+ "Structure" -let locality = ("Local" space+)? +let locality = (space+ "Local")? let multiword_command = - "Set" (space+ ident)* -| "Unset" (space+ ident)* -| "Open" space+ locality "Scope" -| "Close" space+ locality "Scope" -| "Bind" space+ "Scope" -| "Arguments" space+ "Scope" -| "Reserved" space+ "Notation" space+ locality -| "Delimit" space+ "Scope" + ("Uns" | "S")" et" (space+ ident)* +| (("Open" | "Close") locality | "Bind" | " Delimit" ) + space+ "Scope" +| (("Reserved" space+)? "Notation" | "Infix") locality space+ | "Next" space+ "Obligation" | "Solve" space+ "Obligations" | "Require" space+ ("Import"|"Export")? -| "Infix" space+ locality -| "Notation" space+ locality -| "Hint" space+ locality ident +| "Hint" locality space+ ident | "Reset" (space+ "Initial")? | "Tactic" space+ "Notation" -| "Implicit" space+ "Arguments" -| "Implicit" space+ ("Type"|"Types") +| "Implicit" space+ "Type" "s"? | "Combined" space+ "Scheme" | "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"Toplevel"))| ("Library"|"Inline"|"NoInline"|"Blacklist")) | "Recursive" space+ "Extraction" (space+ "Library")? | ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist") | "Extract" space+ (("Inlined" space+) "Constant"| "Inductive") +| "Typeclasses" space+ ("eauto" | "Transparent" | "Opaque") +| ("Generalizable" space+) ("All" | "No")? "Variable" "s"? (* At least still missing: "Inline" + decl, variants of "Identity Coercion", variants of Print, Add, ... *) diff --git a/ide/coqide-gtk2rc b/ide/coqide-gtk2rc index 621d4e84..9da99551 100644 --- a/ide/coqide-gtk2rc +++ b/ide/coqide-gtk2rc @@ -23,16 +23,6 @@ binding "text" { class "GtkTextView" binding "text" -style "views" { -base[NORMAL] = "CornSilk" -# bg_pixmap[NORMAL] = "background.jpg" -} -class "GtkTextView" style "views" - -widget "*.*.*.*.*.ScriptWindow" style "views" -widget "*.*.*.*.GoalWindow" style "views" -widget "*.*.*.*.MessageWindow" style "views" - gtk-font-name = "Sans 12" style "location" { diff --git a/ide/coqide.ml b/ide/coqide.ml index 009a1989..61280fd9 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -27,7 +27,6 @@ let safety_tag = function class type analyzed_views= object val mutable act_id : GtkSignal.id option - val mutable deact_id : GtkSignal.id option val input_buffer : GText.buffer val input_view : Undo.undoable_view val last_array : string array @@ -65,7 +64,6 @@ object method backtrack_to : GText.iter -> unit method backtrack_to_no_lock : GText.iter -> unit method clear_message : unit - method disconnected_keypress_handler : GdkEvent.Key.t -> bool method find_phrase_starting_at : GText.iter -> (GText.iter * GText.iter) option method get_insert : GText.iter @@ -84,6 +82,7 @@ object 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 @@ -889,11 +888,32 @@ object(self) 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 + in + try + match Coq.interp !mycoqtop ~raw:true ~verbose:false 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 - if is_sentence_end stop#backward_char then Some (start,stop) + (* 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 Not_found -> None @@ -1217,22 +1237,6 @@ object(self) let state = GdkEvent.Key.state k in begin match state with - | l when List.mem `MOD1 l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._Return=k - then ignore( - if (input_buffer#insert_interactive "\n") then - begin - let i= self#get_insert#backward_word_start in - prerr_endline "active_kp_hf: Placing cursor"; - self#process_until_iter_or_error i - end); - true - | l when List.mem `CONTROL l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._Break=k - then break (); - false | l -> if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin prerr_endline "active_kp_handler for Tab"; @@ -1241,18 +1245,6 @@ object(self) end else false end - - method disconnected_keypress_handler k = - match GdkEvent.Key.state k with - | l when List.mem `CONTROL l -> - let k = GdkEvent.Key.keyval k in - if GdkKeysyms._c=k - then break (); - false - | l -> false - - - val mutable deact_id = None val mutable act_id = None method activate () = if not is_active then begin @@ -1523,9 +1515,15 @@ let create_session file = 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; @@ -1798,12 +1796,6 @@ let forbid_quit_to_save () = else false) let main files = - (* Statup preferences *) - begin - try load_pref () - with e -> - flash_info ("Could not load preferences ("^Printexc.to_string e^")."); - end; (* Main window *) let w = GWindow.window @@ -1823,9 +1815,9 @@ let main files = let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in let new_f _ = - match select_file_for_save ~title:"Create file" () with - | None -> () - | Some f -> do_load 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 @@ -2181,6 +2173,7 @@ let main files = 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 -> @@ -2327,13 +2320,13 @@ let main files = in let file_actions = GAction.action_group ~name:"File" () in - let export_actions = GAction.action_group ~name:"Export" () 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 display_actions = GAction.action_group ~name:"Display" () 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 @@ -2362,10 +2355,18 @@ let main files = ~accel:(!current.modifier_for_tactics^sc) ~callback:(do_if_active (fun a -> a#insert_command ("progress "^s^".\n") (s^".\n"))) in - let query_shortcut s accel = GAction.add_action s ~label:("_"^s) ?accel - ~callback:(fun _ -> let term = get_current_word () in - session_notebook#current_term.command#new_command ~command:s ~term ()) - in let add_complex_template (name, label, text, offset, len, key) = + 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 @@ -2450,6 +2451,31 @@ let main files = end; reset_revert_timer ()) ~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:("<SHIFT>Left") ~stock:`GO_BACK + ~callback:(fun _ -> session_notebook#previous_page ()); + GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<SHIFT>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 @@ -2532,15 +2558,6 @@ let main files = query_shortcut "Locate" None; query_shortcut "Whelp Locate" None; ]; - GAction.add_action "Display" ~label:"_Display" display_actions; - 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) ()) display_actions) - print_items; GAction.add_actions compile_actions [ GAction.add_action "Compile" ~label:"_Compile"; GAction.add_action "Compile buffer" ~label:"_Compile buffer" ~callback:compile_f; @@ -2551,16 +2568,6 @@ let main files = ]; GAction.add_actions windows_actions [ GAction.add_action "Windows" ~label:"_Windows"; - GAction.add_toggle_action "Show/Hide Query Pane" ~label:"Show/Hide _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"; - GAction.add_toggle_action "Show/Hide Toolbar" ~label:"Show/Hide _Toolbar" - ~active:(!current.show_toolbar) ~callback: - (fun _ -> !current.show_toolbar <- not !current.show_toolbar; - !show_toolbar !current.show_toolbar); GAction.add_action "Detach View" ~label:"Detach _View" ~callback:(fun _ -> do_if_not_computing "detach view" (function {script=v;analyzed_view=av} -> @@ -2608,11 +2615,11 @@ let main files = 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 display_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; @@ -2625,9 +2632,6 @@ let main files = let toolbar = new GObj.widget tbar in vbox#pack toolbar; - show_toolbar := - (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ()); - ignore (w#event#connect#delete ~callback:(fun _ -> quit_f (); true)); (* The vertical Separator between Scripts and Goals *) @@ -2790,17 +2794,39 @@ let main files = (* Progress Bar *) lower_hbox#pack pbar#coerce; pbar#set_text "CoqIde started"; - (* XXX *) - change_font := - (fun fd -> - List.iter - (fun {script=view; proof_view=prf_v; message_view=msg_v} -> - view#misc#modify_font fd; - prf_v#misc#modify_font fd; - msg_v#misc#modify_font fd - ) - session_notebook#pages; + + (* 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)\ @@ -2865,10 +2891,12 @@ let main files = (* *) - resize_window := (fun () -> - w#resize - ~width:!current.window_width - ~height:!current.window_height); +(* 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 -> @@ -2892,7 +2920,7 @@ let main files = session_notebook#goto_page index; end; initial_about session_notebook#current_term.proof_view#buffer; - !show_toolbar !current.show_toolbar; + !refresh_toolbar_hook (); session_notebook#current_term.script#misc#grab_focus ();; (* This function check every half of second if GeoProof has send @@ -2921,43 +2949,24 @@ let rec check_for_geoproof_input () = in the path. Note that the -coqtop option to coqide allows to override this default coqtop path *) -let default_coqtop_path () = - let prog = Sys.executable_name in - try - let pos = String.length prog - 6 in - let i = Str.search_backward (Str.regexp_string "coqide") prog pos in - String.blit "coqtop" 0 prog i 6; - prog - with _ -> "coqtop" - let read_coqide_args argv = let rec filter_coqtop coqtop project_files out = function | "-coqtop" :: prog :: args -> - if coqtop = "" then filter_coqtop prog project_files out args + if coqtop = None then filter_coqtop (Some prog) project_files out args else - (output_string stderr "Error: multiple -coqtop options"; exit 1) + (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; + filter_coqtop coqtop project_files ("-debug"::out) args | arg::args -> filter_coqtop coqtop project_files (arg::out) args - | [] -> ((if coqtop = "" then default_coqtop_path () else coqtop), - List.rev project_files,List.rev out) + | [] -> (coqtop,List.rev project_files,List.rev out) in - let coqtop,project_files,argv = filter_coqtop "" [] [] argv in - Minilib.coqtop_path := coqtop; + let coqtop,project_files,argv = filter_coqtop None [] [] argv in + Ideutils.custom_coqtop := coqtop; custom_project_files := project_files; argv - -let process_argv argv = - try - let continue,filtered = Coq.filter_coq_opts (List.tl argv) in - if not continue then - (List.iter Minilib.safe_prerr_endline filtered; exit 0); - let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in - if opts <> [] then - (Minilib.safe_prerr_endline ("Illegal option: "^List.hd opts); exit 1); - filtered - with _ -> - (Minilib.safe_prerr_endline "coqtop choked on one of your option"; exit 1) diff --git a/ide/coqide.mli b/ide/coqide.mli index 38b0fab0..57158a6a 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -16,9 +16,6 @@ val sup_args : string list ref Minilib.coqtop_path accordingly *) val read_coqide_args : string list -> string list -(** Ask coqtop the remaining options it doesn't recognize *) -val process_argv : string list -> string list - (** Prepare the widgets, load the given files in tabs *) val main : string list -> unit diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 3fec0631..6f4b8b13 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -65,21 +65,21 @@ let () = END let () = - let argl = Array.to_list Sys.argv in - let argl = Coqide.read_coqide_args argl in - let files = Coqide.process_argv argl in - let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in - Coq.check_connection args; - Coqide.sup_args := args; Coqide.ignore_break (); + ignore (GtkMain.Main.init ()); + initmac () ; (try let gtkrcdir = List.find (fun x -> Sys.file_exists (Filename.concat x "coqide-gtk2rc")) Minilib.xdg_config_dirs in GtkMain.Rc.add_default_file (Filename.concat gtkrcdir "coqide-gtk2rc"); with Not_found -> ()); - ignore (GtkMain.Main.init ()); - initmac () ; + (* Statup preferences *) + begin + try Preferences.load_pref () + with e -> + Ideutils.flash_info ("Could not load preferences ("^Printexc.to_string e^")."); + end; (* GtkData.AccelGroup.set_default_mod_mask (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);*) ignore ( @@ -89,7 +89,13 @@ let () = if level land Glib.Message.log_level `WARNING <> 0 then Printf.eprintf "Warning: %s\n" msg else failwith ("Coqide internal error: " ^ msg))); - Coqide.main files; + let argl = Array.to_list Sys.argv in + let argl = Coqide.read_coqide_args argl in + let files = Coq.filter_coq_opts (List.tl argl) in + let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in + Coq.check_connection args; + Coqide.sup_args := args; + Coqide.main files; if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ()); macready (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar") (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs") (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help/Abt"); diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml index 0d7c67ac..eaf1e934 100644 --- a/ide/coqide_ui.ml +++ b/ide/coqide_ui.ml @@ -56,6 +56,22 @@ let init () = <separator /> <menuitem name='Prefs' action='Preferences' /> </menu> + <menu name='View' action='View'> + <menuitem action='Previous tab' /> + <menuitem action='Next tab' /> + <separator/> + <menuitem action='Show Toolbar' /> + <menuitem action='Show Query Pane' /> + <separator/> + <menuitem action='Display implicit arguments' /> + <menuitem action='Display coercions' /> + <menuitem action='Display raw matching expressions' /> + <menuitem action='Display notations' /> + <menuitem action='Display all basic low-level contents' /> + <menuitem action='Display existential variable instances' /> + <menuitem action='Display universe levels' /> + <menuitem action='Display all low-level contents' /> + </menu> <menu action='Navigation'> <menuitem action='Forward' /> <menuitem action='Backward' /> @@ -100,16 +116,6 @@ let init () = <menuitem action='Locate' /> <menuitem action='Whelp Locate' /> </menu> - <menu action='Display'> - <menuitem action='Display implicit arguments' /> - <menuitem action='Display coercions' /> - <menuitem action='Display raw matching expressions' /> - <menuitem action='Display notations' /> - <menuitem action='Display all basic low-level contents' /> - <menuitem action='Display existential variable instances' /> - <menuitem action='Display universe levels' /> - <menuitem action='Display all low-level contents' /> - </menu> <menu action='Compile'> <menuitem action='Compile buffer' /> <menuitem action='Make' /> @@ -117,8 +123,6 @@ let init () = <menuitem action='Make makefile' /> </menu> <menu action='Windows'> - <menuitem action='Show/Hide Query Pane' /> - <menuitem action='Show/Hide Toolbar' /> <menuitem action='Detach View' /> </menu> <menu name='Help' action='Help'> diff --git a/ide/ideproof.ml b/ide/ideproof.ml index 3c3324cb..b79d6469 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -53,7 +53,7 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "" else "s") in let goal_str index total = Printf.sprintf - "\n______________________________________(%d/%d)\n" index total + "______________________________________(%d/%d)\n" index total in (* Insert current goal and its hypotheses *) let hyps_hints, goal_hints = match hints with @@ -76,14 +76,15 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with let () = proof#buffer#insert head_str in let () = insert_hyp hyps_hints hyps in let () = - let tags = if goal_hints <> [] then + let tags = Tags.Proof.goal :: if goal_hints <> [] then let tag = proof#buffer#create_tag [] in let () = hook_tag_cb tag goal_hints sel_cb on_hover in [tag] else [] in proof#buffer#insert (goal_str 1 goals_cnt); - proof#buffer#insert ~tags (cur_goal ^ "\n") + proof#buffer#insert ~tags cur_goal; + proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) let fold_goal i _ { Interface.goal_ccl = g } = @@ -91,10 +92,11 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with proof#buffer#insert (g ^ "\n") in let () = Minilib.list_fold_left_i fold_goal 2 () rem_goals in - ignore(proof#buffer#place_cursor - ~where:((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2))); - ignore(proof#scroll_to_mark `INSERT) + ignore(proof#buffer#place_cursor + ~where:(proof#buffer#end_iter#backward_to_tag_toggle + (Some Tags.Proof.goal))); + ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT) let mode_cesar (proof:GText.view) = function | [] -> assert false @@ -123,7 +125,7 @@ let display mode (view:GText.view) goals hints evars = in List.iter iter evs | _ -> - view#buffer#insert "Proof Completed." + view#buffer#insert "No more subgoals." end | Some { Interface.fg_goals = []; Interface.bg_goals = bg } -> (* No foreground proofs, but still unfocused ones *) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index fd460c4e..a208ad0e 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -63,28 +63,25 @@ let print_id id = let do_convert s = Utf8_convert.f (if Glib.Utf8.validate s then begin - prerr_endline "Input is UTF-8";s - end else - let from_loc () = - let _,char_set = Glib.Convert.get_charset () in - flash_info - ("Converting from locale ("^char_set^")"); - Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s - in - let from_manual () = - flash_info - ("Converting from "^ !current.encoding_manual); - Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:!current.encoding_manual - in - if !current.encoding_use_utf8 || !current.encoding_use_locale then begin - try - from_loc () - with _ -> from_manual () - end else begin - try - from_manual () - with _ -> from_loc () - end) + prerr_endline "Input is UTF-8";s + end else + let from_loc () = + let _,char_set = Glib.Convert.get_charset () in + flash_info + ("Converting from locale ("^char_set^")"); + Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s + in + let from_manual enc = + flash_info + ("Converting from "^ enc); + Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:enc + in + match !current.encoding with + |Preferences.Eutf8 | Preferences.Elocale -> from_loc () + |Emanual enc -> + try + from_manual enc + with _ -> from_loc ()) let try_convert s = try @@ -96,18 +93,21 @@ Please choose a correct encoding in the preference panel.*)";; let try_export file_name s = try let s = - try if !current.encoding_use_utf8 then begin - (prerr_endline "UTF-8 is enforced" ;s) - end else if !current.encoding_use_locale then begin - let is_unicode,char_set = Glib.Convert.get_charset () in - if is_unicode then - (prerr_endline "Locale is UTF-8" ;s) - else - (prerr_endline ("Locale is "^char_set); - Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s) - end else - (prerr_endline ("Manual charset is "^ !current.encoding_manual); - Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:!current.encoding_manual s) + try match !current.encoding with + |Eutf8 -> begin + (prerr_endline "UTF-8 is enforced" ;s) + end + |Elocale -> begin + let is_unicode,char_set = Glib.Convert.get_charset () in + if is_unicode then + (prerr_endline "Locale is UTF-8" ;s) + else + (prerr_endline ("Locale is "^char_set); + Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s) + end + |Emanual enc -> + (prerr_endline ("Manual charset is "^ enc); + Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:enc s) with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s) in let oc = open_out file_name in @@ -252,14 +252,40 @@ let stock_to_widget ?(size=`DIALOG) s = in img#set_stock s; img#coerce +let custom_coqtop = ref None + +let coqtop_path () = + let file = match !custom_coqtop with + | Some s -> s + | None -> + match !current.cmd_coqtop with + | Some s -> s + | None -> + let prog = String.copy Sys.executable_name in + try + let pos = String.length prog - 6 in + let i = Str.search_backward (Str.regexp_string "coqide") prog pos in + String.blit "coqtop" 0 prog i 6; + prog + with Not_found -> "coqtop" + in file + let rec print_list print fmt = function | [] -> () | [x] -> print fmt x | x :: r -> print fmt x; print_list print fmt r +(* In win32, when a command-line is to be executed via cmd.exe + (i.e. Sys.command, Unix.open_process, ...), it cannot contain several + quoted "..." zones otherwise some quotes are lost. Solution: we re-quote + everything. Reference: http://ss64.com/nt/cmd.html *) + +let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd + (* TODO: allow to report output as soon as it comes (user-fiendlier for long commands like make...) *) let run_command f c = + let c = requote c in let result = Buffer.create 127 in let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in let buff = String.make 127 ' ' in @@ -279,11 +305,12 @@ let run_command f c = let browse f url = let com = Minilib.subst_command_placeholder !current.cmd_browse url in - let s = Sys.command com in + let _ = Unix.open_process_out com in () +(* This beautiful message will wait for twt ... if s = 127 then f ("Could not execute\n\""^com^ "\"\ncheck your preferences for setting a valid browser command\n") - +*) let doc_url () = if !current.doc_url = use_default_doc_url || !current.doc_url = "" then let addr = List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";"index.html"] in diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 1e29d323..c433d92a 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -52,6 +52,12 @@ val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit val run_command : (string -> unit) -> string -> Unix.process_status*string +val custom_coqtop : string option ref +(* @return command to call coqtop + - custom_coqtop if set + - from the prefs is set + - try to infer it else *) +val coqtop_path : unit -> string val status : GMisc.statusbar @@ -67,3 +73,10 @@ val pbar : GRange.progress_bar returns an absolute filename equivalent to given filename *) val absolute_filename : string -> string + +(* In win32, when a command-line is to be executed via cmd.exe + (i.e. Sys.command, Unix.open_process, ...), it cannot contain several + quoted "..." zones otherwise some quotes are lost. Solution: we re-quote + everything. Reference: http://ss64.com/nt/cmd.html *) + +val requote : string -> string diff --git a/ide/minilib.ml b/ide/minilib.ml index cec77f3b..4ccb1ccb 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -64,9 +64,10 @@ let string_map f s = let subst_command_placeholder s t = Str.global_replace (Str.regexp_string "%s") t s -let path_to_list p = - let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in - Str.split sep p +(* Split the content of a variable such as $PATH in a list of directories. + The separators are either ":" in unix or ";" in win32 *) + +let path_to_list = Str.split (Str.regexp "[:;]") (* On win32, the home directory is probably not in $HOME, but in some other environment variable *) @@ -76,28 +77,50 @@ let home = try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found -> try Sys.getenv "USERPROFILE" with Not_found -> Filename.current_dir_name +let opt2list = function None -> [] | Some x -> [x] + +let rec lconcat = function + | [] -> assert false + | [x] -> x + | x::l -> Filename.concat x (lconcat l) + let xdg_config_home = try Filename.concat (Sys.getenv "XDG_CONFIG_HOME") "coq" with Not_found -> - Filename.concat home "/.config/coq" + lconcat [home;".config";"coq"] + +let static_xdg_config_dirs = + if Sys.os_type = "Win32" then + let base = Filename.dirname (Filename.dirname Sys.executable_name) in + [Filename.concat base "config"] + else ["/etc/xdg/coq"] let xdg_config_dirs = - xdg_config_home :: (try - List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_CONFIG_DIRS")) - with Not_found -> "/etc/xdg/coq"::(match Coq_config.configdir with |None -> [] |Some d -> [d])) + xdg_config_home :: + try + List.map (fun dir -> Filename.concat dir "coq") + (path_to_list (Sys.getenv "XDG_CONFIG_DIRS")) + with Not_found -> static_xdg_config_dirs @ opt2list Coq_config.configdir let xdg_data_home = try Filename.concat (Sys.getenv "XDG_DATA_HOME") "coq" with Not_found -> - Filename.concat home "/.local/share/coq" + lconcat [home;".local";"share";"coq"] + +let static_xdg_data_dirs = + if Sys.os_type = "Win32" then + let base = Filename.dirname (Filename.dirname Sys.executable_name) in + [Filename.concat base "share"] + else ["/usr/local/share/coq";"/usr/share/coq"] let xdg_data_dirs = - xdg_data_home :: (try - List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS")) - with Not_found -> - "/usr/local/share/coq"::"/usr/share/coq"::(match Coq_config.datadir with |None -> [] |Some d -> [d])) + xdg_data_home :: + try + List.map (fun dir -> Filename.concat dir "coq") + (path_to_list (Sys.getenv "XDG_DATA_DIRS")) + with Not_found -> static_xdg_data_dirs @ opt2list Coq_config.datadir let coqtop_path = ref "" diff --git a/ide/preferences.ml b/ide/preferences.ml index 02673098..d320ddda 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -10,9 +10,22 @@ open Configwin open Printf let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc" - let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys" +let get_config_file name = + let find_config dir = Sys.file_exists (Filename.concat dir name) in + let config_dir = List.find find_config Minilib.xdg_config_dirs in + Filename.concat config_dir name + +(* Small hack to handle v8.3 to v8.4 change in configuration file *) +let loaded_pref_file = + try get_config_file "coqiderc" + with Not_found -> Filename.concat Minilib.home ".coqiderc" + +let loaded_accel_file = + try get_config_file "coqide.keys" + with Not_found -> Filename.concat Minilib.home ".coqide.keys" + let mod_to_str (m:Gdk.Tags.modifier) = match m with | `MOD1 -> "<Alt>" @@ -40,8 +53,32 @@ let project_behavior_of_string s = else if s = "appended to arguments" then Append_args else Ignore_args +type inputenc = Elocale | Eutf8 | Emanual of string + +let string_of_inputenc = function + |Elocale -> "LOCALE" + |Eutf8 -> "UTF-8" + |Emanual s -> s + +let inputenc_of_string s = + (if s = "UTF-8" then Eutf8 + else if s = "LOCALE" then Elocale + else Emanual s) + + +(** Hooks *) + +let refresh_font_hook = ref (fun () -> ()) +let refresh_background_color_hook = ref (fun () -> ()) +let refresh_toolbar_hook = ref (fun () -> ()) +let auto_complete_hook = ref (fun x -> ()) +let contextual_menus_on_goal_hook = ref (fun x -> ()) +let resize_window_hook = ref (fun () -> ()) +let refresh_tabs_hook = ref (fun () -> ()) + type pref = { + mutable cmd_coqtop : string option; mutable cmd_coqc : string; mutable cmd_make : string; mutable cmd_coqmakefile : string; @@ -57,9 +94,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; - mutable encoding_use_locale : bool; - mutable encoding_use_utf8 : bool; - mutable encoding_manual : string; + mutable encoding : inputenc; mutable automatic_tactics : string list; mutable cmd_print : string; @@ -89,15 +124,20 @@ type pref = *) mutable auto_complete : bool; mutable stop_before : bool; - mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; + + mutable background_color : string; + mutable processing_color : string; + mutable processed_color : string; + } let use_default_doc_url = "(automatic)" let (current:pref ref) = ref { + cmd_coqtop = None; cmd_coqc = "coqc"; cmd_make = "make"; cmd_coqmakefile = "coq_makefile -o makefile *.v"; @@ -114,9 +154,7 @@ let (current:pref ref) = read_project = Ignore_args; project_file_name = "_CoqProject"; - encoding_use_locale = true; - encoding_use_utf8 = false; - encoding_manual = "ISO_8859-1"; + encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale; automatic_tactics = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ]; @@ -150,32 +188,25 @@ let (current:pref ref) = *) auto_complete = false; stop_before = true; - lax_syntax = true; vertical_tabs = false; opposite_tabs = false; - } - - -let change_font = ref (fun f -> ()) -let show_toolbar = ref (fun x -> ()) + background_color = "cornsilk"; + processed_color = "light green"; + processing_color = "light blue"; -let auto_complete = ref (fun x -> ()) - -let contextual_menus_on_goal = ref (fun x -> ()) - -let resize_window = ref (fun () -> ()) + } let save_pref () = if not (Sys.file_exists Minilib.xdg_config_home) then Unix.mkdir Minilib.xdg_config_home 0o700; - (try GtkData.AccelMap.save accel_file - with _ -> ()); + let () = try GtkData.AccelMap.save accel_file with _ -> () in let p = !current in let add = Minilib.Stringmap.add in let (++) x f = f x in Minilib.Stringmap.empty ++ + add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++ add "cmd_coqc" [p.cmd_coqc] ++ add "cmd_make" [p.cmd_make] ++ add "cmd_coqmakefile" [p.cmd_coqmakefile] ++ @@ -190,9 +221,7 @@ let save_pref () = add "project_options" [string_of_project_behavior p.read_project] ++ add "project_file_name" [p.project_file_name] ++ - add "encoding_use_locale" [string_of_bool p.encoding_use_locale] ++ - add "encoding_use_utf8" [string_of_bool p.encoding_use_utf8] ++ - add "encoding_manual" [p.encoding_manual] ++ + add "encoding" [string_of_inputenc p.encoding] ++ add "automatic_tactics" p.automatic_tactics ++ add "cmd_print" [p.cmd_print] ++ @@ -217,19 +246,18 @@ let save_pref () = add "query_window_width" [string_of_int p.query_window_width] ++ add "auto_complete" [string_of_bool p.auto_complete] ++ add "stop_before" [string_of_bool p.stop_before] ++ - add "lax_syntax" [string_of_bool p.lax_syntax] ++ add "vertical_tabs" [string_of_bool p.vertical_tabs] ++ add "opposite_tabs" [string_of_bool p.opposite_tabs] ++ + add "background_color" [p.background_color] ++ + add "processing_color" [p.processing_color] ++ + add "processed_color" [p.processed_color] ++ Config_lexer.print_file pref_file let load_pref () = - let accel_dir = List.find - (fun x -> Sys.file_exists (Filename.concat x "coqide.keys")) - Minilib.xdg_config_dirs in - GtkData.AccelMap.load (Filename.concat accel_dir "coqide.keys"); + let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in let p = !current in - let m = Config_lexer.load_file pref_file in + let m = Config_lexer.load_file loaded_pref_file in let np = { p with cmd_coqc = p.cmd_coqc } in let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in let set_hd k f = set k (fun v -> f (List.hd v)) in @@ -239,6 +267,8 @@ let load_pref () = let set_command_with_pair_compat k f = set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit) in + let set_option k f = set k (fun v -> f (match v with |[] -> None |h::_ -> Some h)) in + set_option "cmd_coqtop" (fun v -> np.cmd_coqtop <- v); set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v); set_hd "cmd_make" (fun v -> np.cmd_make <- v); set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v); @@ -249,9 +279,7 @@ let load_pref () = set_bool "auto_save" (fun v -> np.auto_save <- v); set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v); set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2)); - set_bool "encoding_use_locale" (fun v -> np.encoding_use_locale <- v); - set_bool "encoding_use_utf8" (fun v -> np.encoding_use_utf8 <- v); - set_hd "encoding_manual" (fun v -> np.encoding_manual <- v); + set_hd "encoding_manual" (fun v -> np.encoding <- (inputenc_of_string v)); set_hd "project_options" (fun v -> np.read_project <- (project_behavior_of_string v)); set_hd "project_file_name" (fun v -> np.project_file_name <- v); @@ -290,15 +318,21 @@ let load_pref () = set_int "query_window_height" (fun v -> np.query_window_height <- v); set_bool "auto_complete" (fun v -> np.auto_complete <- v); set_bool "stop_before" (fun v -> np.stop_before <- v); - set_bool "lax_syntax" (fun v -> np.lax_syntax <- v); set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v); set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v); + set_hd "background_color" (fun v -> np.background_color <- v); + set_hd "processing_color" (fun v -> np.processing_color <- v); + set_hd "processed_color" (fun v -> np.processed_color <- v); current := np (* Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) let configure ?(apply=(fun () -> ())) () = + let cmd_coqtop = + string + ~f:(fun s -> !current.cmd_coqtop <- if s = "AUTO" then None else Some s) + " coqtop" (match !current.cmd_coqtop with |None -> "AUTO" | Some x -> x) in let cmd_coqc = string ~f:(fun s -> !current.cmd_coqc <- s) @@ -325,7 +359,7 @@ let configure ?(apply=(fun () -> ())) () = let w = GMisc.font_selection () in w#set_preview_text "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z)."; - box#pack w#coerce; + box#pack ~expand:true w#coerce; ignore (w#misc#connect#realize ~callback:(fun () -> w#set_font_name (Pango.Font.to_string !current.text_font))); @@ -338,9 +372,67 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - !change_font !current.text_font) + !refresh_font_hook ()) true in + + let config_color = + let box = GPack.vbox () in + let table = GPack.table + ~row_spacings:5 + ~col_spacings:5 + ~border_width:2 + ~packing:(box#pack ~expand:true) () + in + let background_label = GMisc.label + ~text:"Background color" + ~packing:(table#attach ~expand:`X ~left:0 ~top:0) () + in + let processed_label = GMisc.label + ~text:"Background color of processed text" + ~packing:(table#attach ~expand:`X ~left:0 ~top:1) () + in + let processing_label = GMisc.label + ~text:"Background color of text being processed" + ~packing:(table#attach ~expand:`X ~left:0 ~top:2) () + in + let () = background_label#set_xalign 0. in + let () = processed_label#set_xalign 0. in + let () = processing_label#set_xalign 0. in + let background_button = GButton.color_button + ~color:(Tags.color_of_string (!current.background_color)) + ~packing:(table#attach ~left:1 ~top:0) () + in + let processed_button = GButton.color_button + ~color:(Tags.get_processed_color ()) + ~packing:(table#attach ~left:1 ~top:1) () + in + let processing_button = GButton.color_button + ~color:(Tags.get_processing_color ()) + ~packing:(table#attach ~left:1 ~top:2) () + in + let reset_button = GButton.button + ~label:"Reset" + ~packing:box#pack () + in + let reset_cb () = + background_button#set_color (Tags.color_of_string "cornsilk"); + processing_button#set_color (Tags.color_of_string "light blue"); + processed_button#set_color (Tags.color_of_string "light green"); + in + let _ = reset_button#connect#clicked ~callback:reset_cb in + let label = "Color configuration" in + let callback () = + !current.background_color <- Tags.string_of_color background_button#color; + !current.processing_color <- Tags.string_of_color processing_button#color; + !current.processed_color <- Tags.string_of_color processed_button#color; + !refresh_background_color_hook (); + Tags.set_processing_color processing_button#color; + Tags.set_processed_color processed_button#color + in + custom ~label box callback true + in + (* let show_toolbar = bool @@ -369,7 +461,7 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> !current.auto_complete <- s; - !auto_complete s) + !auto_complete_hook s) "Auto Complete" !current.auto_complete in @@ -416,44 +508,28 @@ let configure ?(apply=(fun () -> ())) () = "Stop interpreting before the current point" !current.stop_before in - let lax_syntax = - bool - ~f:(fun s -> !current.lax_syntax <- s) - "Relax read-only constraint at end of command" !current.lax_syntax - in - let vertical_tabs = bool - ~f:(fun s -> !current.vertical_tabs <- s) + ~f:(fun s -> !current.vertical_tabs <- s; !refresh_tabs_hook ()) "Vertical tabs" !current.vertical_tabs in let opposite_tabs = bool - ~f:(fun s -> !current.opposite_tabs <- s) + ~f:(fun s -> !current.opposite_tabs <- s; !refresh_tabs_hook ()) "Tabs on opposite side" !current.opposite_tabs in let encodings = combo "File charset encoding " - ~f:(fun s -> - match s with - | "UTF-8" -> - !current.encoding_use_utf8 <- true; - !current.encoding_use_locale <- false - | "LOCALE" -> - !current.encoding_use_utf8 <- false; - !current.encoding_use_locale <- true - | _ -> - !current.encoding_use_utf8 <- false; - !current.encoding_use_locale <- false; - !current.encoding_manual <- s; - ) + ~f:(fun s -> !current.encoding <- (inputenc_of_string s)) ~new_allowed: true - ["UTF-8";"LOCALE";!current.encoding_manual] - (if !current.encoding_use_utf8 then "UTF-8" - else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual) + ("UTF-8"::"LOCALE":: match !current.encoding with + |Emanual s -> [s] + |_ -> [] + ) + (string_of_inputenc !current.encoding) in let read_project = combo @@ -579,11 +655,11 @@ let configure ?(apply=(fun () -> ())) () = bool ~f:(fun s -> !current.contextual_menus_on_goal <- s; - !contextual_menus_on_goal s) + !contextual_menus_on_goal_hook s) "Contextual menus on goal" !current.contextual_menus_on_goal in - let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax; + let misc = [contextual_menus_on_goal;auto_complete;stop_before; vertical_tabs;opposite_tabs] in (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! @@ -591,6 +667,7 @@ let configure ?(apply=(fun () -> ())) () = let cmds = [Section("Fonts", Some `SELECT_FONT, [config_font]); + Section("Colors", Some `SELECT_COLOR, [config_color]); Section("Files", Some `DIRECTORY, [global_auto_revert;global_auto_revert_delay; auto_save; auto_save_delay; (* auto_save_name*) @@ -604,9 +681,8 @@ let configure ?(apply=(fun () -> ())) () = config_appearance); *) Section("Externals", None, - [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print; - cmd_editor; - cmd_browse;doc_url;library_url]); + [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; + cmd_print;cmd_editor;cmd_browse;doc_url;library_url]); Section("Tactics Wizard", None, [automatic_tactics]); Section("Shortcuts", Some `PREFERENCES, @@ -618,7 +694,7 @@ let configure ?(apply=(fun () -> ())) () = (* Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) - let x = edit ~apply ~width:500 "Customizations" cmds in + let x = edit ~apply "Customizations" cmds in (* Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font); *) diff --git a/ide/preferences.mli b/ide/preferences.mli index f55088f1..b680c6f0 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -7,9 +7,11 @@ (************************************************************************) type project_behavior = Ignore_args | Append_args | Subst_args +type inputenc = Elocale | Eutf8 | Emanual of string type pref = { + mutable cmd_coqtop : string option; mutable cmd_coqc : string; mutable cmd_make : string; mutable cmd_coqmakefile : string; @@ -25,9 +27,7 @@ type pref = mutable read_project : project_behavior; mutable project_file_name : string; - mutable encoding_use_locale : bool; - mutable encoding_use_utf8 : bool; - mutable encoding_manual : string; + mutable encoding : inputenc; mutable automatic_tactics : string list; mutable cmd_print : string; @@ -57,9 +57,12 @@ type pref = *) mutable auto_complete : bool; mutable stop_before : bool; - mutable lax_syntax : bool; mutable vertical_tabs : bool; mutable opposite_tabs : bool; + + mutable background_color : string; + mutable processing_color : string; + mutable processed_color : string; } val save_pref : unit -> unit @@ -69,9 +72,11 @@ val current : pref ref val configure : ?apply:(unit -> unit) -> unit -> unit -val change_font : ( Pango.font_description -> unit) ref -val show_toolbar : (bool -> unit) ref -val auto_complete : (bool -> unit) ref -val resize_window : (unit -> unit) ref +(* Hooks *) +val refresh_font_hook : (unit -> unit) ref +val refresh_background_color_hook : (unit -> unit) ref +val refresh_toolbar_hook : (unit -> unit) ref +val resize_window_hook : (unit -> unit) ref +val refresh_tabs_hook : (unit -> unit) ref val use_default_doc_url : string diff --git a/ide/tags.ml b/ide/tags.ml index 52ba54dc..eeace465 100644 --- a/ide/tags.ml +++ b/ide/tags.ml @@ -13,6 +13,9 @@ let make_tag (tt:GText.tag_table) ~name prop = tt#add new_tag#as_tag; new_tag +let processed_color = ref "light green" +let processing_color = ref "light blue" + module Script = struct let table = GText.tag_table () @@ -23,8 +26,8 @@ struct let comment = make_tag table ~name:"comment" [`FOREGROUND "brown"] let reserved = make_tag table ~name:"reserved" [`FOREGROUND "dark red"] let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"] - let to_process = make_tag table ~name:"to_process" [`BACKGROUND "light blue" ;`EDITABLE false] - let processed = make_tag table ~name:"processed" [`BACKGROUND "light green" ;`EDITABLE false] + let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color ;`EDITABLE false] + let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`EDITABLE false] let unjustified = make_tag table ~name:"unjustified" [`UNDERLINE `SINGLE; `FOREGROUND "red"; `BACKGROUND "gold";`EDITABLE false] let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"] let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false] @@ -35,7 +38,7 @@ end module Proof = struct let table = GText.tag_table () - let highlight = make_tag table ~name:"highlight" [`BACKGROUND "light green"] + let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color] let hypothesis = make_tag table ~name:"hypothesis" [] let goal = make_tag table ~name:"goal" [] end @@ -45,3 +48,27 @@ struct let error = make_tag table ~name:"error" [`FOREGROUND "red"] end +let string_of_color clr = + let r = Gdk.Color.red clr in + let g = Gdk.Color.green clr in + let b = Gdk.Color.blue clr in + Printf.sprintf "#%04X%04X%04X" r g b + +let color_of_string s = + let colormap = Gdk.Color.get_system_colormap () in + Gdk.Color.alloc ~colormap (`NAME s) + +let get_processed_color () = color_of_string !processed_color + +let set_processed_color clr = + let s = string_of_color clr in + processed_color := s; + Script.processed#set_property (`BACKGROUND s); + Proof.highlight#set_property (`BACKGROUND s) + +let get_processing_color () = color_of_string !processing_color + +let set_processing_color clr = + let s = string_of_color clr in + processing_color := s; + Script.to_process#set_property (`BACKGROUND s) diff --git a/ide/tags.mli b/ide/tags.mli new file mode 100644 index 00000000..53a8c493 --- /dev/null +++ b/ide/tags.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +module Script : +sig + val table : GText.tag_table + val kwd : GText.tag + val qed : GText.tag + val decl : GText.tag + val proof_decl : GText.tag + val comment : GText.tag + val reserved : GText.tag + val error : GText.tag + val to_process : GText.tag + val processed : GText.tag + val unjustified : GText.tag + val found : GText.tag + val hidden : GText.tag + val folded : GText.tag + val paren : GText.tag + val sentence : GText.tag +end + +module Proof : +sig + val table : GText.tag_table + val highlight : GText.tag + val hypothesis : GText.tag + val goal : GText.tag +end + +module Message : +sig + val table : GText.tag_table + val error : GText.tag +end + +val string_of_color : Gdk.color -> string +val color_of_string : string -> Gdk.color + +val get_processed_color : unit -> Gdk.color +val set_processed_color : Gdk.color -> unit + +val get_processing_color : unit -> Gdk.color +val set_processing_color : Gdk.color -> unit diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml index 3ff60799..4606ef29 100644 --- a/ide/utils/configwin.ml +++ b/ide/utils/configwin.ml @@ -60,9 +60,9 @@ let html = Configwin_ihm.html let edit ?(apply=(fun () -> ())) - title ?(width=400) ?(height=400) + title ?width ?height conf_struct_list = - Configwin_ihm.edit ~with_apply: true ~apply title ~width ~height conf_struct_list + Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list let get = Configwin_ihm.edit ~with_apply: false ~apply: (fun () -> ()) diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml index 9ddc90ef..7dbd0452 100644 --- a/ide/utils/configwin_ihm.ml +++ b/ide/utils/configwin_ihm.ml @@ -1022,7 +1022,7 @@ class configuration_box (tt : GData.tooltips) conf_struct = let rec make_tree iter conf_struct = (* box is not shown at first *) - let box = GPack.vbox ~packing:menu_box#add ~show:false () in + let box = GPack.vbox ~packing:(menu_box#pack ~expand:true) ~show:false () in let new_iter = match iter with | None -> tree#append () | Some parent -> tree#append ~parent () @@ -1136,12 +1136,12 @@ let tabbed_box conf_struct_list buttons tooltips = to configure the various parameters. *) let edit ?(with_apply=true) ?(apply=(fun () -> ())) - title ?(width=400) ?(height=400) + title ?width ?height conf_struct = let dialog = GWindow.dialog ~position:`CENTER ~modal: true ~title: title - ~height ~width + ?height ?width () in let tooltips = GData.tooltips () in |