gui option to ask for showing tasks with full context

src/ide/gconfig.ml

@@ -40,6 +40,7 @@ type t =
       mutable default_prover : string; (* "" means none *)
       mutable default_editor : string;
       mutable intro_premises : bool;
+      mutable show_full_context : bool;
       mutable show_labels : bool;
       mutable show_locs : bool;
       mutable show_time_limit : bool;
@@ -74,6 +75,7 @@ type ide = {
   ide_current_tab : int;
   ide_verbose : int;
   ide_intro_premises : bool;
+  ide_show_full_context : bool;
   ide_show_labels : bool;
   ide_show_locs : bool;
   ide_show_time_limit : bool;
@@ -99,6 +101,7 @@ let default_ide =
     ide_current_tab = 0;
     ide_verbose = 0;
     ide_intro_premises = true;
+    ide_show_full_context = false;
     ide_show_labels = false;
     ide_show_locs = false;
     ide_show_time_limit = false;
@@ -134,6 +137,9 @@ let load_ide section =
     ide_intro_premises =
       get_bool section ~default:default_ide.ide_intro_premises
         "intro_premises";
+    ide_show_full_context =
+      get_bool section ~default:default_ide.ide_show_full_context
+        "show_full_context";
     ide_show_labels =
       get_bool section ~default:default_ide.ide_show_labels "print_labels";
     ide_show_locs =
@@ -197,6 +203,7 @@ let load_config config original_config =
     font_size     = ide.ide_font_size;
     verbose       = ide.ide_verbose;
     intro_premises= ide.ide_intro_premises ;
+    show_full_context= ide.ide_show_full_context ;
     show_labels   = ide.ide_show_labels ;
     show_locs     = ide.ide_show_locs ;
     show_time_limit = ide.ide_show_time_limit;
@@ -245,6 +252,7 @@ let save_config t =
   let ide = set_int ide "font_size" t.font_size in
   let ide = set_int ide "verbose" t.verbose in
   let ide = set_bool ide "intro_premises" t.intro_premises in
+  let ide = set_bool ide "show_full_context" t.show_full_context in
   let ide = set_bool ide "print_labels" t.show_labels in
   let ide = set_bool ide "print_locs" t.show_locs in
   let ide = set_bool ide "print_time_limit" t.show_time_limit in
@@ -791,6 +799,15 @@ let appearance_settings (c : t) (notebook:GPack.notebook) =
     intropremises#connect#toggled ~callback:
       (fun () -> c.intro_premises <- not c.intro_premises)
   in
+  let showfullcontext =
+    GButton.check_button ~label:"show full task context"
+      ~packing:display_options_box#add ()
+      ~active:c.show_full_context
+  in
+  let (_ : GtkSignal.id) =
+    showfullcontext#connect#toggled ~callback:
+      (fun () -> c.show_full_context <- not c.show_full_context)
+  in
   let showlabels =
     GButton.check_button
       ~label:"show labels in formulas"
@@ -1263,6 +1280,6 @@ let uninstalled_prover c eS unknown =
 
 (*
 Local Variables:
-compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
+compile-command: "unset LANG; make -C ../.. bin/why3ide.opt"
 End:
 *)

src/ide/gconfig.mli

@@ -22,6 +22,7 @@ type t =
       mutable default_prover : string;
       mutable default_editor : string;
       mutable intro_premises : bool;
+      mutable show_full_context : bool;
       mutable show_labels : bool;
       mutable show_locs : bool;
       mutable show_time_limit : bool;

src/ide/why3ide.ml

@@ -1262,7 +1262,8 @@ let on_selected_row r =
         task_view#source_buffer#set_text ""
       else
         let b = gconfig.intro_premises in
-        send_request (Get_task(id,b, true))
+        let c = gconfig.show_full_context in
+        send_request (Get_task(id,b,c,true))
     | NProofAttempt ->
        let (pa, _obs, _l) = Hint.find node_id_pa id in
        let output_text =
@@ -1289,7 +1290,8 @@ let on_selected_row r =
        counterexample_view#scroll_to_mark `INSERT
     | _ ->
        let b = gconfig.intro_premises in
-       send_request (Get_task(id,b,true))
+       let c = gconfig.show_full_context in
+       send_request (Get_task(id,b,c,true))
   with
     | Not_found -> task_view#source_buffer#set_text ""
 

src/ide/why3web.ml

@@ -69,8 +69,9 @@ let interp_request args =
       | _ -> invalid_arg ("Why3web.interp_request '" ^ args ^ "'"))
   | args when Strings.has_prefix "gettask_" args ->
      let b = false (* TODO: allow user to customize printing with intros or not *) in
+     let c = false in
      let loc = true in
-     Get_task (int_of_string (Strings.remove_prefix "gettask_" args),b,loc)
+     Get_task (int_of_string (Strings.remove_prefix "gettask_" args),b,c,loc)
   | _ -> invalid_arg ("Why3web.interp_request '" ^ args ^ "'")
 
 let handle_script s args =

src/session/itp_communication.ml

@@ -104,7 +104,7 @@ type ide_request =
   | Add_file_req            of string
   | Set_config_param        of string * int
   | Get_file_contents       of string
-  | Get_task                of node_ID * bool * bool
+  | Get_task                of node_ID * bool * bool * bool
   | Focus_req               of node_ID
   | Unfocus_req
   | Remove_subtree          of node_ID

src/session/itp_communication.mli

@@ -113,10 +113,11 @@ type ide_request =
   | Add_file_req            of string
   | Set_config_param        of string * int
   | Get_file_contents       of string
-  | Get_task                of node_ID * bool * bool
-  (** [Get_task(id,b, loc)] requests for the text of the task in node [id],
-      when [b] is true then quantified variables and hypotheses are
-      introduced as local definitions, when [loc] is false the locations are not
+  | Get_task                of node_ID * bool * bool * bool
+  (** [Get_task(id,b,c,loc)] requests for the text of the task in node
+      [id].  When [b] is true then quantified variables and hypotheses
+      are introduced as local definitions. When [c] is true then the
+      full context is show.  When [loc] is false the locations are not
       returned *)
   | Focus_req               of node_ID
   (** Focus on a node. The server only sends info about descendants of this ID *)

src/session/itp_server.ml

@@ -256,7 +256,7 @@ let print_request fmt r =
   | Set_config_param(s,i)           -> fprintf fmt "set config param %s %i" s i
   | Get_file_contents _f            -> fprintf fmt "get file contents"
   | Get_first_unproven_node _nid    -> fprintf fmt "get first unproven node"
-  | Get_task(nid,b,loc)             -> fprintf fmt "get task(%d,%b,%b)" nid b loc
+  | Get_task(nid,b,c,loc)           -> fprintf fmt "get task(%d,%b,%b,%b)" nid b c loc
   | Focus_req _nid                  -> fprintf fmt "focus"
   | Unfocus_req                     -> fprintf fmt "unfocus"
   | Remove_subtree _nid             -> fprintf fmt "remove subtree"
@@ -878,7 +878,7 @@ end
     iter_the_files send_node root_node
 
   (* -- send the task -- *)
-  let task_of_id d id do_intros loc =
+  let task_of_id d id do_intros show_full_context loc =
     let task,tables =
       if do_intros then get_task d.cont.controller_session id
       else
@@ -892,15 +892,15 @@ end
       let pr = tables.Trans.printer in
       let apr = tables.Trans.aprinter in
       let module P = (val Pretty.create pr apr pr pr false) in
-      Pp.string_of P.print_sequent task
+      Pp.string_of (if show_full_context then P.print_task else P.print_sequent) task
     in
     task_text, loc_color_list
 
-  let send_task nid do_intros loc =
+  let send_task nid do_intros show_full_context loc =
     let d = get_server_data () in
     match any_from_node_ID nid with
     | APn id ->
-       let s, list_loc = task_of_id d id do_intros loc in
+       let s, list_loc = task_of_id d id do_intros show_full_context loc in
        P.notify (Task (nid, s, list_loc))
     | ATh t ->
        P.notify (Task (nid, "Theory " ^ (theory_name t).Ident.id_string, []))
@@ -908,7 +908,7 @@ end
        let pa = get_proof_attempt_node  d.cont.controller_session pid in
        let parid = pa.parent in
        let name = Pp.string_of Whyconf.print_prover pa.prover in
-       let s, list_loc = task_of_id d parid do_intros loc in
+       let s, list_loc = task_of_id d parid do_intros show_full_context loc in
        P.notify (Task (nid,s ^ "\n====================> Prover: " ^ name ^ "\n", list_loc))
     | AFile f ->
        P.notify (Task (nid, "File " ^ file_name f, []))
@@ -916,7 +916,7 @@ end
        let name = get_transf_name d.cont.controller_session tid in
        let args = get_transf_args d.cont.controller_session tid in
        let parid = get_trans_parent d.cont.controller_session tid in
-       let s, list_loc = task_of_id d parid do_intros loc in
+       let s, list_loc = task_of_id d parid do_intros show_full_context loc in
        P.notify (Task (nid, s ^ "\n====================> Transformation: " ^ String.concat " " (name :: args) ^ "\n", list_loc))
 
   (* -------------------- *)
@@ -1320,7 +1320,7 @@ end
     | Mark_obsolete_req n          -> mark_obsolete n
     | Save_file_req (name, text)   ->
         save_file name text;
-    | Get_task(nid,b, loc)         -> send_task nid b loc
+    | Get_task(nid,b,c,loc)         -> send_task nid b c loc
     | Replay_req                   -> replay_session ()
     | Interrupt_req                -> C.interrupt ()
     | Command_req (nid, cmd)       ->

src/session/json_util.ml

@@ -178,9 +178,9 @@ let print_request_to_json (r: ide_request): Json_base.json =
   | Set_config_param(s,n) ->
       convert_record ["ide_request", cc r;
            "param", String s; "value", Int n]
-  | Get_task(n,b,loc) ->
+  | Get_task(n,b,c,loc) ->
       convert_record ["ide_request", cc r;
-           "node_ID", Int n; "do_intros", Bool b; "loc", Bool loc]
+           "node_ID", Int n; "do_intros", Bool b; "full_context", Bool c ; "loc", Bool loc]
   | Get_file_contents s ->
       convert_record ["ide_request", cc r;
            "file", String s]
@@ -449,8 +449,9 @@ let parse_request (constr: string) j =
   | "Get_task" ->
     let n = get_int (get_field j "node_ID") in
     let b = get_bool_opt (get_field j "do_intros") false in
+    let c = get_bool_opt (get_field j "full_context") false in
     let loc = get_bool_opt (get_field j "loc") false in
-    Get_task(n,b,loc)
+    Get_task(n,b,c,loc)
 
   | "Remove_subtree" ->
     let n = get_int (get_field j "node_ID") in

src/tools/why3shell.ml

@@ -349,7 +349,8 @@ let interp _chout fmt cmd =
     | ["goto"; n] when int_of_string n < !max_ID ->
         cur_id := int_of_string n;
         let b = false (* TODO: allow user to customize printing with intros or not *) in
-        send_request (Get_task(!cur_id,b,false));
+        let c = false (* TODO *) in
+        send_request (Get_task(!cur_id,b,c,false));
         print_session fmt
     | _ ->
         begin
@@ -357,7 +358,8 @@ let interp _chout fmt cmd =
           | "ng" -> cur_id := (!cur_id + 1) mod !max_ID; print_session fmt
           | "g" ->
              let b = false (* TODO: allow user to customize printing with intros or not *) in
-             send_request (Get_task(!cur_id,b,false))
+             let c = false (* TODO *) in
+             send_request (Get_task(!cur_id,b,c,false))
           | "p" -> print_session fmt
           | _ -> send_request (Command_req (!cur_id, cmd))
         end