From ea3ed5f666080d072ae3f1ec4811531b54bc4c9e Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 16 Oct 2003 15:52:35 +0000
Subject: translator avoids printing a . followed by a ( by inserting a space

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4655 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernac.ml | 22 ++++++++++++++++++----
 1 file changed, 18 insertions(+), 4 deletions(-)

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 00020a85a6..1308b7c701 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -99,12 +99,26 @@ let parse_phrase (po, verbch) =
 
 let just_parsing = ref false
 let chan_translate = ref stdout
+let last_char = ref '\000'
+
+let set_formatter_translator() =
+  let ch = !chan_translate in
+  let out s b e =
+    let n = e-b in
+    if n > 0 then begin
+      (match !last with
+          '.' -> if s.[b] = '(' then output ch " " 0 1 
+        | _ -> ());
+      last := s.[e-1]
+    end;
+    output ch s b e
+  in
+  Format.set_formatter_output_functions out (fun () -> flush ch);
+  Format.set_max_boxes max_int
+
 
 let pr_new_syntax loc ocom =
-  if !translate_file then begin
-    Format.set_formatter_out_channel !chan_translate;
-    Format.set_max_boxes max_int;
-  end;
+  if !translate_file then set_formatter_translator();
   let fs = States.freeze () in
   let com = match ocom with
     | Some (VernacV7only _) ->
-- 
cgit v1.2.3