Skip to content

Commit

Permalink
Parse <message> node correctly
Browse files Browse the repository at this point in the history
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>
  • Loading branch information
WangNan0 committed Dec 21, 2017
1 parent efc4fe5 commit 6d5ef3d
Showing 1 changed file with 10 additions and 2 deletions.
12 changes: 10 additions & 2 deletions autoload/coqtop.py
Original file line number Diff line number Diff line change
Expand Up @@ -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 = ''
Expand All @@ -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:
Expand Down

0 comments on commit 6d5ef3d

Please sign in to comment.