aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/coq.ml3
-rw-r--r--ide/coqide.ml137
-rw-r--r--ide/ideutils.ml12
-rw-r--r--ide/preferences.ml180
-rw-r--r--ide/preferences.mli2
-rw-r--r--ide/wg_Command.ml12
-rw-r--r--ide/wg_Command.mli2
7 files changed, 175 insertions, 173 deletions
diff --git a/ide/coq.ml b/ide/coq.ml
index 3f96e66a3..db549b19a 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -7,6 +7,7 @@
(************************************************************************)
open Ideutils
+open Preferences
(** * Version and date *)
@@ -61,7 +62,7 @@ let rec filter_coq_opts args =
~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
match pb_mes#run () with
| `YES ->
- let () = !Preferences.current.Preferences.cmd_coqtop <- None in
+ let () = current.cmd_coqtop <- None in
let () = custom_coqtop := None in
let () = pb_mes#destroy () in
filter_coq_opts args
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b94f09053..dcece7aed 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -138,7 +138,7 @@ let cb = GData.clipboard Gdk.Atom.primary
let update_notebook_pos () =
let pos =
- match !current.vertical_tabs, !current.opposite_tabs with
+ match current.vertical_tabs, current.opposite_tabs with
| false, false -> `TOP
| false, true -> `BOTTOM
| true , false -> `LEFT
@@ -532,7 +532,7 @@ object(self)
val mutable last_auto_save_time = 0.
val mutable detached_views = []
- val mutable auto_complete_on = !current.auto_complete
+ val mutable auto_complete_on = current.auto_complete
val hidden_proofs = Hashtbl.create 32
method private toggle_auto_complete =
@@ -597,7 +597,7 @@ object(self)
flash_info "Could not overwrite file"
| _ ->
prerr_endline "Auto revert set to false";
- !current.global_auto_revert <- false;
+ current.global_auto_revert <- false;
disconnect_revert_timer ()
else do_revert ()
end
@@ -620,9 +620,9 @@ object(self)
| None -> None
| Some f ->
let dir = Filename.dirname f in
- let base = (fst !current.auto_save_name) ^
+ let base = (fst current.auto_save_name) ^
(Filename.basename f) ^
- (snd !current.auto_save_name)
+ (snd current.auto_save_name)
in Some (Filename.concat dir base)
method private need_auto_save =
@@ -753,7 +753,7 @@ object(self)
if not full_goal_done then
proof_view#buffer#set_text "";
begin
- let menu_callback = if !current.contextual_menus_on_goal then
+ 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
@@ -991,7 +991,7 @@ object(self)
input_view#set_editable false) ();
push_info "Coq is computing";
let get_current () =
- if !current.stop_before then
+ 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
@@ -1360,16 +1360,17 @@ let search_next_error () =
(**********************************************************************)
let create_session file =
+ let script_buffer =
+ GSourceView2.source_buffer
+ ~tag_table:Tags.Script.table
+ ~highlight_matching_brackets:true
+ ?language:(lang_manager#language current.source_language)
+ ?style_scheme:(style_manager#style_scheme current.source_style)
+ ()
+ in
let script =
Undo.undoable_view
- ~source_buffer:(GSourceView2.source_buffer
- ~tag_table:Tags.Script.table
- ~highlight_matching_brackets:true
- ?language:
- (Preferences.lang_manager#language !current.source_language)
- ?style_scheme:
- (Preferences.style_manager#style_scheme !current.source_style)
- ())
+ ~source_buffer:script_buffer
~show_line_numbers:true
~wrap_mode:`NONE () in
let proof =
@@ -1387,14 +1388,14 @@ let create_session file =
let stack = Stack.create () in
let coqtop_args = match file with
|None -> !sup_args
- |Some the_file -> match !current.read_project with
+ |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)
+ |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
+ |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 Wg_Command.command_window ct current in
+ let command = new Wg_Command.command_window ct in
let finder = new Wg_Find.finder (script :> GText.view) in
let legacy_av = new analyzed_view script proof message stack ct file in
let () = legacy_av#update_stats in
@@ -1428,13 +1429,13 @@ let create_session file =
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;
+ 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];
+ 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;
script=script;
@@ -1577,8 +1578,8 @@ let do_print session =
|Some f_name -> begin
let cmd =
local_cd f_name ^
- !current.cmd_coqdoc ^ " -ps " ^ Filename.quote (Filename.basename f_name) ^
- " | " ^ !current.cmd_print
+ 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
@@ -1712,7 +1713,7 @@ let main files =
let w = GWindow.window
~wm_class:"CoqIde" ~wm_name:"CoqIde"
~allow_grow:true ~allow_shrink:true
- ~width:!current.window_width ~height:!current.window_height
+ ~width:current.window_width ~height:current.window_height
~title:"CoqIde" ()
in
(try
@@ -1815,7 +1816,7 @@ let main files =
| _ -> assert false
in
let cmd =
- local_cd f ^ !current.cmd_coqdoc ^ " --" ^ kind ^
+ local_cd f ^ current.cmd_coqdoc ^ " --" ^ kind ^
" -o " ^ (Filename.quote output) ^ " " ^ (Filename.quote basef)
in
let s,_ = run_command av#insert_message cmd in
@@ -1837,7 +1838,7 @@ let main files =
(*
let toggle_auto_complete_i =
edit_f#add_check_item "_Auto Completion"
- ~active:!current.auto_complete
+ ~active:current.auto_complete
~callback:
in
*)
@@ -1850,9 +1851,9 @@ let main files =
(* begin Preferences *)
let reset_revert_timer () =
disconnect_revert_timer ();
- if !current.global_auto_revert then
+ if current.global_auto_revert then
revert_timer := Some
- (GMain.Timeout.add ~ms:!current.global_auto_revert_delay
+ (GMain.Timeout.add ~ms:current.global_auto_revert_delay
~callback:
(fun () ->
do_if_not_computing "revert" (sync revert_f) session_notebook#pages;
@@ -1867,9 +1868,9 @@ let main files =
let reset_auto_save_timer () =
disconnect_auto_save_timer ();
- if !current.auto_save then
+ if current.auto_save then
auto_save_timer := Some
- (GMain.Timeout.add ~ms:!current.auto_save_delay
+ (GMain.Timeout.add ~ms:current.auto_save_delay
~callback:
(fun () ->
do_if_not_computing "autosave" (sync auto_save_f) session_notebook#pages;
@@ -1944,7 +1945,7 @@ let main files =
| None ->
flash_info "Active buffer has no name"
| Some f ->
- let cmd = !current.cmd_coqc ^ " -I "
+ 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
@@ -1964,7 +1965,7 @@ let main files =
| None ->
flash_info "Cannot make: this buffer has no name"
| Some f ->
- let cmd = local_cd f ^ !current.cmd_make in
+ let cmd = local_cd f ^ current.cmd_make in
(*
save_f ();
@@ -1973,7 +1974,7 @@ let main files =
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")
+ flash_info (current.cmd_make ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
let next_error _ =
try
@@ -2016,10 +2017,10 @@ let main files =
| None ->
flash_info "Cannot make makefile: this buffer has no name"
| Some f ->
- let cmd = local_cd f ^ !current.cmd_coqmakefile in
+ 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")
+ (current.cmd_coqmakefile ^ if s = Unix.WEXITED 0 then " succeeded" else " failed")
in
let file_actions = GAction.action_group ~name:"File" () in
@@ -2055,7 +2056,7 @@ let main files =
) l
in
let tactic_shortcut s sc = GAction.add_action s ~label:("_"^s)
- ~accel:(!current.modifier_for_tactics^sc)
+ ~accel:(current.modifier_for_tactics^sc)
~callback:(do_if_active (fun a -> a#insert_command
("progress "^s^".\n") (s^".\n"))) in
let query_callback command _ =
@@ -2081,7 +2082,7 @@ let main files =
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)
+ |Some ac -> GAction.add_action name ~label ~callback ~accel:(current.modifier_for_templates^ac)
|None -> GAction.add_action name ~label ~callback ?accel:None
in
GAction.add_actions file_actions [
@@ -2152,7 +2153,7 @@ let main files =
| 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 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 _ ->
@@ -2169,8 +2170,8 @@ let main files =
GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<Ctrl>Tab") ~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;
+ ~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
@@ -2182,7 +2183,7 @@ let main files =
List.iter
(fun (opts,name,label,key,dflt) ->
GAction.add_toggle_action name ~active:dflt ~label
- ~accel:(!current.modifier_for_display^key)
+ ~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)
@@ -2191,41 +2192,41 @@ let main files =
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");
+ ~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");
+ ~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");
+ ~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");
+ ~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");
+ ~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");
+ ~accel:(current.modifier_for_navigation^"Break");
(* wait for this available in GtkSourceView !
GAction.add_action "Hide" ~label:"_Hide" ~stock:`MISSING_IMAGE
~callback:(fun _ -> let sess = session_notebook#current_term in
toggle_proof_visibility sess.script#buffer
sess.analyzed_view#get_insert) ~tooltip:"Hide proof"
- ~accel:(!current.modifier_for_navigation^"h");*)
+ ~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");
+ ~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");
+ ~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");
+ current.automatic_tactics))
+ ~accel:(current.modifier_for_tactics^"dollar");
tactic_shortcut "auto" "a";
tactic_shortcut "auto with *" "asterisk";
tactic_shortcut "eauto" "e";
@@ -2258,7 +2259,7 @@ let main files =
"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");
+ ~accel:(current.modifier_for_templates^"C");
];
add_gen_actions "Template" templates_actions Coq_commands.commands;
GAction.add_actions queries_actions [
@@ -2284,8 +2285,8 @@ let main files =
~callback:(fun _ -> do_if_not_computing "detach view"
(function {script=v;analyzed_view=av} ->
let w = GWindow.window ~show:true
- ~width:(!current.window_width*2/3)
- ~height:(!current.window_height*2/3)
+ ~width:(current.window_width*2/3)
+ ~height:(current.window_height*2/3)
~position:`CENTER
~title:(match av#filename with
| None -> "*Unnamed*"
@@ -2301,7 +2302,7 @@ let main files =
()
in
nv#misc#modify_font
- !current.text_font;
+ current.text_font;
ignore (w#connect#destroy
~callback:
(fun () -> av#remove_detached_view w));
@@ -2317,7 +2318,7 @@ let main files =
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);
+ 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;
@@ -2366,10 +2367,10 @@ let main files =
(* Initializing hooks *)
refresh_toolbar_hook :=
- (fun () -> if !current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ());
+ (fun () -> if current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ());
refresh_font_hook :=
(fun () ->
- let fd = !current.text_font in
+ let fd = current.text_font in
let iter_page p =
p.script#misc#modify_font fd;
p.proof_view#misc#modify_font fd;
@@ -2380,7 +2381,7 @@ let main files =
);
refresh_background_color_hook :=
(fun () ->
- let clr = Tags.color_of_string !current.background_color in
+ 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];
@@ -2391,8 +2392,8 @@ let main files =
);
resize_window_hook := (fun () ->
w#resize
- ~width:!current.window_width
- ~height:!current.window_height);
+ ~width:current.window_width
+ ~height:current.window_height);
refresh_tabs_hook := update_notebook_pos;
let about_full_string =
@@ -2461,8 +2462,8 @@ let main files =
*)
(* 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);
+ 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
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index ea15bd5f8..2507c914a 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -76,7 +76,7 @@ let do_convert s =
("Converting from "^ enc);
Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:enc
in
- match !current.encoding with
+ match current.encoding with
|Preferences.Eutf8 | Preferences.Elocale -> from_loc ()
|Emanual enc ->
try
@@ -93,7 +93,7 @@ Please choose a correct encoding in the preference panel.*)";;
let try_export file_name s =
try let s =
- try match !current.encoding with
+ try match current.encoding with
|Eutf8 -> begin
(prerr_endline "UTF-8 is enforced" ;s)
end
@@ -258,7 +258,7 @@ let coqtop_path () =
let file = match !custom_coqtop with
| Some s -> s
| None ->
- match !current.cmd_coqtop with
+ match current.cmd_coqtop with
| Some s -> s
| None ->
let prog = String.copy Sys.executable_name in
@@ -296,7 +296,7 @@ let run_command f c =
(Unix.close_process_full (cin,cout,cerr), Buffer.contents result)
let browse f url =
- let com = Minilib.subst_command_placeholder !current.cmd_browse url in
+ let com = Minilib.subst_command_placeholder current.cmd_browse url in
let _ = Unix.open_process_out com in ()
(* This beautiful message will wait for twt ...
if s = 127 then
@@ -304,10 +304,10 @@ let browse f url =
"\"\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
+ 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
if Sys.file_exists addr then "file://"^addr else Coq_config.wwwrefman
- else !current.doc_url
+ else current.doc_url
let url_for_keyword =
let ht = Hashtbl.create 97 in
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 3600363d6..2303b0011 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -144,8 +144,7 @@ type pref =
let use_default_doc_url = "(automatic)"
-let (current:pref ref) =
- ref {
+let current = {
cmd_coqtop = None;
cmd_coqc = "coqc";
cmd_make = "make";
@@ -213,7 +212,7 @@ let save_pref () =
if not (Sys.file_exists Minilib.xdg_config_home)
then Unix.mkdir Minilib.xdg_config_home 0o700;
let () = try GtkData.AccelMap.save accel_file with _ -> () in
- let p = !current in
+ let p = current in
let add = Minilib.Stringmap.add in
let (++) x f = f x in
@@ -269,7 +268,7 @@ let save_pref () =
let load_pref () =
let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
- let p = !current in
+ let p = current in
let m = Config_lexer.load_file loaded_pref_file in
let np = { p with cmd_coqc = p.cmd_coqc } in
@@ -338,37 +337,36 @@ let load_pref () =
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
+ set_hd "processed_color" (fun v -> np.processed_color <- v)
(*
- Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+ 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
+ ~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)
- " coqc" !current.cmd_coqc in
+ ~f:(fun s -> current.cmd_coqc <- s)
+ " coqc" current.cmd_coqc in
let cmd_make =
string
- ~f:(fun s -> !current.cmd_make <- s)
- " make" !current.cmd_make in
+ ~f:(fun s -> current.cmd_make <- s)
+ " make" current.cmd_make in
let cmd_coqmakefile =
string
- ~f:(fun s -> !current.cmd_coqmakefile <- s)
- "coqmakefile" !current.cmd_coqmakefile in
+ ~f:(fun s -> current.cmd_coqmakefile <- s)
+ "coqmakefile" current.cmd_coqmakefile in
let cmd_coqdoc =
string
- ~f:(fun s -> !current.cmd_coqdoc <- s)
- " coqdoc" !current.cmd_coqdoc in
+ ~f:(fun s -> current.cmd_coqdoc <- s)
+ " coqdoc" current.cmd_coqdoc in
let cmd_print =
string
- ~f:(fun s -> !current.cmd_print <- s)
- " Print ps" !current.cmd_print in
+ ~f:(fun s -> current.cmd_print <- s)
+ " Print ps" current.cmd_print in
let config_font =
let box = GPack.hbox () in
@@ -378,15 +376,15 @@ let configure ?(apply=(fun () -> ())) () =
box#pack ~expand:true w#coerce;
ignore (w#misc#connect#realize
~callback:(fun () -> w#set_font_name
- (Pango.Font.to_string !current.text_font)));
+ (Pango.Font.to_string current.text_font)));
custom
~label:"Fonts for text"
box
(fun () ->
let fd = w#font_name in
- !current.text_font <- (Pango.Font.from_string fd) ;
+ current.text_font <- (Pango.Font.from_string fd) ;
(*
- Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+ Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string current.text_font);
*)
!refresh_font_hook ())
true
@@ -416,7 +414,7 @@ let configure ?(apply=(fun () -> ())) () =
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))
+ ~color:(Tags.color_of_string (current.background_color))
~packing:(table#attach ~left:1 ~top:0) ()
in
let processed_button = GButton.color_button
@@ -439,9 +437,9 @@ let configure ?(apply=(fun () -> ())) () =
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;
+ 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
@@ -453,40 +451,40 @@ let configure ?(apply=(fun () -> ())) () =
let show_toolbar =
bool
~f:(fun s ->
- !current.show_toolbar <- s;
+ current.show_toolbar <- s;
!show_toolbar s)
- "Show toolbar" !current.show_toolbar
+ "Show toolbar" current.show_toolbar
in
let window_height =
string
- ~f:(fun s -> !current.window_height <- (try int_of_string s with _ -> 600);
+ ~f:(fun s -> current.window_height <- (try int_of_string s with _ -> 600);
!resize_window ();
)
"Window height"
- (string_of_int !current.window_height)
+ (string_of_int current.window_height)
in
let window_width =
string
- ~f:(fun s -> !current.window_width <-
+ ~f:(fun s -> current.window_width <-
(try int_of_string s with _ -> 800))
"Window width"
- (string_of_int !current.window_width)
+ (string_of_int current.window_width)
in
*)
let auto_complete =
bool
~f:(fun s ->
- !current.auto_complete <- s;
+ current.auto_complete <- s;
!auto_complete_hook s)
- "Auto Complete" !current.auto_complete
+ "Auto Complete" current.auto_complete
in
(* let use_utf8_notation =
bool
~f:(fun b ->
- !current.use_utf8_notation <- b;
+ current.use_utf8_notation <- b;
)
- "Use Unicode Notation: " !current.use_utf8_notation
+ "Use Unicode Notation: " current.use_utf8_notation
in
*)
(*
@@ -494,120 +492,120 @@ let configure ?(apply=(fun () -> ())) () =
*)
let global_auto_revert =
bool
- ~f:(fun s -> !current.global_auto_revert <- s)
- "Enable global auto revert" !current.global_auto_revert
+ ~f:(fun s -> current.global_auto_revert <- s)
+ "Enable global auto revert" current.global_auto_revert
in
let global_auto_revert_delay =
string
- ~f:(fun s -> !current.global_auto_revert_delay <-
+ ~f:(fun s -> current.global_auto_revert_delay <-
(try int_of_string s with _ -> 10000))
"Global auto revert delay (ms)"
- (string_of_int !current.global_auto_revert_delay)
+ (string_of_int current.global_auto_revert_delay)
in
let auto_save =
bool
- ~f:(fun s -> !current.auto_save <- s)
- "Enable auto save" !current.auto_save
+ ~f:(fun s -> current.auto_save <- s)
+ "Enable auto save" current.auto_save
in
let auto_save_delay =
string
- ~f:(fun s -> !current.auto_save_delay <-
+ ~f:(fun s -> current.auto_save_delay <-
(try int_of_string s with _ -> 10000))
"Auto save delay (ms)"
- (string_of_int !current.auto_save_delay)
+ (string_of_int current.auto_save_delay)
in
let stop_before =
bool
- ~f:(fun s -> !current.stop_before <- s)
- "Stop interpreting before the current point" !current.stop_before
+ ~f:(fun s -> current.stop_before <- s)
+ "Stop interpreting before the current point" current.stop_before
in
let vertical_tabs =
bool
- ~f:(fun s -> !current.vertical_tabs <- s; !refresh_tabs_hook ())
- "Vertical tabs" !current.vertical_tabs
+ ~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; !refresh_tabs_hook ())
- "Tabs on opposite side" !current.opposite_tabs
+ ~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 -> !current.encoding <- (inputenc_of_string s))
+ ~f:(fun s -> current.encoding <- (inputenc_of_string s))
~new_allowed: true
- ("UTF-8"::"LOCALE":: match !current.encoding with
+ ("UTF-8"::"LOCALE":: match current.encoding with
|Emanual s -> [s]
|_ -> []
)
- (string_of_inputenc !current.encoding)
+ (string_of_inputenc current.encoding)
in
let source_style =
combo "Highlighting style"
- ~f:(fun s -> !current.source_style <- s) ~new_allowed:false
- style_manager#style_scheme_ids !current.source_style
+ ~f:(fun s -> current.source_style <- s) ~new_allowed:false
+ style_manager#style_scheme_ids current.source_style
in
let read_project =
combo
"Project file options are"
- ~f:(fun s -> !current.read_project <- project_behavior_of_string s)
+ ~f:(fun s -> current.read_project <- project_behavior_of_string s)
~editable:false
[string_of_project_behavior Subst_args;
string_of_project_behavior Append_args;
string_of_project_behavior Ignore_args]
- (string_of_project_behavior !current.read_project)
+ (string_of_project_behavior current.read_project)
in
let project_file_name =
string "Default name for project file"
- ~f:(fun s -> !current.project_file_name <- s)
- !current.project_file_name
+ ~f:(fun s -> current.project_file_name <- s)
+ current.project_file_name
in
let help_string =
"restart to apply"
in
- let the_valid_mod = str_to_mod_list !current.modifiers_valid in
+ let the_valid_mod = str_to_mod_list current.modifiers_valid in
let modifier_for_tactics =
modifiers
~allow:the_valid_mod
- ~f:(fun l -> !current.modifier_for_tactics <- mod_list_to_str l)
+ ~f:(fun l -> current.modifier_for_tactics <- mod_list_to_str l)
~help:help_string
"Modifiers for Tactics Menu"
- (str_to_mod_list !current.modifier_for_tactics)
+ (str_to_mod_list current.modifier_for_tactics)
in
let modifier_for_templates =
modifiers
~allow:the_valid_mod
- ~f:(fun l -> !current.modifier_for_templates <- mod_list_to_str l)
+ ~f:(fun l -> current.modifier_for_templates <- mod_list_to_str l)
~help:help_string
"Modifiers for Templates Menu"
- (str_to_mod_list !current.modifier_for_templates)
+ (str_to_mod_list current.modifier_for_templates)
in
let modifier_for_navigation =
modifiers
~allow:the_valid_mod
- ~f:(fun l -> !current.modifier_for_navigation <- mod_list_to_str l)
+ ~f:(fun l -> current.modifier_for_navigation <- mod_list_to_str l)
~help:help_string
"Modifiers for Navigation Menu"
- (str_to_mod_list !current.modifier_for_navigation)
+ (str_to_mod_list current.modifier_for_navigation)
in
let modifier_for_display =
modifiers
~allow:the_valid_mod
- ~f:(fun l -> !current.modifier_for_display <- mod_list_to_str l)
+ ~f:(fun l -> current.modifier_for_display <- mod_list_to_str l)
~help:help_string
"Modifiers for Display Menu"
- (str_to_mod_list !current.modifier_for_display)
+ (str_to_mod_list current.modifier_for_display)
in
let modifiers_valid =
modifiers
- ~f:(fun l -> !current.modifiers_valid <- mod_list_to_str l)
+ ~f:(fun l -> current.modifiers_valid <- mod_list_to_str l)
"Allowed modifiers"
the_valid_mod
in
@@ -616,11 +614,11 @@ let configure ?(apply=(fun () -> ())) () =
combo
~help:"(%s for file name)"
"External editor"
- ~f:(fun s -> !current.cmd_editor <- s)
+ ~f:(fun s -> current.cmd_editor <- s)
~new_allowed: true
- (predefined@[if List.mem !current.cmd_editor predefined then ""
- else !current.cmd_editor])
- !current.cmd_editor
+ (predefined@[if List.mem current.cmd_editor predefined then ""
+ else current.cmd_editor])
+ current.cmd_editor
in
let cmd_browse =
let predefined = [
@@ -633,11 +631,11 @@ let configure ?(apply=(fun () -> ())) () =
combo
~help:"(%s for url)"
"Browser"
- ~f:(fun s -> !current.cmd_browse <- s)
+ ~f:(fun s -> current.cmd_browse <- s)
~new_allowed: true
- (predefined@[if List.mem !current.cmd_browse predefined then ""
- else !current.cmd_browse])
- !current.cmd_browse
+ (predefined@[if List.mem current.cmd_browse predefined then ""
+ else current.cmd_browse])
+ current.cmd_browse
in
let doc_url =
let predefined = [
@@ -647,11 +645,11 @@ let configure ?(apply=(fun () -> ())) () =
] in
combo
"Manual URL"
- ~f:(fun s -> !current.doc_url <- s)
+ ~f:(fun s -> current.doc_url <- s)
~new_allowed: true
- (predefined@[if List.mem !current.doc_url predefined then ""
- else !current.doc_url])
- !current.doc_url in
+ (predefined@[if List.mem current.doc_url predefined then ""
+ else current.doc_url])
+ current.doc_url in
let library_url =
let predefined = [
"file://"^(List.fold_left Filename.concat (Coq_config.docdir) ["html";"stdlib";""]);
@@ -659,27 +657,27 @@ let configure ?(apply=(fun () -> ())) () =
] in
combo
"Library URL"
- ~f:(fun s -> !current.library_url <- s)
+ ~f:(fun s -> current.library_url <- s)
~new_allowed: true
- (predefined@[if List.mem !current.library_url predefined then ""
- else !current.library_url])
- !current.library_url
+ (predefined@[if List.mem current.library_url predefined then ""
+ else current.library_url])
+ current.library_url
in
let automatic_tactics =
strings
- ~f:(fun l -> !current.automatic_tactics <- l)
+ ~f:(fun l -> current.automatic_tactics <- l)
~add:(fun () -> ["<edit me>"])
"Wizard tactics to try in order"
- !current.automatic_tactics
+ current.automatic_tactics
in
let contextual_menus_on_goal =
bool
~f:(fun s ->
- !current.contextual_menus_on_goal <- s;
+ current.contextual_menus_on_goal <- s;
!contextual_menus_on_goal_hook s)
- "Contextual menus on goal" !current.contextual_menus_on_goal
+ "Contextual menus on goal" current.contextual_menus_on_goal
in
let misc = [contextual_menus_on_goal;auto_complete;stop_before;
@@ -715,11 +713,11 @@ let configure ?(apply=(fun () -> ())) () =
misc)]
in
(*
- Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+ Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string current.text_font);
*)
let x = edit ~apply "Customizations" cmds in
(*
- Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+ Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string current.text_font);
*)
match x with
| Return_apply | Return_ok -> save_pref ()
diff --git a/ide/preferences.mli b/ide/preferences.mli
index fae7ebd9f..92a748ef9 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -74,7 +74,7 @@ type pref =
val save_pref : unit -> unit
val load_pref : unit -> unit
-val current : pref ref
+val current : pref
val configure : ?apply:(unit -> unit) -> unit -> unit
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index a34e5ebeb..d52be74cb 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -6,7 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-class command_window coqtop current =
+open Preferences
+
+class command_window coqtop =
(* let window = GWindow.window
~allow_grow:true ~allow_shrink:true
~width:500 ~height:250
@@ -98,8 +100,8 @@ object(self)
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_font current.text_font;
+ let clr = Tags.color_of_string current.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;
@@ -144,11 +146,11 @@ object(self)
self#frame#misc#show ()
method refresh_font () =
- let iter view = view#misc#modify_font !current.Preferences.text_font in
+ let iter view = view#misc#modify_font current.text_font in
List.iter iter !views
method refresh_color () =
- let clr = Tags.color_of_string !current.Preferences.background_color in
+ let clr = Tags.color_of_string current.background_color in
let iter view = view#misc#modify_base [`NORMAL, `COLOR clr] in
List.iter iter !views
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index c34b6cf67..c1af68323 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -7,7 +7,7 @@
(************************************************************************)
class command_window :
- Coq.coqtop ref -> Preferences.pref ref ->
+ Coq.coqtop ref ->
object
method new_command : ?command:string -> ?term:string -> unit -> unit
method frame : GBin.frame
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 23:14:01 +0000