diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdep.ml | 24 | ||||
| -rw-r--r-- | tools/coqdep_boot.ml | 6 | ||||
| -rw-r--r-- | tools/coqdep_common.ml | 20 | ||||
| -rw-r--r-- | tools/coqdep_common.mli | 5 | ||||
| -rw-r--r-- | tools/coqdoc/cdglobals.mli | 49 |
5 files changed, 90 insertions, 14 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 044399544a..cba9c3eb07 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -320,19 +320,25 @@ let treat_coq_file chan = List.fold_left (fun accu v -> mark_v_done from accu v) acc strl | Declare sl -> let declare suff dir s = - let base = file_name s dir in - let opt = if !option_natdynlk then " " ^ base ^ ".cmxs" else "" in - (escape base, suff ^ opt) + let base = escape (file_name s dir) in + match !option_dynlink with + | No -> [] + | Byte -> [base,suff] + | Opt -> [base,".cmxs"] + | Both -> [base,suff; base,".cmxs"] + | Variable -> + if suff=".cmo" then [base,"$(DYNOBJ)"] + else [base,"$(DYNLIB)"] in let decl acc str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then let () = deja_vu_ml := StrSet.add s !deja_vu_ml in match search_mllib_known s with - | Some mldir -> (declare ".cma" mldir s) :: acc + | Some mldir -> (declare ".cma" mldir s) @ acc | None -> match search_ml_known s with - | Some mldir -> (declare ".cmo" mldir s) :: acc + | Some mldir -> (declare ".cmo" mldir s) @ acc | None -> acc else acc in @@ -449,6 +455,7 @@ let usage () = eprintf " -coqlib dir : set the coq standard library directory\n"; eprintf " -suffix s : \n"; eprintf " -slash : deprecated, no effect\n"; + eprintf " -dyndep (opt|byte|both|no|var) : set how dependencies over ML modules are printed"; exit 1 let split_period = Str.split (Str.regexp (Str.quote ".")) @@ -476,17 +483,22 @@ let rec parse = function | "-slash" :: ll -> Printf.eprintf "warning: option -slash has no effect and is deprecated.\n"; parse ll + | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll + | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll + | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll + | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll + | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () | f :: ll -> treat_file None f; parse ll | [] -> () let coqdep () = if Array.length Sys.argv < 2 then usage (); + if not Coq_config.has_natdynlink then option_dynlink := No; parse (List.tl (Array.to_list Sys.argv)); (* Add current dir with empty logical path if not set by options above. *) (try ignore (Coqdep_common.find_dir_logpath (Sys.getcwd())) with Not_found -> add_norec_dir_import add_known "." []); - if not Coq_config.has_natdynlink then option_natdynlk := false; (* NOTE: These directories are searched from last to first *) if !option_boot then begin add_rec_dir_import add_known "theories" ["Coq"]; diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 6fc826833e..25f62d2bec 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -16,7 +16,11 @@ open Coqdep_common *) let rec parse = function - | "-natdynlink" :: "no" :: ll -> option_natdynlk := false; parse ll + | "-dyndep" :: "no" :: ll -> option_dynlink := No; parse ll + | "-dyndep" :: "opt" :: ll -> option_dynlink := Opt; parse ll + | "-dyndep" :: "byte" :: ll -> option_dynlink := Byte; parse ll + | "-dyndep" :: "both" :: ll -> option_dynlink := Both; parse ll + | "-dyndep" :: "var" :: ll -> option_dynlink := Variable; parse ll | "-c" :: ll -> option_c := true; parse ll | "-boot" :: ll -> parse ll (* We're already in boot mode by default *) | "-mldep" :: ocamldep :: ll -> diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index f5e93527c9..bf8bcd0c44 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -15,7 +15,7 @@ open Minisys behavior is the one of [coqdep -boot]. Its only dependencies are [Coqdep_lexer], [Unix] and [Minisys], and it should stay so. If it need someday some additional information, pass it via - options (see for instance [option_natdynlk] below). + options (see for instance [option_dynlink] below). *) module StrSet = Set.Make(String) @@ -26,9 +26,11 @@ module StrListMap = Map.Make(StrList) let stderr = Pervasives.stderr let stdout = Pervasives.stdout +type dynlink = Opt | Byte | Both | No | Variable + let option_c = ref false let option_noglob = ref false -let option_natdynlk = ref true +let option_dynlink = ref Both let option_boot = ref false let option_mldep = ref None @@ -383,10 +385,16 @@ let rec traite_fichier_Coq suffixe verbose f = end) strl | Declare sl -> let declare suff dir s = - let base = file_name s dir in - let opt = if !option_natdynlk then " "^base^".cmxs" else "" in - printf " %s%s%s" (escape base) suff opt - in + let base = escape (file_name s dir) in + match !option_dynlink with + | No -> () + | Byte -> printf " %s%s" base suff + | Opt -> printf " %s.cmxs" base + | Both -> printf " %s%s %s.cmxs" base suff base + | Variable -> + printf " %s%s" base + (if suff=".cmo" then "$(DYNOBJ)" else "$(DYNLIB)") + in let decl str = let s = basename_noext str in if not (StrSet.mem s !deja_vu_ml) then begin diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index 10da0240dd..8c1787d315 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -19,7 +19,10 @@ val find_dir_logpath: string -> string list val option_c : bool ref val option_noglob : bool ref val option_boot : bool ref -val option_natdynlk : bool ref + +type dynlink = Opt | Byte | Both | No | Variable + +val option_dynlink : dynlink ref val option_mldep : string option ref val norec_dirs : StrSet.t ref val suffixe : string ref diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli new file mode 100644 index 0000000000..2c9b3fb8e8 --- /dev/null +++ b/tools/coqdoc/cdglobals.mli @@ -0,0 +1,49 @@ +type target_language = LaTeX | HTML | TeXmacs | Raw +val target_language : target_language ref +type output_t = StdOut | MultFiles | File of string +val output_dir : string ref +val out_to : output_t ref +val out_channel : out_channel ref +val ( / ) : string -> string -> string +val coqdoc_out : string -> string +val open_out_file : string -> unit +val close_out_file : unit -> unit +type glob_source_t = NoGlob | DotGlob | GlobFile of string +val glob_source : glob_source_t ref +val normalize_path : string -> string +val normalize_filename : string -> string * string +val guess_coqlib : unit -> string +val header_trailer : bool ref +val header_file : string ref +val header_file_spec : bool ref +val footer_file : string ref +val footer_file_spec : bool ref +val quiet : bool ref +val light : bool ref +val gallina : bool ref +val short : bool ref +val index : bool ref +val multi_index : bool ref +val index_name : string ref +val toc : bool ref +val page_title : string ref +val title : string ref +val externals : bool ref +val coqlib : string ref +val coqlib_path : string ref +val raw_comments : bool ref +val parse_comments : bool ref +val plain_comments : bool ref +val toc_depth : int option ref +val lib_name : string ref +val lib_subtitles : bool ref +val interpolate : bool ref +val inline_notmono : bool ref +val charset : string ref +val inputenc : string ref +val latin1 : bool ref +val utf8 : bool ref +val set_latin1 : unit -> unit +val set_utf8 : unit -> unit +type coq_module = string +type file = Vernac_file of string * coq_module | Latex_file of string |