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

@@ -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.
 

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 [] "".
 

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 [] "".
 

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 [] "".