proofs: a token may start after a skipped literal in the postulate scan

scripts/check-agda.sh

@@ -92,7 +92,7 @@ printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \
   '{- postulate {- nested postulate -} postulate -}' \
   'x--postulate : Set₁' 'x--postulate = Set' \
   's : String' 's = "a postulate in a string \" still the string"' \
-  '{-# FOREIGN GHC postulate = () #-}' \
+  '{-# FOREIGN GHC postulate = () #-}' "c = 'x'-- postulate after a character literal" \
   > "$work/CommentsOnly.agda"
 # One planted postulate per line, 2 to 5: after a block comment; bounded by
 # NO-BREAK SPACE (U+00A0), which Agda reads as whitespace; separated from its

scripts/scan-postulates.sh

@@ -42,7 +42,9 @@ hits="$(LC_ALL=C awk -v ws="$ws" '
     code = ""; i = 1; n = length(line)
     while (i <= n) {
       c = substr(line, i, 1); two = substr(line, i, 2)
-      prev = (i > 1) ? substr(line, i - 1, 1) : ""
+      # The last character emitted as code, not the raw one before i: a skipped
+      # literal, comment or pragma leaves a space, so a token may start after it.
+      prev = (code == "") ? "" : substr(code, length(code), 1)
       if (pragma) {                        # inside {-# … #-}: skip to the first #-}
         if (substr(line, i, 3) == "#-}") { pragma = 0; i += 3; code = code " " } else i++
         continue