fix parsing error : return commands even when the end of the file con…

…tains parsing error

src/lsp/lp_doc.ml

@@ -164,35 +164,29 @@ let dummy_loc =
 
 let check_text ~doc =
   let uri, version = doc.uri, doc.version in
+  let cmds, error = Pure.parse_text ~fname:uri doc.text in
   let root =
     match doc.root with
-    | Some(ss) -> ss
+    | Some ss -> ss
     | None ->
-      raise(Error.fatal_no_pos "Root state is missing
-      probably because new_doc has raised exception")
+        raise(Error.fatal_no_pos "Root state is missing probably because \
+                                  new_doc raised an exception")
   in
-  try
-    let cmds =
-      let (cmds, root) = Pure.parse_text root ~fname:uri doc.text in
-      (* One shot state update after parsing. *)
-      doc.root <- Some(root); doc.final <- Some(root); cmds
-    in
-
-    (* compute rangemap *)
-    let map = Pure.rangemap cmds in
-
-    let nodes, final, diag, logs =
-      List.fold_left (process_cmd uri) ([],root,[],[]) cmds in
-    let logs = List.rev logs in
-    let doc = { doc with nodes; final=Some(final); map; logs } in
-    doc,
-    LSP.mk_diagnostics ~uri ~version @@
+  let nodes, final, diags, logs =
+    List.fold_left (process_cmd uri) ([],root,[],[]) cmds in
+  let logs = List.rev logs
+  and diags = (* filter out diagnostics with no position *)
     List.fold_left (fun acc (pos,lvl,msg,goal) ->
         match pos with
         | None     -> acc
         | Some pos -> (pos,lvl,msg,goal) :: acc
-      ) [] diag
-  with
-  | Pure.Parse_error(loc, msg) ->
-    let logs = [((1, msg), Some loc)] in
-    {doc with logs}, mk_error ~doc loc msg
+      ) [] diags
+  in
+  let logs, diags =
+    match error with
+    | None -> logs, diags
+    | Some(pos,msg) -> ((1, msg), Some pos)::logs, (pos,1,msg,None)::diags
+  in
+  let map = Pure.rangemap cmds in
+  let doc = { doc with nodes; final=Some(final); map; logs } in
+  doc, LSP.mk_diagnostics ~uri ~version diags

src/pure/pure.ml

@@ -58,29 +58,23 @@ end
 type state = Time.t * Sig_state.t
 
 (** Exception raised by [parse_text] on error. *)
-exception Parse_error of Pos.pos * string
 
-let parse_text : state -> fname:string -> string -> Command.t list * state =
-    fun (t,st) ~fname s ->
-  let dk_syntax = Filename.check_suffix fname dk_src_extension in
+let parse_text :
+      fname:string -> string -> Command.t list * (Pos.pos * string) option =
+  fun ~fname s ->
+  let parse_string =
+    if Filename.check_suffix fname dk_src_extension then
+      Parser.Dk.parse_string
+    else Parser.parse_string
+  in
+  let cmds = Stdlib.ref [] in
   try
-    Time.restore t;
-    let ast =
-      let strm =
-        if dk_syntax then Parser.Dk.parse_string fname s
-        else Parser.parse_string fname s
-      in
-      (* NOTE this processing could be avoided with a parser for a list of
-         commands. Such a parser is not trivially done. *)
-      let cmds = Stdlib.ref [] in
-      Stream.iter (fun c -> Stdlib.(cmds := c :: !cmds)) strm;
-      List.rev Stdlib.(!cmds)
-    in
-    (ast, (Time.save (), st))
+    Stream.iter (fun c -> Stdlib.(cmds := c :: !cmds)) (parse_string fname s);
+    List.rev Stdlib.(!cmds), None
   with
-  | Fatal(Some(Some(pos)), msg) -> raise (Parse_error(pos, msg))
-  | Fatal(Some(None)     , _  ) -> assert false (* Should not produce. *)
-  | Fatal(None           , _  ) -> assert false (* Should not produce. *)
+  | Fatal(Some(Some(pos)), msg) -> List.rev Stdlib.(!cmds), Some(pos, msg)
+  | Fatal(Some(None)     , _  ) -> assert false
+  | Fatal(None           , _  ) -> assert false
 
 type proof_finalizer = Sig_state.t -> Proof.proof_state -> Sig_state.t
 

src/pure/pure.mli

@@ -35,14 +35,12 @@ type state
 (** Representation of the state when in a proof. *)
 type proof_state
 
-(** Exception raised by [parse_text]. *)
-exception Parse_error of Pos.pos * string
-
-(** [parse_text st ~fname contents] runs the parser on the string [contents]
-   as if it were a file named [fname]. The action takes place in the state
-   [st], and an updated state is returned. The function may raise
-   [Parse_error]. *)
-val parse_text : state -> fname:string -> string -> Command.t list * state
+(** [parse_text ~fname contents] runs the parser on the string [contents] as
+    if it were a file named [fname]. It returns the list of commands it could
+    parse and, either [None] if it could parse all commands, or some position
+    and error message otherwise. *)
+    val parse_text :
+    fname:string -> string -> Command.t list * (Pos.pos * string) option
 
 (** A goal is given by a list of assumptions and a conclusion. Each assumption
    has a name and a type. *)