[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.

2 files changed, 0 insertions, 19 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index ebe68680f..3c31dd96b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -26,9 +26,6 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
-let emacs_str s =
-  if !Flags.print_emacs then s else ""
-
 let get_current_context () =
   Pfedit.get_current_context ()
 
@@ -656,9 +653,6 @@ let print_dependent_evars gl sigma seeds =
     in
     cut () ++ cut () ++
     str "(dependent evars:" ++ evars ++ str ")"
-    else if !Flags.print_emacs then
-      (* IDEs prefer something dummy instead of nothing *)
-      cut () ++ cut () ++ str "(dependent evars: (printing disabled) )"
     else mt ()
   in
   constraints ++ evars ()
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 *)