diff --git a/autoload/coqtop.py b/autoload/coqtop.py index 8d35600..2194bb4 100644 --- a/autoload/coqtop.py +++ b/autoload/coqtop.py @@ -7,7 +7,7 @@ from collections import deque, namedtuple Ok = namedtuple('Ok', ['val', 'msg']) -Err = namedtuple('Err', ['err']) +Err = namedtuple('Err', ['err', 'loc_s', 'loc_e']) Inl = namedtuple('Inl', ['val']) Inr = namedtuple('Inr', ['val']) @@ -29,8 +29,9 @@ def parse_response(xml): if xml.get('val') == 'good': return Ok(parse_value(xml[0]), None) elif xml.get('val') == 'fail': - print('err: %s' % ET.tostring(xml)) - return Err(parse_error(xml)) + # Don't print the error immediately : let the caller decide wether + # it must be printed and in which way + return parse_error(xml) else: assert False, 'expected "good" or "fail" in ' @@ -86,7 +87,13 @@ def parse_value(xml): return ''.join(xml.itertext()) def parse_error(xml): - return ET.fromstring(re.sub(r"", '', ET.tostring(xml))) + print(xml) + loc_s = xml.get('loc_s') + loc_e = xml.get('loc_e') + if loc_s is not None: + return Err('Err: ' + loc_s + ' to ' + loc_e, int(loc_s), int(loc_e)) + else: + return Err('Err: invalid', None, None) def build(tag, val=None, children=()): attribs = {'val': val} if val is not None else {} @@ -179,6 +186,9 @@ def get_answer(): messageNode = messageNode + "\n\n" + parse_value(c[2]) else: messageNode = parse_value(c[2]) + # Extract messages from feedbacks to handle errors + if c.tag == 'feedback' and c[1].get('val') == 'message': + messageNode = parse_value(c[1][0][2]) if shouldWait: continue else: @@ -186,6 +196,9 @@ def get_answer(): if messageNode is not None: if isinstance(vp, Ok): return Ok(vp.val, messageNode) + elif isinstance(vp, Err): + # Override error message : coq provides one + return Err(messageNode, vp.loc_s, vp.loc_e) return vp except ET.ParseError: continue diff --git a/autoload/coquille.py b/autoload/coquille.py index 67e54f3..dfc04b0 100644 --- a/autoload/coquille.py +++ b/autoload/coquille.py @@ -78,7 +78,7 @@ def coq_rewind(steps=1): if isinstance(response, CT.Ok): encountered_dots = encountered_dots[:len(encountered_dots) - steps] else: - info_msg = "[COQUILLE ERROR] Unexpected answer:\n\n%s" % response + info_msg = "[COQUILLE ERROR] Unexpected answer:\n\n%s" % response.err refresh() @@ -154,8 +154,7 @@ def coq_raw_query(*args): if response.msg is not None: info_msg = response.msg elif isinstance(response, CT.Err): - info_msg = response.err.text - print("FAIL") + info_msg = response.err else: print("(ANOMALY) unknown answer: %s" % ET.tostring(response)) # ugly @@ -198,8 +197,13 @@ def show_goal(): print('ERROR: the Coq process died') return - if response.msg is not None: - info_msg = response.msg + if isinstance(response, CT.Ok): + if response.msg is not None: + info_msg = response.msg + elif isinstance(response, CT.Err): + if response.err is not None: + info_msg = response.err + return if response.val.val is None: buff.append('No goals.') @@ -335,12 +339,10 @@ def send_until_fail(): else: send_queue.clear() if isinstance(response, CT.Err): - response = response.err - info_msg = response.text - loc_s = response.get('loc_s') + info_msg = response.err + loc_s = response.loc_s if loc_s is not None: - loc_s = int(loc_s) - loc_e = int(response.get('loc_e')) + loc_e = response.loc_e (l, c) = message_range['start'] (l_start, c_start) = _pos_from_offset(c, message, loc_s) (l_stop, c_stop) = _pos_from_offset(c, message, loc_e)