From 91ee24b4a7843793a84950379277d92992ba1651 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 11 Feb 2016 02:13:30 +0100 Subject: Feedback cleanup This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work. --- toplevel/metasyntax.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'toplevel/metasyntax.ml') diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index d60c73939..52117f13f 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -568,7 +568,7 @@ let is_not_small_constr = function let rec define_keywords_aux = function | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l when is_not_small_constr e -> - Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); + Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | n :: l -> n :: define_keywords_aux l @@ -577,7 +577,7 @@ let rec define_keywords_aux = function (* Ensure that IDENT articulation terminal symbols are keywords *) let define_keywords = function | GramConstrTerminal(IDENT k)::l -> - Flags.if_verbose msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); + Flags.if_verbose Feedback.msg_info (str "Identifier '" ++ str k ++ str "' now a keyword"); CLexer.add_keyword k; GramConstrTerminal(KEYWORD k) :: define_keywords_aux l | l -> define_keywords_aux l @@ -855,12 +855,12 @@ let check_rule_productivity l = let is_not_printable onlyparse noninjective = function | NVar _ -> let () = if not onlyparse then - msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.") + Feedback.msg_warning (strbrk "This notation will not be used for printing as it is bound to a single variable.") in true | _ -> if not onlyparse && noninjective then - let () = msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in + let () = Feedback.msg_warning (strbrk "This notation will not be used for printing as it is not reversible.") in true else onlyparse @@ -886,7 +886,7 @@ let find_precedence lev etyps symbols = | ETName | ETBigint | ETReference -> begin match lev with | None -> - ([msg_info,strbrk "Setting notation at level 0."],0) + ([Feedback.msg_info,strbrk "Setting notation at level 0."],0) | Some 0 -> ([],0) | _ -> @@ -904,7 +904,7 @@ let find_precedence lev etyps symbols = else [],Option.get lev) | Terminal _ when last_is_terminal () -> if Option.is_empty lev then - ([msg_info,strbrk "Setting notation at level 0."], 0) + ([Feedback.msg_info,strbrk "Setting notation at level 0."], 0) else [],Option.get lev | _ -> if Option.is_empty lev then error "Cannot determine the level."; @@ -931,7 +931,7 @@ let remove_curly_brackets l = (match next' with | Terminal "}" as t2 :: l'' as l1 -> if not (List.equal Notation.symbol_eq l l0) || not (List.equal Notation.symbol_eq l' l1) then - msg_warning (strbrk "Skipping spaces inside curly brackets"); + Feedback.msg_warning (strbrk "Skipping spaces inside curly brackets"); if deb && List.is_empty l'' then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' @@ -976,7 +976,7 @@ let compute_pure_syntax_data df mods = let (msgs,(onlyparse,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in let msgs = if onlyparse then - (msg_warning, + (Feedback.msg_warning, strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs else msgs in msgs, sy_data, extra -- cgit v1.2.3