Merge branch 'v8.5'

6 files changed, 35 insertions, 22 deletions

diff --git a/stm/spawned.ml b/stm/spawned.ml
index a8372195d4..66fe07dbc4 100644
--- a/stm/spawned.ml
+++ b/stm/spawned.ml
@@ -11,7 +11,7 @@ open Spawn
 let pr_err s = Printf.eprintf "(Spawned,%d) %s\n%!" (Unix.getpid ()) s
 let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
 
-type chandescr = AnonPipe | Socket of string * int
+type chandescr = AnonPipe | Socket of string * int * int
 
 let handshake cin cout =
   try
@@ -26,18 +26,19 @@ let handshake cin cout =
   | End_of_file ->
       pr_err "Handshake failed: End_of_file"; raise (Failure "handshake")
 
-let open_bin_connection h p =
+let open_bin_connection h pr pw =
   let open Unix in
-  let cin, cout = open_connection (ADDR_INET (inet_addr_of_string h,p)) in
+  let _, cout = open_connection (ADDR_INET (inet_addr_of_string h,pr)) in
+  let cin, _ = open_connection (ADDR_INET (inet_addr_of_string h,pw)) in
   set_binary_mode_in cin true;
   set_binary_mode_out cout true;
   let cin = CThread.prepare_in_channel_for_thread_friendly_io cin in
   cin, cout
 
-let controller h p =
+let controller h pr pw =
   prerr_endline "starting controller thread";
   let main () =
-    let ic, oc = open_bin_connection h p in
+    let ic, oc = open_bin_connection h pr pw in
     let rec loop () =
       try
         match CThread.thread_friendly_input_value ic with
@@ -61,8 +62,8 @@ let init_channels () =
   if !channels <> None then Errors.anomaly(Pp.str "init_channels called twice");
   let () = match !main_channel with
   | None -> ()
-  | Some (Socket(mh,mp)) ->
-    channels := Some (open_bin_connection mh mp);
+  | Some (Socket(mh,mpr,mpw)) ->
+    channels := Some (open_bin_connection mh mpr mpw);
   | Some AnonPipe ->
     let stdin = Unix.in_channel_of_descr (Unix.dup Unix.stdin) in
     let stdout = Unix.out_channel_of_descr (Unix.dup Unix.stdout) in
@@ -74,8 +75,8 @@ let init_channels () =
   in
   match !control_channel with
   | None -> ()
-  | Some (Socket (ch, cp)) ->
-    controller ch cp
+  | Some (Socket (ch, cpr, cpw)) ->
+    controller ch cpr cpw
   | Some AnonPipe ->
     Errors.anomaly (Pp.str "control channel cannot be a pipe")
 
diff --git a/stm/spawned.mli b/stm/spawned.mli
index d9e7baff3b..d0183e081d 100644
--- a/stm/spawned.mli
+++ b/stm/spawned.mli
@@ -8,7 +8,7 @@
 
 (* To link this file, threads are needed *)
 
-type chandescr = AnonPipe | Socket of string * int
+type chandescr = AnonPipe | Socket of string * int * int
 
 (* Argument parsing should set these *)
 val main_channel : chandescr option ref
diff --git a/stm/stm.ml b/stm/stm.ml
index f178c3ae4a..c7836d118b 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -888,9 +888,16 @@ let set_compilation_hints file =
   hints := Aux_file.load_aux_file_for file
 let get_hint_ctx loc =
   let s = Aux_file.get !hints loc "context_used" in
-  let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in
-  let ids = List.map (fun id -> Loc.ghost, id) ids in
-  SsExpr (SsSet ids)
+  match Str.split (Str.regexp ";") s with
+  | ids :: _ ->
+      let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") ids) in
+      let ids = List.map (fun id -> Loc.ghost, id) ids in
+      begin match ids with
+      | [] -> SsEmpty
+      | x :: xs ->
+          List.fold_left (fun a x -> SsUnion (SsSingl x,a)) (SsSingl x) xs
+      end
+  | _ -> raise Not_found
 
 let get_hint_bp_time proof_name =
   try float_of_string (Aux_file.get !hints Loc.ghost proof_name)
@@ -1577,7 +1584,8 @@ end = struct (* {{{ *)
       vernac_interp r_for { r_what with verbose = true };
       feedback ~state_id:r_for Feedback.Processed     
     with e when Errors.noncritical e ->
-      let msg = string_of_ppcmds (print e) in
+      let e = Errors.push e in
+      let msg = string_of_ppcmds (iprint e) in
       feedback ~state_id:r_for (Feedback.ErrorMsg (Loc.ghost, msg))
     
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
@@ -2341,7 +2349,8 @@ let edit_at id =
     VCS.delete_cluster_of id;
     VCS.gc ();
     VCS.print ();
-    Reach.known_state ~cache:(interactive ()) id;
+    if not !Flags.async_proofs_full then
+      Reach.known_state ~cache:(interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
   try
diff --git a/stm/stm.mli b/stm/stm.mli
index 1d926e998e..4bad7f0a6d 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -35,7 +35,9 @@ val query :
    new document tip, the document between [id] and [fo.stop] has been dropped.
    The portion between [fo.stop] and [fo.tip] has been kept.  [fo.start] is
    just to tell the gui where the editing zone starts, in case it wants to
-   graphically denote it.  All subsequent [add] happen on top of [id]. *)
+   graphically denote it.  All subsequent [add] happen on top of [id].
+   If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is.
+*)
 type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t }
 val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ]
 
@@ -49,11 +51,11 @@ val stop_worker : string -> unit
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
 
-(* Saves on the dist a .vio corresponding to the current status:
-   - if the worker prool is empty, all tasks are saved
+(* Saves on the disk a .vio corresponding to the current status:
+   - if the worker pool is empty, all tasks are saved
    - if the worker proof is not empty, then it waits until all workers
      are done with their current jobs and then dumps (or fails if one
-     of the completed tasks is a failuere) *)
+     of the completed tasks is a failure) *)
 val snapshot_vio : DirPath.t -> string -> unit
 
 (* Empties the task queue, can be used only if the worker pool is empty (E.g.
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index fb41bb7bea..b912080413 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -575,10 +575,11 @@ let rec tmpp v loc =
       end
   | VernacExactProof _ as x -> xmlTODO loc x
   | VernacAssumption ((l, a), _, sbwcl) ->
+      let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
       let many =
-        List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in
+        List.length (List.flatten (List.map fst binders)) > 1 in
       let exprs =
-        List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in
+        List.flatten (List.map pp_simple_binder binders) in
       let l = match l with Some x -> x | None -> Decl_kinds.Global in
       let kind = string_of_assumption_kind l a many in
       xmlAssumption kind loc exprs
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 8aa2a59177..a898c687be 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -141,7 +141,7 @@ let rec classify_vernac e =
         else VtSideff ids, VtLater
     (* Sideff: apply to all open branches. usually run on master only *)
     | VernacAssumption (_,_,l) ->
-        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map snd l) l) in
+        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in
         VtSideff ids, VtLater    
     | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff [id], VtLater
     | VernacInductive (_,_,l) ->