From 6b041a242607ec906fbab451e53c15af6339e4ef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 May 2017 07:31:36 +0200 Subject: [emacs] [toplevel] Make emacs flag local to the toplevel. We remove the emacs-specific printing code from the core of Coq, now `-emacs` is a printing flag controlled by the toplevel. --- printing/printer.mli | 13 ------------- 1 file changed, 13 deletions(-) (limited to 'printing/printer.mli') diff --git a/printing/printer.mli b/printing/printer.mli index 24107394e..3fce06561 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -169,19 +169,6 @@ val pr_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map -> val pr_prim_rule : prim_rule -> std_ppcmds -(** Emacs/proof general support - (emacs_str s) outputs - - s if emacs mode, - - nothing otherwise. - This function was previously used to insert special chars like - [(String.make 1 (Char.chr 253))] to parenthesize sub-parts of the - proof context for proof by pointing. This part of the code is - removed for now because it interacted badly with utf8. We may put - it back some day using some xml-like tags instead of special - chars. See for example the tag in the prompt when in - emacs mode. *) -val emacs_str : string -> string - (** Backwards compatibility *) val prterm : constr -> std_ppcmds (** = pr_lconstr *) -- cgit v1.2.3