···

       
71
       
71
       
 
       
    let add_text text =

     

       
72
       
72
       
 
       
      let trimmed = String.trim text in

     

       
73
       
73
       
 
       
      if trimmed <> "" then begin

     

       
74
       
74
       
-
       
        (* Add space if needed and last char isn't already whitespace *)

     

       
75
       
75
       
-
       
        if !need_space then begin

     

       
74
       
74
       
+
       
        (* Check if text starts with punctuation that shouldn't have space before it *)

     

       
75
       
75
       
+
       
        let starts_with_punctuation =

     

       
76
       
76
       
+
       
          String.length trimmed > 0 &&

     

       
77
       
77
       
+
       
          (match trimmed.[0] with

     

       
78
       
78
       
+
       
          | ',' | '.' | ';' | ':' | '!' | '?' | ')' | ']' | '}' -> true

     

       
79
       
79
       
+
       
          | _ -> false)

     

       
80
       
80
       
+
       
        in

     

       
81
       
81
       
+
       


     

       
82
       
82
       
+
       
        (* Add space if needed, unless we're before punctuation *)

     

       
83
       
83
       
+
       
        if !need_space && not starts_with_punctuation then begin

     

       
76
       
84
       
 
       
          match last_char () with

     

       
77
       
85
       
 
       
          | Some (' ' | '\n') -> ()

     

       
78
       
86
       
 
       
          | _ -> Buffer.add_char buffer ' '