From 44a220a9b4eeace88286b1aac6270ffb313d69b4 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.
---
 prelude/strings.v          | 10 ++++++++--
 proofmode/intro_patterns.v |  5 +++--
 proofmode/sel_patterns.v   |  5 +++--
 proofmode/spec_patterns.v  |  5 +++--
 4 files changed, 17 insertions(+), 8 deletions(-)

diff --git a/prelude/strings.v b/prelude/strings.v
index acf0c2c46..3064d39d8 100644
--- a/prelude/strings.v
+++ b/prelude/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.
 
diff --git a/proofmode/intro_patterns.v b/proofmode/intro_patterns.v
index bbb58d62a..b999e0be3 100644
--- a/proofmode/intro_patterns.v
+++ b/proofmode/intro_patterns.v
@@ -54,7 +54,6 @@ Fixpoint cons_name (kn : string) (k : list token) : list token :=
 Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   match s with
   | "" => rev (cons_name kn k)
-  | String " " s => tokenize_go s (cons_name kn k) ""
   | String "?" s => tokenize_go s (TAnom :: cons_name kn k) ""
   | String "_" s => tokenize_go s (TDrop :: cons_name kn k) ""
   | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
@@ -75,7 +74,9 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_name kn k) ""
   | String "*" (String "*" s) => tokenize_go s (TAll :: cons_name kn k) ""
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
-  | String a s => tokenize_go s k (String a kn)
+  | String a s =>
+     if is_space a then tokenize_go s (cons_name kn k) ""
+     else tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
diff --git a/proofmode/sel_patterns.v b/proofmode/sel_patterns.v
index 75aa2ee49..4a77f4f08 100644
--- a/proofmode/sel_patterns.v
+++ b/proofmode/sel_patterns.v
@@ -20,14 +20,15 @@ Fixpoint cons_name (kn : string) (k : list sel_pat) : list sel_pat :=
 Fixpoint parse_go (s : string) (k : list sel_pat) (kn : string) : list sel_pat :=
   match s with
   | "" => rev (cons_name kn k)
-  | String " " s => parse_go s (cons_name kn k) ""
   | String "%" s => parse_go s (SelPure :: cons_name kn k) ""
   | String "#" s => parse_go s (SelPersistent :: cons_name kn k) ""
   | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
       (String (Ascii.Ascii false false false true false false false true)
       (String (Ascii.Ascii true true true false true false false true) s)) =>
      parse_go s (SelSpatial :: cons_name kn k) ""
-  | String a s => parse_go s k (String a kn)
+  | String a s =>
+     if is_space a then parse_go s (cons_name kn k) ""
+     else parse_go s k (String a kn)
   end.
 Definition parse (s : string) : list sel_pat := parse_go s [] "".
 
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index 4f9cbada3..25c548311 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -31,7 +31,6 @@ Fixpoint cons_name (kn : string) (k : list token) : list token :=
 Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   match s with
   | "" => rev (cons_name kn k)
-  | String " " s => tokenize_go s (cons_name kn k) ""
   | String "-" s => tokenize_go s (TMinus :: cons_name kn k) ""
   | String "[" s => tokenize_go s (TBracketL :: cons_name kn k) ""
   | String "]" s => tokenize_go s (TBracketR :: cons_name kn k) ""
@@ -40,7 +39,9 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
   | String ">" s => tokenize_go s (TModal :: cons_name kn k) ""
   | String "$" s => tokenize_go s (TFrame :: cons_name kn k) ""
-  | String a s => tokenize_go s k (String a kn)
+  | String a s =>
+     if is_space a then tokenize_go s (cons_name kn k) ""
+     else tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
 
-- 
GitLab