diff --git a/controller/coq_lsp.ml b/controller/coq_lsp.ml
index 2edae0a4d..17387cab4 100644
--- a/controller/coq_lsp.ml
+++ b/controller/coq_lsp.ml
@@ -231,7 +231,8 @@ let do_open ~state params =
     DocHandle.create ~uri ~doc;
     Check.schedule ~uri
   (* Maybe send some diagnostics in this case? *)
-  | Coq.Protect.R.Completed (Result.Error (_, msg)) ->
+  | Coq.Protect.R.Completed (Result.Error (Anomaly (_, msg)))
+  | Coq.Protect.R.Completed (Result.Error (User (_, msg))) ->
     let msg = Pp.string_of_ppcmds msg in
     LIO.trace "Fleche.Doc.create" ("internal error" ^ msg)
   | Coq.Protect.R.Interrupted -> ()
@@ -306,7 +307,7 @@ let do_symbols ofmt ~id params =
     let slist = Coq.Ast.grab_definitions f ast in
     let msg = LSP.mk_reply ~id ~result:(`List slist) in
     LIO.send_json ofmt msg
-  | Stopped _ ->
+  | Stopped _ | Failed _ ->
     (* -32802 = RequestFailed | -32803 = ServerCancelled ; *)
     let code = -32802 in
     let message = "Document is not ready" in
@@ -319,7 +320,7 @@ let do_position_request ofmt ~id params ~handler =
   let in_range =
     match doc.completed with
     | Yes _ -> true
-    | Stopped loc ->
+    | Failed loc | Stopped loc ->
       line < loc.line_nb_last
       || (line = loc.line_nb_last && col <= loc.ep - loc.bol_pos_last)
   in
diff --git a/coq/init.ml b/coq/init.ml
index c33a9685f..91de9ffbd 100644
--- a/coq/init.ml
+++ b/coq/init.ml
@@ -72,7 +72,7 @@ let coq_init opts =
 (**************************************************************************)
 
 (* Inits the context for a document *)
-let doc_init ~root_state ~workspace ~libname =
+let doc_init ~root_state ~workspace ~libname () =
   (* Lsp.Io.log_error "init" "starting"; *)
   Vernacstate.unfreeze_interp_state (State.to_coq root_state);
 
@@ -83,3 +83,6 @@ let doc_init ~root_state ~workspace ~libname =
 
   (* We return the state at this point! *)
   Vernacstate.freeze_interp_state ~marshallable:false |> State.of_coq
+
+let doc_init ~root_state ~workspace ~libname =
+  Protect.eval ~f:(doc_init ~root_state ~workspace ~libname) ()
diff --git a/coq/init.mli b/coq/init.mli
index 2358bf1a1..42351de8d 100644
--- a/coq/init.mli
+++ b/coq/init.mli
@@ -33,4 +33,4 @@ val doc_init :
      root_state:State.t
   -> workspace:Workspace.t
   -> libname:Names.DirPath.t
-  -> State.t
+  -> State.t Protect.R.t
diff --git a/coq/interp.ml b/coq/interp.ml
index 784bbb1ae..ff3f261c4 100644
--- a/coq/interp.ml
+++ b/coq/interp.ml
@@ -50,18 +50,15 @@ let marshal_out f oc res =
     | Ok res ->
       Marshal.to_channel oc 0 [];
       f oc res.Info.res
-    | Error (loc, msg) ->
+    | Error _err ->
       Marshal.to_channel oc 1 [];
-      Marshal.to_channel oc loc [];
-      Marshal.to_channel oc msg [];
+      (* Marshal.to_channel oc loc []; *)
+      (* Marshal.to_channel oc msg []; *)
       ())
 
-let marshal_in f ic =
-  let tag : int = Marshal.from_channel ic in
-  if tag = 0 then
-    let res = f ic in
-    Protect.R.Completed (Ok { Info.res; feedback = [] })
-  else
-    let loc : Loc.t option = Marshal.from_channel ic in
-    let msg : Pp.t = Marshal.from_channel ic in
-    Protect.R.Completed (Error (loc, msg))
+(* Needs to be implemeted by Protect.marshal_in *)
+let marshal_in _f _ic = Obj.magic 0
+(* let tag : int = Marshal.from_channel ic in if tag = 0 then let res = f ic in
+   Protect.R.Completed (Ok { Info.res; feedback = [] }) else let loc : Loc.t
+   option = Marshal.from_channel ic in let msg : Pp.t = Marshal.from_channel ic
+   in Protect.R.Completed (Error (User (loc, msg))) *)
diff --git a/coq/parsing.ml b/coq/parsing.ml
new file mode 100644
index 000000000..9f396c887
--- /dev/null
+++ b/coq/parsing.ml
@@ -0,0 +1,10 @@
+let parse ~st ps =
+  let mode = State.mode ~st in
+  let st = State.parsing ~st in
+  (* Coq is missing this, so we add it here. Note that this MUST run inside
+     coq_protect *)
+  Control.check_for_interrupt ();
+  Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps
+  |> Option.map Ast.of_coq
+
+let parse ~st ps = Protect.eval ~f:(parse ~st) ps
diff --git a/coq/parsing.mli b/coq/parsing.mli
new file mode 100644
index 000000000..aba4a267b
--- /dev/null
+++ b/coq/parsing.mli
@@ -0,0 +1 @@
+val parse : st:State.t -> Pcoq.Parsable.t -> Ast.t option Protect.R.t
diff --git a/coq/protect.ml b/coq/protect.ml
index f166e8eca..dc66b7100 100644
--- a/coq/protect.ml
+++ b/coq/protect.ml
@@ -1,5 +1,13 @@
 module Error = struct
-  type t = Loc.t option * Pp.t
+  type payload = Loc.t option * Pp.t
+
+  type t =
+    | User of payload
+    | Anomaly of payload
+
+  let map ~f = function
+    | User e -> User (f e)
+    | Anomaly e -> Anomaly (f e)
 end
 
 module R = struct
@@ -13,7 +21,7 @@ module R = struct
     | Interrupted -> Interrupted
 
   let map_error ~f = function
-    | Completed (Error (loc, msg)) -> Completed (Error (f (loc, msg)))
+    | Completed (Error e) -> Completed (Error (Error.map ~f e))
     | res -> res
 
   let map_loc ~f =
@@ -31,4 +39,5 @@ let eval ~f x =
     let e, info = Exninfo.capture exn in
     let loc = Loc.(get_loc info) in
     let msg = CErrors.iprint (e, info) in
-    R.Completed (Error (loc, msg))
+    if CErrors.is_anomaly e then R.Completed (Error (User (loc, msg)))
+    else R.Completed (Error (Anomaly (loc, msg)))
diff --git a/coq/protect.mli b/coq/protect.mli
index 3fc28a46a..5cb645056 100644
--- a/coq/protect.mli
+++ b/coq/protect.mli
@@ -1,14 +1,18 @@
 module Error : sig
-  type t = Loc.t option * Pp.t
+  type payload = Loc.t option * Pp.t
+
+  type t = private
+    | User of payload
+    | Anomaly of payload
 end
 
 module R : sig
-  type 'a t =
+  type 'a t = private
     | Completed of ('a, Error.t) result
     | Interrupted (* signal sent, eval didn't complete *)
 
   val map : f:('a -> 'b) -> 'a t -> 'b t
-  val map_error : f:(Error.t -> Error.t) -> 'a t -> 'a t
+  val map_error : f:(Error.payload -> Error.payload) -> 'a t -> 'a t
 
   (** Update the loc stored in the result, this is used by our cache-aware
       location *)
diff --git a/coq/state.ml b/coq/state.ml
index 368ccdd4c..c73b73f67 100644
--- a/coq/state.ml
+++ b/coq/state.ml
@@ -77,10 +77,6 @@ let mode ~st =
 let parsing ~st = st.Vernacstate.parsing
 let lemmas ~st = st.Vernacstate.lemmas
 
-let in_state ~st ~f a =
-  Vernacstate.unfreeze_interp_state st;
-  f a
-
 let drop_proofs ~st =
   let open Vernacstate in
   { st with
@@ -88,6 +84,13 @@ let drop_proofs ~st =
       Option.cata (fun s -> snd @@ Vernacstate.LemmaStack.pop s) None st.lemmas
   }
 
+let in_state ~st ~f a =
+  let f a =
+    Vernacstate.unfreeze_interp_state st;
+    f a
+  in
+  Protect.eval ~f a
+
 let admit ~st =
   let () = Vernacstate.unfreeze_interp_state st in
   match st.Vernacstate.lemmas with
@@ -99,3 +102,6 @@ let admit ~st =
     let program = NeList.map_head (fun _ -> pm) st.Vernacstate.program in
     let st = Vernacstate.freeze_interp_state ~marshallable:false in
     { st with lemmas; program }
+
+(* TODO *)
+(* let admit ~st = Protect.eval ~f:(admit ~st) () *)
diff --git a/coq/state.mli b/coq/state.mli
index d1fbea864..cf62f928c 100644
--- a/coq/state.mli
+++ b/coq/state.mli
@@ -10,10 +10,16 @@ val hash : t -> int
 val mode : st:t -> Pvernac.proof_mode option
 val parsing : st:t -> Vernacstate.Parser.t
 val lemmas : st:t -> Vernacstate.LemmaStack.t option
-val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b
+
+(** Execute a command in state [st]. Unfortunately this can produce anomalies as
+    Coq state setting is imperative, so we need to wrap it in protect. *)
+val in_state : st:t -> f:('a -> 'b) -> 'a -> 'b Protect.R.t
 
 (** Drop the proofs from the state *)
 val drop_proofs : st:t -> t
 
-(** Admit an ongoing proof *)
+(* TODO *)
+(* val admit : st:t -> t Protect.R.t *)
+
+(** Admit an ongoing proof, can produce errors *)
 val admit : st:t -> t
diff --git a/fleche/doc.ml b/fleche/doc.ml
index baa1810e8..b3cc3c969 100644
--- a/fleche/doc.ml
+++ b/fleche/doc.ml
@@ -27,6 +27,7 @@ module Completion = struct
   type t =
     | Yes of Loc.t  (** Location of the last token in the document *)
     | Stopped of Loc.t  (** Location of the last valid token *)
+    | Failed of Loc.t  (** Critical failure, like an anomaly *)
 end
 
 (* Private. A doc is a list of nodes for now. The first element in the list is
@@ -46,8 +47,7 @@ type t =
 let mk_doc root_state workspace =
   (* XXX This shouldn't be foo *)
   let libname = Names.(DirPath.make [ Id.of_string "foo" ]) in
-  let f () = Coq.Init.doc_init ~root_state ~workspace ~libname in
-  Coq.Protect.eval ~f ()
+  Coq.Init.doc_init ~root_state ~workspace ~libname
 
 let init_loc ~uri = Loc.initial (InFile { dirpath = None; file = uri })
 
@@ -164,16 +164,8 @@ let report_progress ~doc last_tok =
 (* let close_doc _modname = () *)
 
 let parse_stm ~st ps =
-  let mode = Coq.State.mode ~st in
-  let st = Coq.State.parsing ~st in
-  let parse ps =
-    (* Coq is missing this, so we add it here. Note that this MUST run inside
-       coq_protect *)
-    Control.check_for_interrupt ();
-    Vernacstate.Parser.parse st Pvernac.(main_entry mode) ps
-    |> Option.map Coq.Ast.of_coq
-  in
-  Stats.record ~kind:Stats.Kind.Parsing ~f:(Coq.Protect.eval ~f:parse) ps
+  let f ps = Coq.Parsing.parse ~st ps in
+  Stats.record ~kind:Stats.Kind.Parsing ~f ps
 
 (* Read the input stream until a dot or a "end of proof" token is encountered *)
 let parse_to_terminator : unit Pcoq.Entry.t =
@@ -318,8 +310,14 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
         | Ok (Some ast) ->
           let () = if Debug.parsing then debug_parsed_sentence ~ast in
           (Process ast, [], time)
-        | Error (loc, msg) ->
-          let err_loc = Option.get loc in
+        | Error (Anomaly (_, msg))
+        | Error (User (None, msg)) ->
+          (* We don't have a better altenative :(, usually missing error loc
+             here means an anomaly, so we stop *)
+          let err_loc = last_tok in
+          let diags = [ mk_diag err_loc 1 msg ] in
+          (EOF (Stopped last_tok), diags, time)
+        | Error (User (Some err_loc, msg)) ->
           let diags = [ mk_diag err_loc 1 msg ] in
           discard_to_dot doc_handle;
           let last_tok = Pcoq.Parsable.loc doc_handle in
@@ -370,7 +368,8 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
           in
           let doc = add_node ~node doc in
           stm doc state last_tok_new
-        | Error (err_loc, msg) ->
+        | Error (Anomaly (err_loc, msg) as coq_err)
+        | Error (User (err_loc, msg) as coq_err) ->
           let err_loc = Option.default ast_loc err_loc in
           let diags = [ mk_error_diagnostic ~loc:err_loc ~msg ~ast ] in
           (* FB should be handled by Coq.Protect.eval XXX *)
@@ -390,7 +389,11 @@ let process_and_parse ~uri ~version ~fb_queue doc last_tok doc_handle =
             }
           in
           let doc = add_node ~node doc in
-          stm doc st last_tok_new))
+          match coq_err with
+          | Anomaly _ ->
+            set_completion ~completed:(Failed last_tok_new) doc
+          | User _ ->
+            stm doc st last_tok_new))
   in
   (* Note that nodes and diags in reversed order here *)
   (match doc.nodes with
@@ -439,11 +442,21 @@ let log_resume last_tok =
       asprintf "resuming, from: %d l: %d" last_tok.Loc.ep
         last_tok.Loc.line_nb_last)
 
+let safe_sub s pos len =
+  if pos < 0 || len < 0 || pos > String.length s - len then (
+    Io.Log.trace "string_sub"
+      (Format.asprintf "error for pos: %d len: %d str: %s" pos len s);
+    s)
+  else String.sub s pos len
+
 let check ~ofmt:_ ~doc ~fb_queue =
   match doc.completed with
   | Yes _ ->
     Io.Log.trace "check" "resuming, completed=yes, nothing to do";
     doc
+  | Failed _ ->
+    Io.Log.trace "check" "can't resume, failed=yes, nothing to do";
+    doc
   | Stopped last_tok ->
     log_resume last_tok;
     let uri, version, contents = (doc.uri, doc.version, doc.contents) in
@@ -453,7 +466,8 @@ let check ~ofmt:_ ~doc ~fb_queue =
     let resume_loc = CLexer.after last_tok in
     let offset = resume_loc.bp in
     let processed_content =
-      String.(sub processed_content offset (length processed_content - offset))
+      safe_sub processed_content offset
+        (String.length processed_content - offset)
     in
     let handle =
       Pcoq.Parsable.make ~loc:resume_loc
@@ -473,8 +487,9 @@ let check ~ofmt:_ ~doc ~fb_queue =
         match doc.completed with
         | Yes loc -> loc
         | Stopped loc -> loc
+        | Failed loc -> loc
       in
-      Format.asprintf "done [%.2f]: document fully checked %s" timestamp
+      Format.asprintf "done [%.2f]: document fully checked up to %s" timestamp
         (Coq.Ast.pr_loc loc)
     in
     Io.Log.trace "check" end_msg;
diff --git a/fleche/doc.mli b/fleche/doc.mli
index 59b2ef254..d8c60f840 100644
--- a/fleche/doc.mli
+++ b/fleche/doc.mli
@@ -31,6 +31,7 @@ module Completion : sig
   type t =
     | Yes of Loc.t  (** Location of the last token in the document *)
     | Stopped of Loc.t  (** Location of the last valid token *)
+    | Failed of Loc.t  (** Critical failure, like an anomaly *)
 end
 
 type t = private
diff --git a/fleche/info.ml b/fleche/info.ml
index 7b88aa561..2e57de6b1 100644
--- a/fleche/info.ml
+++ b/fleche/info.ml
@@ -181,10 +181,15 @@ module Make (P : Point) : S with module P := P = struct
     let node = find ~doc ~point approx in
     Option.bind node (fun node -> node.Doc.ast)
 
+  let in_state ~st ~f node =
+    match Coq.State.in_state ~st ~f node with
+    | Coq.Protect.R.Completed (Result.Ok res) -> res
+    | Coq.Protect.R.Completed (Result.Error _) | Coq.Protect.R.Interrupted ->
+      None
+
   let goals ~doc ~point approx =
     find ~doc ~point approx
-    |> obind (fun node ->
-           Coq.State.in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state)
+    |> obind (fun node -> in_state ~st:node.Doc.state ~f:pr_goal node.Doc.state)
 
   let messages ~doc ~point approx =
     find ~doc ~point approx |> Option.map (fun node -> node.Doc.messages)
@@ -205,7 +210,7 @@ module Make (P : Point) : S with module P := P = struct
   let completion ~doc ~point prefix =
     find ~doc ~point Exact
     |> obind (fun node ->
-           Coq.State.in_state ~st:node.Doc.state prefix ~f:(fun prefix ->
+           in_state ~st:node.Doc.state prefix ~f:(fun prefix ->
                to_qualid prefix
                |> obind (fun p ->
                       Nametab.completion_canditates p
diff --git a/fleche/memo.mli b/fleche/memo.mli
index c28bc1b6a..534386df5 100644
--- a/fleche/memo.mli
+++ b/fleche/memo.mli
@@ -17,6 +17,9 @@ val interp_command :
   -> Coq.State.t Coq.Interp.interp_result Stats.t
 
 val interp_admitted : st:Coq.State.t -> Coq.State.t
+(* TODO *)
+(* val interp_admitted : st:Coq.State.t -> Coq.State.t Coq.Protect.R.t *)
+
 val mem_stats : unit -> int
 val load_from_disk : file:string -> unit
 val save_to_disk : file:string -> unit