Update ide mode to delay dependence scanning until the first check of the full buffer

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 -> ()

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

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"}