From 39af7f8b72d51b5690dae39a7b87d5ad6a5a4005 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 19 Nov 2016 01:47:55 +0100
Subject: [PATCH] Also treat 009-013 as whitespace in the intro patterns
 parsers.

That range includes tabs and new lines.

Thanks Morten for spotting this problem.
---
 theories/strings.v | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/theories/strings.v b/theories/strings.v
index ea8f5402..f08e9b0a 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -31,11 +31,17 @@ Fixpoint string_rev_app (s1 s2 : string) : string :=
 Definition string_rev (s : string) : string := string_rev_app s "".
 
 (* Break a string up into lists of words, delimited by white space *)
+Definition is_space (x : Ascii.ascii) : bool :=
+  match x with
+  | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
+  end%char.
+
 Fixpoint words_go (cur : option string) (s : string) : list string :=
   match s with
   | "" => option_list (string_rev <$> cur)
-  | String " " s => option_list (string_rev <$> cur) ++ words_go None s
-  | String a s => words_go (Some (default (String a "") cur (String a))) s
+  | String a s =>
+     if is_space a then option_list (string_rev <$> cur) ++ words_go None s
+     else words_go (Some (default (String a "") cur (String a))) s
   end.
 Definition words : string → list string := words_go None.
 
-- 
GitLab