diff options
| -rw-r--r-- | .travis.yml | 3 | ||||
| -rw-r--r-- | dev/include | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 18 | ||||
| -rw-r--r-- | lib/terminal.ml | 12 | ||||
| -rw-r--r-- | lib/terminal.mli | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 8 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 51 | ||||
| -rw-r--r-- | vernac/topfmt.mli | 4 |
8 files changed, 77 insertions, 25 deletions
diff --git a/.travis.yml b/.travis.yml index d2d779d8ba..6de63d387b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -145,6 +145,9 @@ matrix: - brew update - brew install opam +before_install: +- if [ "${TRAVIS_PULL_REQUEST}" != "false" ]; then echo "Tested commit (followed by parent commits):"; git log -1; for commit in `git log -1 --format="%P"`; do echo; git log -1 $commit; done; fi + install: - opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) diff --git a/dev/include b/dev/include index 31ae5da71a..0d34595f4f 100644 --- a/dev/include +++ b/dev/include @@ -31,6 +31,7 @@ #install_printer (* glob_constr *) ppglob_constr;; #install_printer (* open constr *) ppopenconstr;; #install_printer (* constr *) ppconstr;; +#install_printer (* econstr *) ppeconstr;; #install_printer (* constr_substituted *) ppsconstr;; #install_printer (* constraints *) ppconstraints;; #install_printer (* univ constraints *) ppuniverseconstraints;; diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index f338c30551..713f344cbe 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -705,20 +705,20 @@ when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}: This command can be seen as a generalization of {\tt Fixpoint}. It is actually a wrapper for several ways of defining a function \emph{and other useful related objects}, namely: an induction principle that reflects the -recursive structure of the function (see \ref{FunInduction}), and its +recursive structure of the function (see \ref{FunInduction}) and its fixpoint equality. The meaning of this declaration is to define a function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be -given (unless the function is not recursive), but it must not -necessary be \emph{structurally} decreasing. The point of the {\tt +given (unless the function is not recursive), but it might not +necessarily be \emph{structurally} decreasing. The point of the {\tt \{\}} annotation is to name the decreasing argument \emph{and} to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. -The {\tt Function} construction enjoys also the {\tt with} extension +The {\tt Function} construction also enjoys the {\tt with} extension to define mutually recursive definitions. However, this feature does -not work for non structural recursive functions. % VRAI?? +not work for non structurally recursive functions. % VRAI?? See the documentation of {\tt functional induction} (see Section~\ref{FunInduction}) and {\tt Functional Scheme} @@ -749,7 +749,7 @@ Function plus (n m : nat) {struct n} : nat := \end{coq_example*} \paragraph[Limitations]{Limitations\label{sec:Function-limitations}} -\term$_0$ must be build as a \emph{pure pattern-matching tree} +\term$_0$ must be built as a \emph{pure pattern-matching tree} (\texttt{match...with}) with applications only \emph{at the end} of each branch. @@ -776,7 +776,7 @@ For now dependent cases are not treated for non structurally terminating functio The generation of the graph relation \texttt{(R\_\ident)} used to compute the induction scheme of \ident\ raised a typing error. Only - the ident is defined, the induction scheme will not be generated. + the ident is defined; the induction scheme will not be generated. This error happens generally when: @@ -848,14 +848,14 @@ the following: being the decreasing argument and \term$_1$ being a function from type of \ident$_0$ to \texttt{nat} for which value on the decreasing argument decreases (for the {\tt lt} order on {\tt - nat}) at each recursive call of \term$_0$, parameters of the + nat}) at each recursive call of \term$_0$. Parameters of the function are bound in \term$_0$; \item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being the decreasing argument and \term$_1$ an ordering relation on the type of \ident$_0$ (i.e. of type T$_{\ident_0}$ $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which the decreasing argument decreases at each recursive call of - \term$_0$. The order must be well founded. parameters of the + \term$_0$. The order must be well founded. Parameters of the function are bound in \term$_0$. \end{itemize} diff --git a/lib/terminal.ml b/lib/terminal.ml index 3b6e34f0b8..34efddfbca 100644 --- a/lib/terminal.ml +++ b/lib/terminal.ml @@ -35,6 +35,8 @@ type style = { italic : bool option; underline : bool option; negative : bool option; + prefix : string option; + suffix : string option; } let set o1 o2 = match o1 with @@ -51,9 +53,11 @@ let default = { italic = None; underline = None; negative = None; + prefix = None; + suffix = None; } -let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style () = +let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style ?prefix ?suffix () = let st = match style with | None -> default | Some st -> st @@ -65,6 +69,8 @@ let make ?fg_color ?bg_color ?bold ?italic ?underline ?negative ?style () = italic = set st.italic italic; underline = set st.underline underline; negative = set st.negative negative; + prefix = set st.prefix prefix; + suffix = set st.suffix suffix; } let merge s1 s2 = @@ -75,6 +81,8 @@ let merge s1 s2 = italic = set s1.italic s2.italic; underline = set s1.underline s2.underline; negative = set s1.negative s2.negative; + prefix = set s1.prefix s2.prefix; + suffix = set s1.suffix s2.suffix; } let base_color = function @@ -168,6 +176,8 @@ let reset_style = { italic = Some false; underline = Some false; negative = Some false; + prefix = None; + suffix = None; } let has_style t = diff --git a/lib/terminal.mli b/lib/terminal.mli index dbc418dd6a..b1b76e6e2a 100644 --- a/lib/terminal.mli +++ b/lib/terminal.mli @@ -35,11 +35,14 @@ type style = { italic : bool option; underline : bool option; negative : bool option; + prefix : string option; + suffix : string option; } val make : ?fg_color:color -> ?bg_color:color -> ?bold:bool -> ?italic:bool -> ?underline:bool -> - ?negative:bool -> ?style:style -> unit -> style + ?negative:bool -> ?style:style -> + ?prefix:string -> ?suffix:string -> unit -> style (** Create a style from the given flags. It is derived from the optional [style] argument if given. *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 8c394316e9..08c2350237 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -58,16 +58,18 @@ let init_color () = match colors with | None -> (** Default colors *) - Topfmt.init_color_output () + Topfmt.init_terminal_output ~color:true | Some "" -> (** No color output *) - () + Topfmt.init_terminal_output ~color:false | Some s -> (** Overwrite all colors *) Topfmt.clear_styles (); Topfmt.parse_color_config s; - Topfmt.init_color_output () + Topfmt.init_terminal_output ~color:true end + else + Topfmt.init_terminal_output ~color:false let toploop_init = ref begin fun x -> let () = init_color () in diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index b3810f7d53..e7b14309d1 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -149,7 +149,7 @@ let gen_logger dbg warn ?pre_hdr level msg = match level with (** Standard loggers *) (* We provide a generic clear_log_backend callback for backends - wanting to do clenaup after the print. + wanting to do cleanup after the print. *) let std_logger_cleanup = ref (fun () -> ()) @@ -207,6 +207,8 @@ let make_style_stack () = italic = Some false; underline = Some false; negative = Some false; + prefix = None; + suffix = None; }) in let style_stack = ref [] in @@ -235,20 +237,49 @@ let make_style_stack () = let clear () = style_stack := [] in push, pop, clear -let init_color_output () = +let make_printing_functions () = + let empty = Terminal.make () in + let print_prefix ft tag = + let style = + try CString.Map.find tag !tag_map + with | Not_found -> empty + in + match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () + in + let print_suffix ft tag = + let style = + try CString.Map.find tag !tag_map + with | Not_found -> empty + in + match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () + in + print_prefix, print_suffix + +let init_terminal_output ~color = init_tag_map (default_tag_map ()); let push_tag, pop_tag, clear_tag = make_style_stack () in - std_logger_cleanup := clear_tag; - let tag_handler = { + let print_prefix, print_suffix = make_printing_functions () in + let tag_handler ft = { Format.mark_open_tag = push_tag; Format.mark_close_tag = pop_tag; - Format.print_open_tag = ignore; - Format.print_close_tag = ignore; + Format.print_open_tag = print_prefix ft; + Format.print_close_tag = print_suffix ft; } in - Format.pp_set_mark_tags !std_ft true; - Format.pp_set_mark_tags !err_ft true; - Format.pp_set_formatter_tag_functions !std_ft tag_handler; - Format.pp_set_formatter_tag_functions !err_ft tag_handler + if color then + (* Use 0-length markers *) + begin + std_logger_cleanup := clear_tag; + Format.pp_set_mark_tags !std_ft true; + Format.pp_set_mark_tags !err_ft true + end + else + (* Use textual markers *) + begin + Format.pp_set_print_tags !std_ft true; + Format.pp_set_print_tags !err_ft true + end; + Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft); + Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft) (* Rules for emacs: - Debug/info: emacs_quote_info diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 0e781bcc1b..6e006fc6c9 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -41,11 +41,13 @@ val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit (** Color output *) -val init_color_output : unit -> unit val clear_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list +(** Initialization of interpretation of tags *) +val init_terminal_output : color:bool -> unit + (** Error printing *) (* To be deprecated when we can fully move to feedback-based error printing. *) |