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

10 files changed, 20 insertions, 40 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index b2671e5b6..6a3b7a426 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -87,7 +87,6 @@ let in_toplevel = ref false
 
 let profile = false
 
-let print_emacs = ref false
 let xml_export = ref false
 
 let ide_slave = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 7ce808041..e2cf09474 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -13,7 +13,9 @@
 val boot : bool ref
 val load_init : bool ref
 
+(* Will affect STM caching *)
 val batch_mode : bool ref
+
 type compilation_mode = BuildVo | BuildVio | Vio2Vo
 val compilation_mode : compilation_mode ref
 val compilation_output_name : string option ref
@@ -56,8 +58,6 @@ val profile : bool
 
 (* Legacy flags *)
 
-(* -emacs option: printing includes emacs tags, will affect stm caching. *)
-val print_emacs : bool ref
 (* -xml option: xml hooks will be called *)
 val xml_export : bool ref
 
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 *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 259e96a27..91e6dc4ab 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -188,8 +188,6 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
       (fun hypl -> List.subtract cmp hypl oldhyps)
       hyps
   in
-  let emacs_str s =
-    if !Flags.print_emacs then s else "" in
   let s = 
     let frst = ref true in
     List.fold_left
@@ -199,9 +197,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
 	   "" lh))
     "" newhyps in
   Feedback.msg_notice
-    (str (emacs_str "<infoH>")
+    (str "<infoH>"
       ++  (hov 0 (str s))
-      ++  (str (emacs_str "</infoH>")));
+      ++  (str "</infoH>"));
   tclIDTAC goal;;
 
 
diff --git a/stm/stm.ml b/stm/stm.ml
index b98cb312e..2057496f4 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -66,7 +66,7 @@ end
 
 (* During interactive use we cache more states so that Undoing is fast *)
 let interactive () =
-  if !Flags.ide_slave || !Flags.print_emacs || not !Flags.batch_mode then `Yes
+  if !Flags.ide_slave || not !Flags.batch_mode then `Yes
   else `No
 
 let async_proofs_workers_extra_env = ref [||]
@@ -1094,7 +1094,7 @@ end = struct (* {{{ *)
           VtStm (VtBack oid, true), VtLater
       | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
-          VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
+          VtStm (VtBack (Stateid.of_int id), not !Flags.batch_mode), VtNow
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index 8acfed5d0..ca56f032f 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -8,5 +8,3 @@ subgoal 2 (ID 35) is:
  1 = S (S m')
 subgoal 3 (ID 22) is:
  S (S n') = S m
-
-(dependent evars: (printing disabled) )
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index ab5104c78..8806c7356 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -8,6 +8,8 @@
 
 open Pp
 
+let print_emacs = ref false
+
 let top_stderr x =
   Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x
 
@@ -45,9 +47,8 @@ let resynch_buffer ibuf =
 
 (* emacs special prompt tag for easy detection. No special character,
    to avoid interfering with utf8. Compatibility code removed. *)
-
-let emacs_prompt_startstring() = Printer.emacs_str "<prompt>"
-let emacs_prompt_endstring() = Printer.emacs_str "</prompt>"
+let emacs_prompt_startstring () = if !print_emacs then "<prompt>"  else ""
+let emacs_prompt_endstring   () = if !print_emacs then "</prompt>" else ""
 
 (* Read a char in an input channel, displaying a prompt at every
    beginning of line. *)
@@ -56,7 +57,7 @@ let prompt_char ic ibuf count =
     | ll::_ -> Int.equal ibuf.len ll
     | [] -> Int.equal ibuf.len 0
   in
-  if bol && not !Flags.print_emacs then top_stderr (str (ibuf.prompt()));
+  if bol && not !print_emacs then top_stderr (str (ibuf.prompt()));
   try
     let c = input_char ic in
     if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -168,7 +169,7 @@ let error_info_for_buffer ?loc buf =
 (* Actual printing routine *)
 let print_error_for_buffer ?loc lvl msg buf =
   let pre_hdr = error_info_for_buffer ?loc buf in
-  if !Flags.print_emacs
+  if !print_emacs
   then Topfmt.emacs_logger ?pre_hdr lvl msg
   else Topfmt.std_logger   ?pre_hdr lvl msg
 
@@ -207,7 +208,7 @@ let make_emacs_prompt() =
       (fun acc x -> acc ^ (if CString.is_empty acc then "" else "|") ^ Names.Id.to_string x)
       "" pending in
   let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
-  if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
+  if !print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
   else ""
 
 (* A buffer to store the current command read on stdin. It is
@@ -299,7 +300,7 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
 
 let do_vernac sid =
   top_stderr (fnl());
-  if !Flags.print_emacs then top_stderr (str (top_buffer.prompt()));
+  if !print_emacs then top_stderr (str (top_buffer.prompt()));
   resynch_buffer top_buffer;
   try
     let input = (top_buffer.tokens, None) in
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 13e860a88..a0e2f1e02 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -8,6 +8,9 @@
 
 (** The Coq toplevel loop. *)
 
+(** -emacs option: printing includes emacs tags. *)
+val print_emacs : bool ref
+
 (** A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 7834b5113..26ee413fb 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -246,21 +246,21 @@ let compile_files () =
 let set_emacs () =
   if not (Option.is_empty !toploop) then
     user_err Pp.(str "Flag -emacs is incompatible with a custom toplevel loop");
-  Flags.print_emacs := true;
+  Coqloop.print_emacs := true;
   Printer.enable_goal_tags_printing := true;
   color := `OFF
 
 (** Options for CoqIDE *)
 
 let set_ideslave () =
-  if !Flags.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible");
+  if !Coqloop.print_emacs then user_err Pp.(str "Flags -ideslave and -emacs are incompatible");
   toploop := Some "coqidetop";
   Flags.ide_slave := true
 
 (** Options for slaves *)
 
 let set_toploop name =
-  if !Flags.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible");
+  if !Coqloop.print_emacs then user_err Pp.(str "Flags -toploop and -emacs are incompatible");
   toploop := Some name
 
 (** GC tweaking *)