diff --git a/src/interactive/FStarC.Interactive.Incremental.fst b/src/interactive/FStarC.Interactive.Incremental.fst index b43b3967ad8..56403e39651 100644 --- a/src/interactive/FStarC.Interactive.Incremental.fst +++ b/src/interactive/FStarC.Interactive.Incremental.fst @@ -269,7 +269,12 @@ let run_full_buffer (st:repl_state) (with_symbols:bool) (write_full_buffer_fragment_progress: fragment_progress -> unit) : list query & list json - = let parse_result = parse_code None code in + = // updating the vfs entry allows dependence scanning on the file to + // to use the latest snapshot of the file, rather than what was present + // in the buffer when the IDE was started. This is especially useful when + // creating a new file and launching F* on it + FStarC.Parser.ParseIt.add_vfs_entry st.repl_fname code; + let parse_result = parse_code None code in let log_syntax_issues err = match err with | None -> () diff --git a/tests/ide/Makefile b/tests/ide/Makefile index 6923acf6a08..fdb4e7cfd29 100644 --- a/tests/ide/Makefile +++ b/tests/ide/Makefile @@ -5,12 +5,15 @@ include $(FSTAR_ROOT)/mk/test.mk INCR_TEST_FILES := $(wildcard $(FSTAR_ROOT)/ulib/*.fst $(FSTAR_ROOT)/ulib/*.fsti) -.PHONY: test_incremental +.PHONY: test_incremental test_ide_without_file test_incremental: $(patsubst $(FSTAR_ROOT)/ulib/%, %.test-incr, $(INCR_TEST_FILES)) +test_ide_without_file: + $(FSTAR_EXE) --ide TestNoFile.fst < idewithoutfile.in + %.test-incr: $(FSTAR_ROOT)/ulib/% $(call msg, "IDE_INCR", $<) python3 test-incremental.py $(FSTAR_EXE) $< $(if $(V),,>/dev/null) @touch $@ -all: test_incremental +all: test_incremental test_ide_without_file diff --git a/tests/ide/idewithoutfile.in b/tests/ide/idewithoutfile.in new file mode 100644 index 00000000000..636a47feb55 --- /dev/null +++ b/tests/ide/idewithoutfile.in @@ -0,0 +1 @@ +{"query":"full-buffer","args":{"kind":"verify-to-position","with-symbols":false,"code":"module TestNoFile\n\nmodule L = FStar.List.Tot let test x = L.length x","line":0,"column":0,"to-position":{"line":3,"column":9}},"query-id":"2"}