Commit 39af7f8b authored by Robbert Krebbers's avatar Robbert Krebbers

Also treat 009-013 as whitespace in the intro patterns parsers.

That range includes tabs and new lines.

Thanks Morten for spotting this problem.
parent 95cee475
......@@ -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.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment