Currently, F* namespace arguments to --already_cached must be separated with spaces:

fstar.exe --already_cached '* -A +B -C' ...

This may cause issues in such Makefile rules as the following (found in LowParse or miTLS):

FSTAR_INCLUDES = $(QD_HOME)/src/lowparse $(KREMLIN_HOME)/kremlib
FSTAR_OPTIONS += --already_cached '* -A +B +C' $(addprefix --include ,$(FSTAR_INCLUDES))

%.fst-in %.fsti-in:
           echo $(FSTAR_OPTIONS)

This pull request solves (at least) this issue by allowing the user to write --already_cached *,-A,+B,+C above, replacing spaces with commas.

It works by replacing all spaces with commas, then splitting across commas instead of spaces.

This pull request "collapses" all consecutive commas or spaces into a single one, in fact by removing all empty items returned by FStar.Util.split.

This pull request is not specific to --already_cached, it also impacts --extract and --using_facts_from in the same way.

(Note: this pull request supersedes #1709, which was allowing arguments with no separator at all, but this was not a future-proof idea in the face of changes in the semantics of *, + or -)