Add a smart constructor for [update_session] conf

examples/use_api/create_session.ml

@@ -59,13 +59,9 @@ let dummy_keygen ?parent () = ()
 (* create an empty session in the current directory *)
 let env_session,_,_ =
   let dummy_session : unit Session.session = Session.create_session "." in
-  let ctxt = {
-    Session.allow_obsolete_goals = true;
-    Session.keep_unmatched_theories = false;
-    Session.release_tasks = false;
-    Session.use_shapes_for_pairing_sub_goals = false;
-    Session.keygen = dummy_keygen;
-  }
+  let ctxt = Session.mk_update_context
+    ~allow_obsolete_goals:true
+    dummy_keygen
   in
   Session.update_session ~ctxt dummy_session env config
 

src/session/session.ml

@@ -2294,6 +2294,20 @@ type 'key update_context =
     keep_unmatched_theories : bool;
   }
 
+let mk_update_context
+  ?(allow_obsolete_goals=false)
+  ?(release_tasks=false)
+  ?(use_shapes_for_pairing_sub_goals=false)
+  ?(keep_unmatched_theories=false)
+  keygen =
+  { allow_obsolete_goals;
+    release_tasks;
+    use_shapes_for_pairing_sub_goals;
+    keygen;
+    keep_unmatched_theories;
+  }
+
+
 let rec recover_sub_tasks ~theories env_session task g =
   g.goal_task <- Some task;
   (* Check that the sum and shape don't change (the order is kept)

src/session/session.mli

@@ -248,6 +248,16 @@ type 'key update_context =
     keep_unmatched_theories : bool;
   }
 
+val mk_update_context:
+  ?allow_obsolete_goals : bool ->
+  ?release_tasks : bool ->
+  ?use_shapes_for_pairing_sub_goals : bool ->
+  ?keep_unmatched_theories : bool ->
+  'key keygen ->
+  'key update_context
+(** By default all optional arguments are false. The meaning of the
+    arguments is described in {!Session.update_session} *)
+
 val update_session :
   ctxt:'key update_context ->
   'oldkey session ->

src/session/session_scheduler.ml

@@ -294,13 +294,11 @@ let init_session session = session_iter init_any session
 let update_session ~allow_obsolete ~release ~use_shapes
     old_session env whyconf  =
   O.reset ();
-  let ctxt = {
-    keep_unmatched_theories = false;
-    allow_obsolete_goals = allow_obsolete;
-    release_tasks = release;
-    use_shapes_for_pairing_sub_goals = use_shapes;
-    keygen = O.create;
-  }
+  let ctxt = Session.mk_update_context
+      ~allow_obsolete_goals:allow_obsolete
+      ~release_tasks:release
+      ~use_shapes_for_pairing_sub_goals:use_shapes
+      O.create
   in
   let (env_session,_,_) as res =
     update_session ~ctxt old_session env whyconf

src/why3session/why3session_lib.ml

@@ -74,13 +74,10 @@ let read_env_spec () =
 let read_update_session ~allow_obsolete env config fname =
   let project_dir = S.get_project_dir fname in
   let session,use_shapes = S.read_session project_dir in
-  let ctxt = {
-    S.allow_obsolete_goals = allow_obsolete;
-    S.keep_unmatched_theories = false;
-    S.release_tasks = false;
-    S.use_shapes_for_pairing_sub_goals = use_shapes;
-    S.keygen = (fun ?parent:_ () -> ());
-  }
+  let ctxt = S.mk_update_context
+    ~allow_obsolete_goals:allow_obsolete
+    ~use_shapes_for_pairing_sub_goals:use_shapes
+    (fun ?parent:_ () -> ())
   in
   S.update_session ~ctxt session env config