From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 10 Jul 2014 17:05:45 +0000 (-0400)
Subject: reorganize friendlyparser, behavior unchanged
X-Git-Tag: cvc5-1.0.0~6701^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2cfbaa1de281ce0b85e2c7a6d058a05d940f5aaf;p=cvc5.git

reorganize friendlyparser, behavior unchanged
---

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index ca8f805b4..d72b311cb 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -400,32 +400,38 @@ std::string parseErrorHelper(const char* lineStart, int charPositionInLine, cons
         }
       }
     } else {
-      // go to nearest alphanumeric string (before current position),
-      // see if that word can be found in original message. If so,
-      // point to that, else keep pointer where it was.
-      int nearestWordEn = caretPos - 1;
-      while(nearestWordEn > 0 && !isSimpleChar(slice[nearestWordEn])) {
-        --nearestWordEn;
-      }
-      if(isSimpleChar(slice[nearestWordEn])) {
-        int nearestWordSt = nearestWordEn;
-        while(nearestWordSt > 0 && isSimpleChar(slice[nearestWordSt - 1])) {
-          --nearestWordSt;
+      bool foundCaretPos = false;
+
+      for(int tries = 0; tries < 1 && caretPos > 0 && !foundCaretPos; ++tries) {
+        // go to nearest alphanumeric string (before current position),
+        // see if that word can be found in original message. If so,
+        // point to that, else keep pointer where it was.
+        int nearestWordEn = caretPos - 1;
+        while(nearestWordEn > 0 && !isSimpleChar(slice[nearestWordEn])) {
+          --nearestWordEn;
         }
-        string word = slice.substr(nearestWordSt, (nearestWordEn - nearestWordSt + 1));
-        size_t matchLoc = wholeWordMatch(message, word, isSimpleChar);
-        Debug("friendlyparser") << "[friendlyparser] nearest word = " << word << std::endl;
-        Debug("friendlyparser") << "[friendlyparser] matchLoc = " << matchLoc << endl;
-        if( matchLoc != string::npos ) {
-          Debug("friendlyparser") << "[friendlyparser] strong evidence that caret should be at "
-                                  << nearestWordSt << std::endl;
+        if(isSimpleChar(slice[nearestWordEn])) {
+          int nearestWordSt = nearestWordEn;
+          while(nearestWordSt > 0 && isSimpleChar(slice[nearestWordSt - 1])) {
+            --nearestWordSt;
+          }
+          string word = slice.substr(nearestWordSt, (nearestWordEn - nearestWordSt + 1));
+          size_t matchLoc = wholeWordMatch(message, word, isSimpleChar);
+          Debug("friendlyparser") << "[friendlyparser] nearest word = " << word << std::endl;
+          Debug("friendlyparser") << "[friendlyparser] matchLoc = " << matchLoc << endl;
+          if( matchLoc != string::npos ) {
+            Debug("friendlyparser") << "[friendlyparser] strong evidence that caret should be at "
+                                    << nearestWordSt << std::endl;
+            foundCaretPos = true;
+          }
           caretPos = nearestWordSt;
-        } else {
-          // this doesn't look good. caret generally getting printed
-          // at unhelpful positions. improve upstream?
-          return message;
         }
       }
+      if( !foundCaretPos) {
+        // this doesn't look good. caret generally getting printed
+        // at unhelpful positions. improve upstream?
+        return message;
+      }
     }
     caretPos += caretPosExtra;
   }// end of caret position computation/heuristics