diff options
| -rw-r--r-- | Makefile.build | 20 | ||||
| -rw-r--r-- | ide/coq.ml | 26 | ||||
| -rw-r--r-- | ide/coq.mli | 3 | ||||
| -rw-r--r-- | ide/coqide.ml | 12 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 1 | ||||
| -rw-r--r-- | ide/ideutils.ml | 59 | ||||
| -rw-r--r-- | ide/ideutils.mli | 1 | ||||
| -rw-r--r-- | ide/minilib.ml | 12 | ||||
| -rw-r--r-- | ide/minilib.mli | 3 | ||||
| -rw-r--r-- | lib/envars.ml | 3 |
10 files changed, 59 insertions, 81 deletions
diff --git a/Makefile.build b/Makefile.build index 0e49c1381..5a8f5dbfc 100644 --- a/Makefile.build +++ b/Makefile.build @@ -330,8 +330,6 @@ $(COQIDE): .PHONY: install-coqide install-ide-no install-ide-byte install-ide-opt .PHONY: install-ide-files install-ide-info install-im -FULLIDELIB=$(FULLCOQLIB)/ide - install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info install-ide-no: @@ -351,23 +349,15 @@ install-ide-opt: cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE) install-ide-files: - $(MKDIR) $(FULLIDELIB) - $(INSTALLLIB) ide/coq.png $(FULLIDELIB) + $(MKDIR) $(FULLDATADIR) + $(INSTALLLIB) ide/coq.png $(FULLDATADIR) $(MKDIR) $(FULLCONFIGDIR) $(INSTALLLIB) ide/coqide-gtk2rc $(FULLCONFIGDIR) if [ $(IDEOPTINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi install-ide-info: - $(MKDIR) $(FULLIDELIB) - $(INSTALLLIB) ide/FAQ $(FULLIDELIB) - -# IM files - -IMFILES=$(addprefix ide/uim/, coqide.scm coqide-rules.scm coqide-custom.scm) - -install-im: - $(INSTALLLIB) $(IMFILES) $(UIMSCRIPTDIR) - uim-module-manager --register coqide + $(MKDIR) $(FULLDOCDIR) + $(INSTALLLIB) ide/FAQ $(FULLDOCDIR)/FAQ-CoqIde ########################################################################### # tests @@ -580,6 +570,7 @@ ifdef COQINSTALLPREFIX FULLBINDIR=$(BINDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) +FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) @@ -588,6 +579,7 @@ else FULLBINDIR=$(BINDIR) FULLCOQLIB=$(COQLIBINSTALL) FULLCONFIGDIR=$(CONFIGDIR) +FULLDATADIR=$(DATADIR) FULLMANDIR=$(MANDIR) FULLEMACSLIB=$(EMACSLIB) FULLCOQDOCDIR=$(COQDOCDIR) diff --git a/ide/coq.ml b/ide/coq.ml index d5fc90e1e..16a07b01c 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -85,32 +85,6 @@ let check_connection args = List.iter Minilib.safe_prerr_endline lines; exit 1 -(** It is tempting to merge the following function with the previous one, - but check_connection fails if no initial.coq is found, while - check_coqlib doesn't check that. *) - -let check_coqlib args = - try - let argstr = String.concat " " (List.map Filename.quote args) in - let cmd = Filename.quote !Minilib.coqtop_path ^ " " ^ argstr ^ " -where" in - let ic = Unix.open_process_in cmd in - let lines = read_all_lines ic in - match Unix.close_process_in ic with - | Unix.WEXITED 0 -> - (match lines with - | [coqlib] -> coqlib - | _ -> raise (Coqtop_output lines)) - | _ -> 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 - - (** * The structure describing a coqtop sub-process *) type coqtop = { diff --git a/ide/coq.mli b/ide/coq.mli index 662c6ccf2..9d64da6c2 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -20,9 +20,6 @@ val filter_coq_opts : string list -> bool * string list (** A mock coqtop launch, checking in particular that initial.coq is found *) val check_connection : string list -> unit -(** Same, with less checks, but returning coqlib *) -val check_coqlib : string list -> string - (** * The structure describing a coqtop sub-process *) type coqtop diff --git a/ide/coqide.ml b/ide/coqide.ml index 7a1d18485..009a19892 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1813,7 +1813,9 @@ let main files = ~title:"CoqIde" () in (try - let icon_image = lib_ide_file "coq.png" in + let icon_image = Filename.concat (List.find + (fun x -> Sys.file_exists (Filename.concat x "coq.png")) + Minilib.xdg_data_dirs) "coq.png" in let icon = GdkPixbuf.from_file icon_image in w#set_icon (Some icon) with _ -> ()); @@ -2828,7 +2830,9 @@ let main files = if Glib.Utf8.validate initial_string then b#insert ~iter:b#start_iter initial_string; (try - let image = lib_ide_file "coq.png" in + let image = Filename.concat (List.find + (fun x -> Sys.file_exists (Filename.concat x "coq.png")) + Minilib.xdg_data_dirs) "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; @@ -2838,7 +2842,9 @@ let main files = let about (b:GText.buffer) = (try - let image = lib_ide_file "coq.png" in + let image = Filename.concat (List.find + (fun x -> Sys.file_exists (Filename.concat x "coq.png")) + Minilib.xdg_data_dirs) "coq.png" in let startup_image = GdkPixbuf.from_file image in b#insert ~iter:b#start_iter "\n\n"; b#insert_pixbuf ~iter:b#start_iter ~pixbuf:startup_image; diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4 index 650cf9274..3fec06313 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml4 @@ -70,7 +70,6 @@ let () = 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; - Minilib.coqlib := Coq.check_coqlib args; Coqide.sup_args := args; Coqide.ignore_break (); (try diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 1cf24948e..fd460c4e9 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -34,9 +34,6 @@ let debug = ref (false) let prerr_endline s = if !debug then try prerr_endline s;flush stderr with _ -> () -let lib_ide_file f = - Filename.concat (Filename.concat !Minilib.coqlib "ide") f - let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT let is_char_start c = let code = Char.code c in code < 0x80 || code >= 0xc0 @@ -295,34 +292,36 @@ let doc_url () = let url_for_keyword = let ht = Hashtbl.create 97 in - lazy ( - begin try - let cin = - try open_in (lib_ide_file "index_urls.txt") - with _ -> - let doc_url = doc_url () in - let n = String.length doc_url in - if n > 8 && String.sub doc_url 0 7 = "file://" then - open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt") - else - raise Exit - in - try while true do - let s = input_line cin in - try - let i = String.index s ',' in - let k = String.sub s 0 i in - let u = String.sub s (i + 1) (String.length s - i - 1) in - Hashtbl.add ht k u + lazy ( + begin try + let cin = + try let index_urls = Filename.concat (List.find + (fun x -> Sys.file_exists (Filename.concat x "index_urls.txt")) + Minilib.xdg_config_dirs) "index_urls.txt" in + open_in index_urls + with Not_found -> + let doc_url = doc_url () in + let n = String.length doc_url in + if n > 8 && String.sub doc_url 0 7 = "file://" then + open_in (String.sub doc_url 7 (n-7) ^ "index_urls.txt") + else + raise Exit + in + try while true do + let s = input_line cin in + try + let i = String.index s ',' in + let k = String.sub s 0 i in + let u = String.sub s (i + 1) (String.length s - i - 1) in + Hashtbl.add ht k u + with _ -> + Minilib.safe_prerr_endline "Warning: Cannot parse documentation index file." + done with End_of_file -> + close_in cin with _ -> - Minilib.safe_prerr_endline "Warning: Cannot parse documentation index file." - done with End_of_file -> - close_in cin - with _ -> - Minilib.safe_prerr_endline "Warning: Cannot find documentation index file." - end; - Hashtbl.find ht : string -> string) - + Minilib.safe_prerr_endline "Warning: Cannot find documentation index file." + end; + Hashtbl.find ht : string -> string) let browse_keyword f text = try let u = Lazy.force url_for_keyword text in browse f (doc_url() ^ u) diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 977aa0c14..1e29d323c 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -27,7 +27,6 @@ val get_insert : < get_iter_at_mark : [> `INSERT] -> 'a; .. > -> 'a val is_char_start : char -> bool -val lib_ide_file : string -> string val my_stat : string -> Unix.stats option (** debug printing *) diff --git a/ide/minilib.ml b/ide/minilib.ml index 4896cbd4b..cec77f3b8 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -87,8 +87,18 @@ let xdg_config_dirs = 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])) +let xdg_data_home = + try + Filename.concat (Sys.getenv "XDG_DATA_HOME") "coq" + with Not_found -> + Filename.concat home "/.local/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])) -let coqlib = ref "" let coqtop_path = ref "" (* On a Win32 application with no console, writing to stderr raise diff --git a/ide/minilib.mli b/ide/minilib.mli index 60a5eed48..53d6c87c2 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -24,8 +24,9 @@ val subst_command_placeholder : string -> string -> string val home : string val xdg_config_home : string val xdg_config_dirs : string list +val xdg_data_home : string +val xdg_data_dirs : string list -val coqlib : string ref val coqtop_path : string ref (** safe version of Pervasives.prerr_endline diff --git a/lib/envars.ml b/lib/envars.ml index dc71cb433..e5c938037 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -64,7 +64,8 @@ let xdg_config_home = let xdg_data_dirs = 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" ] + with Not_found -> "/usr/local/share/coq" :: "/usr/share/coq" + :: (match Coq_config.datadir with |None -> [] |Some datadir -> [datadir]) let xdg_dirs = let dirs = xdg_data_home :: xdg_data_dirs |