Quelle common.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* Misc types **********************************************************************)
type target_language = LaTeX | HTML | TeXmacs | Raw
type output_t = StdOut | MultFiles | File of string
type coq_module = string
type file_t = Vernac_file of string * coq_module | Latex_file of string
type glob_source_t = NoGlob | DotGlob | GlobFile of string
type encoding_t = {
  charset : string;
  inputenc : string;
  latin1 : bool;
  utf8 : bool;
}
type otype = Dvi | Ps | Pdf
(* End misc types ******************************************************************)

(** User-setable options from command line [coqdoc] arugments **********************)
type t = {
  targetlang : target_language;
  coqlib : string option;
  compile_targets : otype list;
  out_to : output_t;
  output_dir: string;
  gallina: bool;
  short : bool;
  light : bool;
  title : string;
  header_trailer : bool;
  header_file_spec : bool;
  header_file : string;
  footer_file_spec : bool;
  footer_file : string;
  index: bool;
  binder_index : bool;
  multi_index : bool;
  index_name : string;
  toc: bool;
  files : file_t list;
  glob_source : glob_source_t;
  quiet : bool;
  externals : bool;
  coqlib_url: string;
  paths : (string * string) list;
  encoding : encoding_t;
  interpolate : bool;
  raw_comments : bool;
  parse_comments : bool;
  plain_comments : bool;
  toc_depth : int option;
  lib_name : string;
  lib_subtitles : bool;
  inline_notmono : bool;
}

let default : t = {
  targetlang = HTML;
  coqlib = None;
  compile_targets = [];
  out_to = MultFiles;
  output_dir = "";
  gallina = false;
  short = false;
  light = false;
  title = "";
  header_trailer = true;
  header_file_spec = false;
  header_file = "";
  footer_file_spec = false;
  footer_file = "";
  index = true;
  multi_index = false;
  index_name = "index";
  binder_index = false;
  toc = false;
  files = [];
  glob_source = DotGlob;
  quiet = true;
  externals = true;
  coqlib_url = Coq_config.wwwstdlib;
  paths = [];
  encoding = {
    charset = "iso-8859-1";
    inputenc = "";
    latin1 = false;
    utf8 = false;
  };
  interpolate = false;
  raw_comments = false;
  parse_comments = false;
  plain_comments = false;
  toc_depth = None;
  lib_name = "Library";
  lib_subtitles = false;
  inline_notmono = false;
}

let prefs = ref default

(* Globals *************************************************************************)
let page_title = ref ""
let out_channel = ref stdout
(* End globals *********************************************************************)

(* Little helpers ******************************************************************)
let (/) = Filename.concat

let coqdoc_out f =
  if !prefs.output_dir <> "" && Filename.is_relative f then
    if not (Sys.file_exists !prefs.output_dir) then
      (Printf.eprintf "No such directory: %s\n" !prefs.output_dir; exit 1)
    else
      !prefs.output_dir / f
  else
    f

let open_out_file f =
  out_channel :=
    try open_out (coqdoc_out f)
    with Sys_error s -> Printf.eprintf "%s\n" s; exit 1

let close_out_file () = close_out !out_channel
(* End little helpers **************************************************************)

quality99%

¤ Dauer der Verarbeitung: 0.5 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.