bug#27761: Crash while using proof-general/company-coq on OS X

[YAMAMOTO Mitsuharu]

>>>>> On Thu, 03 Aug 2017 19:18:20 +0300, Eli Zaretskii <eliz@gnu.org> said:

>> The recent post on gdb session implies it has something to do with
>> the string " 163" and overlays.  The key point to reproduce it was
>> to turn on linum-mode.  Without linum-mode, the above procedure did
>> not crash.

> Yes, I guess 163 is the line number?

I think so, too.  On my environment, it->object (and it->string) is a
Lisp string " 164".  The value of it->current.pos.charpos is 4139
rather than OP's 4138.  Perhaps the text is slightly different.

> The problem has to do with something that prevents the display
> engine to pop the iterator state from the stack when it reaches the
> end of a Lisp string (" 163") which it needs to display.  I'm trying
> to understand why this happens, my guess is that some condition
> somewhere is not working as expected, perhaps because the display of
> the string specifies padding with blanks (or so it seems).

I noticed that if I turn off prettify-symbol-mode, then it does not
crash.  Attached are the screenshots with and without
prettify-symbol-mode: the former crashes and the latter does not.  The
original contents of Line 164 is

forall T1, 1 <= size_typ T1.

and the strings "forall" and "<=" are composed by the following
prettify-symbols-alist value:

(("|-" . 8866)
 ("||" . 8214)
 ("/\\" . 8743)
 ("\\/" . 8744)
 ("->" . 8594)
 ("<-" . 8592)
 ("<->" . 8596)
 ("=>" . 8658)
 ("<=" . 8804)
 (">=" . 8805)
 ("<>" . 8800)
 ("True" . 8868)
 ("False" . 8869)
 ("fun" . 955)
 ("forall" . 8704)
 ("exists" . 8707)
 ("nat" . 8469)
 ("Prop" . 8473)
 ("Real" . 8477)
 ("bool" . 120121)
 (">->" . 8611)
 ("-->" . 10230)
 ("<--" . 10229)
 ("<-->" . 10231)
 ("==>" . 10233)
 ("<==" . 10232)
 ("~~>" . 10239)
 ("<~~" . 11059))

                             YAMAMOTO Mitsuharu
                        mituharu@math.s.chiba-u.ac.jp