From 6d5ef3d76cc91f3dca0ff7797b6c5b6c324119fb Mon Sep 17 00:00:00 2001
From: Wang Nan <wangnan0@huawei.com>
Date: Sun, 17 Dec 2017 23:17:38 +0800
Subject: [PATCH] Parse <message> node correctly

Message can be reported this way:

 <message>
   <message_level val="info"/>
   <string>mypred_Sx&nbsp;is&nbsp;defined</string>
 </message>

When recving message like this, python raise an exception
in get_answer() because accessing 'c[2]' is invalid in this case.

We should look for the exact node instead.

Signed-off-by: Wang Nan <wangnan0@huawei.com>
---
 autoload/coqtop.py | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/autoload/coqtop.py b/autoload/coqtop.py
index ef30396..6997bed 100644
--- a/autoload/coqtop.py
+++ b/autoload/coqtop.py
@@ -173,6 +173,14 @@ def escape(cmd):
               .replace("&#40;", '(') \
               .replace("&#41;", ')')
 
+# Extract <string> from a <message> element
+def parse_message(elt):
+    for e in elt:
+        if e.tag == 'string':
+            return parse_value(e)
+    # message without string?
+    return ''
+
 def get_answer():
     fd = coqtop.stdout.fileno()
     data = ''
@@ -192,9 +200,9 @@ def get_answer():
                         valueNode = c
                     if c.tag == 'message':
                         if messageNode is not None:
-                            messageNode = messageNode + "\n\n" + parse_value(c[2])
+                            messageNode = messageNode + "\n\n" + parse_message(c)
                         else:
-                            messageNode = parse_value(c[2])
+                            messageNode = parse_message(c)
                 if shouldWait:
                     continue
                 else: