Fix #46

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 <value>'
 
@@ -86,7 +87,13 @@ def parse_value(xml):
         return ''.join(xml.itertext())
 
 def parse_error(xml):
-    return ET.fromstring(re.sub(r"<state_id val=\"\d+\" />", '', 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,13 +186,19 @@ 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:
                     vp = parse_response(valueNode)
                     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

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)