diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-25 23:29:52 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-26 00:34:21 +0200 |
commit | 20ae742e391a8db65e203213a124126ce8621fe1 (patch) | |
tree | 4b0e7ff8640323fc5c83bfec8f13d4e9ac45f710 /ide/ideutils.ml | |
parent | bfbb9f063434623d7c3dac8aa4aaf64c4ec84373 (diff) |
Replacing old-style preferences in CoqIDE.
There is no remaining global preference record anymore, every preference
is now defined in the new event-based style.
Diffstat (limited to 'ide/ideutils.ml')
-rw-r--r-- | ide/ideutils.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 3c5a551c1..053bba805 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -74,7 +74,7 @@ let do_convert s = in let s = if Glib.Utf8.validate s then (Minilib.log "Input is UTF-8"; s) - else match current.encoding with + else match encoding#get with |Preferences.Eutf8 | Preferences.Elocale -> from_loc () |Emanual enc -> try from_manual enc with _ -> from_loc () in @@ -90,7 +90,7 @@ Please choose a correct encoding in the preference panel.*)";; let try_export file_name s = let s = - try match current.encoding with + try match encoding#get with |Eutf8 -> Minilib.log "UTF-8 is enforced" ; s |Elocale -> let is_unicode,char_set = Glib.Convert.get_charset () in @@ -364,7 +364,7 @@ let run_command display finally cmd = (** Web browsing *) let browse prerr url = - let com = Util.subst_command_placeholder current.cmd_browse url in + let com = Util.subst_command_placeholder cmd_browse#get url in let finally = function | Unix.WEXITED 127 -> prerr @@ -375,13 +375,13 @@ let browse prerr url = run_command (fun _ -> ()) finally com let doc_url () = - if current.doc_url = use_default_doc_url || current.doc_url = "" + if doc_url#get = use_default_doc_url || doc_url#get = "" 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 doc_url#get let url_for_keyword = let ht = Hashtbl.create 97 in |