Tweak column numbers in IDE digest computation

Author: mtzguido

src/interactive/FStarC.Interactive.Ide.fst

@@ -533,7 +533,7 @@ let run_segment (st: repl_state) (code: string) =
   // Unfortunately, frag_fname is a special case in the interactive mode,
   // while in LSP, it is the only mode. To cope with this difference,
   // pass a frag_fname that is expected by the Interactive mode.
-  let frag = { frag_fname = "<input>"; frag_text = code; frag_line = 1; frag_col = 0 } in
+  let frag = { frag_fname = "<input>"; frag_text = code; frag_line = 1; frag_col = 1 } in
 
   let collect_decls () =
     match Parser.Driver.parse_fragment None frag with

src/ml/FStarC_Parser_ParseIt.ml

@@ -186,18 +186,19 @@ let parse_incremental_decls
   in
   parse []
 
-let contents_at contents =
+let contents_at (contents : string) : Range.t -> code_fragment =
     let lines = U.splitlines contents in
     let split_line_at_col line col =
-        if col > 0
+        (* NB: columns are 1-based *)
+        if col > 1
         then (
             (* Don't index directly into the string, since this is a UTF-8 string.
                 Convert first to a list of characters, index into that, and then convert
                 back to a string *)
             let chars = FStar_String.list_of_string line in
-            if col <= List.length chars
+            if col <= List.length chars + 1
             then (
-              let prefix, suffix = FStarC_Util.first_N (Z.of_int col) chars in
+              let prefix, suffix = FStarC_Util.first_N (Z.of_int (col - 1)) chars in
               Some (FStar_String.string_of_list prefix, 
                     FStar_String.string_of_list suffix)
             )

tests/ide/emacs/Tutorial.segment.ideout.expected

@@ -1,2 +1,2 @@
 {"kind": "protocol-info", "rest": "[...]"}
-{"kind": "response", "query-id": "1", "response": {"decls": [{"def_range": {"beg": [1, 0], "end": [1, 15], "fname": "<input>"}}, {"def_range": {"beg": [2, 0], "end": [2, 13], "fname": "<input>"}}, {"def_range": {"beg": [3, 0], "end": [3, 14], "fname": "<input>"}}, {"def_range": {"beg": [6, 0], "end": [6, 22], "fname": "<input>"}}, {"def_range": {"beg": [9, 0], "end": [12, 16], "fname": "<input>"}}, {"def_range": {"beg": [15, 0], "end": [17, 20], "fname": "<input>"}}, {"def_range": {"beg": [20, 0], "end": [20, 47], "fname": "<input>"}}, {"def_range": {"beg": [21, 0], "end": [21, 73], "fname": "<input>"}}, {"def_range": {"beg": [23, 0], "end": [23, 55], "fname": "<input>"}}, {"def_range": {"beg": [24, 0], "end": [24, 93], "fname": "<input>"}}, {"def_range": {"beg": [27, 0], "end": [27, 29], "fname": "<input>"}}, {"def_range": {"beg": [28, 0], "end": [28, 27], "fname": "<input>"}}, {"def_range": {"beg": [29, 0], "end": [29, 29], "fname": "<input>"}}, {"def_range": {"beg": [32, 0], "end": [32, 36], "fname": "<input>"}}, {"def_range": {"beg": [33, 0], "end": [37, 20], "fname": "<input>"}}, {"def_range": {"beg": [41, 0], "end": [41, 21], "fname": "<input>"}}, {"def_range": {"beg": [42, 0], "end": [42, 39], "fname": "<input>"}}, {"def_range": {"beg": [43, 0], "end": [44, 49], "fname": "<input>"}}, {"def_range": {"beg": [47, 7], "end": [47, 55], "fname": "<input>"}}, {"def_range": {"beg": [54, 0], "end": [59, 28], "fname": "<input>"}}, {"def_range": {"beg": [61, 0], "end": [61, 48], "fname": "<input>"}}]}, "status": "success"}
+{"kind": "response", "query-id": "1", "response": {"decls": [{"def_range": {"beg": [1, 1], "end": [1, 16], "fname": "<input>"}}, {"def_range": {"beg": [2, 0], "end": [2, 13], "fname": "<input>"}}, {"def_range": {"beg": [3, 0], "end": [3, 14], "fname": "<input>"}}, {"def_range": {"beg": [6, 0], "end": [6, 22], "fname": "<input>"}}, {"def_range": {"beg": [9, 0], "end": [12, 16], "fname": "<input>"}}, {"def_range": {"beg": [15, 0], "end": [17, 20], "fname": "<input>"}}, {"def_range": {"beg": [20, 0], "end": [20, 47], "fname": "<input>"}}, {"def_range": {"beg": [21, 0], "end": [21, 73], "fname": "<input>"}}, {"def_range": {"beg": [23, 0], "end": [23, 55], "fname": "<input>"}}, {"def_range": {"beg": [24, 0], "end": [24, 93], "fname": "<input>"}}, {"def_range": {"beg": [27, 0], "end": [27, 29], "fname": "<input>"}}, {"def_range": {"beg": [28, 0], "end": [28, 27], "fname": "<input>"}}, {"def_range": {"beg": [29, 0], "end": [29, 29], "fname": "<input>"}}, {"def_range": {"beg": [32, 0], "end": [32, 36], "fname": "<input>"}}, {"def_range": {"beg": [33, 0], "end": [37, 20], "fname": "<input>"}}, {"def_range": {"beg": [41, 0], "end": [41, 21], "fname": "<input>"}}, {"def_range": {"beg": [42, 0], "end": [42, 39], "fname": "<input>"}}, {"def_range": {"beg": [43, 0], "end": [44, 49], "fname": "<input>"}}, {"def_range": {"beg": [47, 7], "end": [47, 55], "fname": "<input>"}}, {"def_range": {"beg": [54, 0], "end": [59, 28], "fname": "<input>"}}, {"def_range": {"beg": [61, 0], "end": [61, 48], "fname": "<input>"}}]}, "status": "success"}