in lean/scripts/lint_style.py [0:0]
def skip_string(enumerate_lines):
in_string = False
in_comment = False
for line_nr, line in enumerate_lines:
# ignore comment markers inside string literals
if not in_string:
if "/-" in line:
in_comment = True
if "-/" in line:
in_comment = False
# ignore quotes inside comments
if not in_comment:
# crude heuristic: if the number of non-escaped quote signs is odd,
# we're starting / ending a string literal
if line.count("\"") - line.count("\\\"") % 2 == 1:
in_string = not in_string
# if there are quote signs in this line,
# a string literal probably begins and / or ends here,
# so we skip this line
if line.count("\"") > 0:
continue
if in_string:
continue
yield line_nr, line