diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-18 07:31:36 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-01 15:50:26 +0200 |
| commit | 6b041a242607ec906fbab451e53c15af6339e4ef (patch) | |
| tree | ac7b4e6a25c0607c1770da551ed4f5de4addb310 /printing/printer.mli | |
| parent | f3a388baf9cf2a14a658cab77554a0802b999486 (diff) | |
[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.
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 13 |
1 files changed, 0 insertions, 13 deletions
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 <prompt> tag in the prompt when in - emacs mode. *) -val emacs_str : string -> string - (** Backwards compatibility *) val prterm : constr -> std_ppcmds (** = pr_lconstr *) |