1 files changed, 23 insertions, 13 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bd98fe16e..12ef0e075 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -130,7 +130,8 @@ let annotate phrase =
 
 (** Goal display *)
 
-let hyp_next_tac sigma env (id,_,ast) =
+let hyp_next_tac sigma env decl =
+  let (id,_,ast) = Context.Named.Declaration.to_tuple decl in
   let id_s = Names.Id.to_string id in
   let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in
   [
@@ -184,14 +185,19 @@ let process_goal sigma g =
   let id = Goal.uid g in
   let ccl =
     let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in
+    Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
+  in
   let process_hyp d (env,l) =
-    let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in
-    let d' = List.map (fun x -> (x, pi2 d, pi3 d)) (pi1 d) in
+    let d = Context.NamedList.Declaration.map_constr (Reductionops.nf_evar sigma) d in
+    let d' = List.map (fun name -> let open Context.Named.Declaration in
+                                   match pi2 d with
+                                   | None -> LocalAssum (name, pi3 d)
+                                   | Some value -> LocalDef (name, value, pi3 d))
+                      (pi1 d) in
       (List.fold_right Environ.push_named d' env,
-       (string_of_ppcmds (pr_var_list_decl env sigma d)) :: l) in
+       (Richpp.richpp_of_pp (pr_var_list_decl env sigma d)) :: l) in
   let (_env, hyps) =
-    Context.fold_named_list_context process_hyp
+    Context.NamedList.fold process_hyp
       (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
   { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
 
@@ -333,10 +339,14 @@ let handle_exn (e, info) =
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
-  let mk_msg () = read_stdout ()^"\n"^string_of_ppcmds (Errors.print ~info e) in
+  let mk_msg () =
+    let msg = read_stdout () in
+    let msg = str msg ++ fnl () ++ Errors.print ~info e in
+    Richpp.richpp_of_pp msg
+  in
   match e with
-  | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
-  | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
+  | Errors.Drop -> dummy, None, Richpp.richpp_of_string "Drop is not allowed by coqide!"
+  | Errors.Quit -> dummy, None, Richpp.richpp_of_string "Quit is not allowed by coqide!"
   | e ->
       match Stateid.get info with
       | Some (valid, _) -> valid, loc_of info, mk_msg ()
@@ -432,12 +442,12 @@ let print_xml =
 
 let slave_logger xml_oc level message =
   (* convert the message into XML *)
-  let msg = string_of_ppcmds (hov 0 message) in
+  let msg = hov 0 message in
   let message = {
     Pp.message_level = level;
-    Pp.message_content = msg;
+    Pp.message_content = (Richpp.repr (Richpp.richpp_of_pp msg));
   } in
-  let () = pr_debug (Printf.sprintf "-> %S" msg) in
+  let () = pr_debug (Printf.sprintf "-> %S" (string_of_ppcmds msg)) in
   let xml = Pp.of_message message in
   print_xml xml_oc xml
 
@@ -469,7 +479,7 @@ let loop () =
     try
       let xml_query = Xml_parser.parse xml_ic in
 (*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
-      let q = Xmlprotocol.to_call xml_query in
+      let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
       let () = pr_debug_call q in
       let r = eval_call xml_oc (slave_logger xml_oc Pp.Notice) q in
       let () = pr_debug_answer q r in