Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit ae868e72 authored by Sylvain Dailler's avatar Sylvain Dailler

Displaying of background colors in source loc according to current task.

Premises, goals and neg_premises of the task can now be shown directly on
the source code.
Notification Task was extended with a list of couple location, color.
parent b675e0b9
......@@ -540,7 +540,7 @@ let interpNotif (n: notification) =
PE.error_print_msg "Notification File_contents not handled yet"
| Next_Unproven_Node_Id (_nid1,_nid2) ->
PE.error_print_msg "Notification Next_Unproven_Node_Id not handled yet"
| Task (nid, task) ->
| Task (nid, task, _list_loc) -> (* TODO add color on sources *)
Hashtbl.add TaskList.printed_task_list (string_of_int nid) task
| Remove nid ->
TaskList.remove_node (string_of_int nid)
......
......@@ -228,6 +228,38 @@ let try_convert s =
s
with Glib.Convert.Error _ as e -> Printexc.to_string e
(****************************)
(* Color handling in source *)
(****************************)
(* For each view, we have to recreate the tags *)
let create_colors v =
let premise_tag (v: GSourceView2.source_view) = v#buffer#create_tag
~name:"premise_tag" [`BACKGROUND gconfig.premise_color] in
let neg_premise_tag (v: GSourceView2.source_view) = v#buffer#create_tag
~name:"neg_premise_tag" [`BACKGROUND gconfig.neg_premise_color] in
let goal_tag (v: GSourceView2.source_view) = v#buffer#create_tag
~name:"goal_tag" [`BACKGROUND gconfig.goal_color] in
let error_tag (v: GSourceView2.source_view) = v#buffer#create_tag
~name:"error_tag" [`BACKGROUND gconfig.error_color] in
let _ : GText.tag = premise_tag v in
let _ : GText.tag = neg_premise_tag v in
let _ : GText.tag = goal_tag v in
let _ : GText.tag = error_tag v in
()
(* Erase all the source location tags in a source file *)
let erase_color_loc (v:GSourceView2.source_view) =
let buf = v#buffer in
buf#remove_tag_by_name "premise_tag" ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag_by_name "neg_premise_tag" ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag_by_name "goal_tag" ~start:buf#start_iter ~stop:buf#end_iter;
buf#remove_tag_by_name "error_tag" ~start:buf#start_iter ~stop:buf#end_iter
(*******************)
(* Graphical tools *)
(*******************)
......@@ -253,6 +285,15 @@ let exit_function_unsafe () =
let source_view_table : (int * GSourceView2.source_view * bool ref * GMisc.label) Hstr.t =
Hstr.create 14
(* The corresponding file does not have a source view *)
exception Nosourceview of string
(* This returns the source_view of a file *)
let get_source_view (file: string) : GSourceView2.source_view =
match Hstr.find source_view_table file with
| (_, v, _, _) -> v
| exception Not_found -> raise (Nosourceview file)
(* Saving function for sources *)
let save_sources () =
Hstr.iter
......@@ -670,6 +711,9 @@ let create_source_view =
with Not_found -> () ) in
Gconfig.add_modifiable_mono_font_view source_view#misc;
source_view#source_buffer#set_language why_lang;
(* We have to create the tags for background colors for each view.
They are not reusable from the other views. *)
create_colors source_view;
Gconfig.set_fonts ()
end in
create_source_view
......@@ -817,6 +861,46 @@ let (_ : GtkSignal.id) =
replay_menu_item#connect#activate
~callback:(fun () -> send_request Replay_req)
(********************)
(* Locations colors *)
(********************)
(* This apply a background [color] on a location given by its file view [v] line
[l] beginning char [b] and end char [e]. *)
let color_loc (v:GSourceView2.source_view) ~color l b e =
let buf = v#buffer in
let top = buf#start_iter in
let start = top#forward_lines (l-1) in
let start = start#forward_chars b in
let stop = start#forward_chars (e-b) in
buf#apply_tag_by_name ~start ~stop color
let convert_color (color: color): string =
match color with
| Neg_premise_color -> "neg_premise_tag"
| Premise_color -> "premise_tag"
| Goal_color -> "goal_tag"
(* Add a color tag on the right locations on the correct file.
If the file was not open yet, nothing is done *)
let color_loc ~color loc =
let f, l, b, e = Loc.get loc in
try
let v: GSourceView2.source_view = get_source_view f in
let color = convert_color color in
color_loc ~color v l b e
with
| Nosourceview _ ->
(* If the file is not present do nothing *)
()
(* Erase the colors and apply the colors given by l (which come from the task)
to appropriate source files *)
let apply_loc_on_source (l: (Loc.position * color) list) =
Hstr.iter (fun _ (_, v, _, _) -> erase_color_loc v) source_view_table;
List.iter (fun (loc, color) ->
color_loc ~color loc) l
(**************************)
(* Graphical proof status *)
(**************************)
......@@ -1031,7 +1115,7 @@ let on_selected_row r =
task_view#source_buffer#set_text ""
else
send_request (Get_task id)
| _ -> send_request (Get_task id)
| _ -> send_request (Get_task id)
with
| Not_found -> task_view#source_buffer#set_text ""
......@@ -1283,10 +1367,11 @@ let treat_notification n =
if !quit_on_saved = true then
exit_function_safe ()
| Message (msg) -> treat_message_notification msg
| Task (id, s) ->
| Task (id, s, list_loc) ->
if_selected_alone
id
(fun _ -> task_view#source_buffer#set_text s;
apply_loc_on_source list_loc;
(* scroll to end of text *)
task_view#scroll_to_mark `INSERT)
| File_contents (file_name, content) ->
......
......@@ -45,6 +45,14 @@ type node_type =
| NGoal
| NProofAttempt
(* Used to give colors to the parts of the source code that corresponds to the
following property in the current task. For example, the code corresponding
to the goal of the task will have Goal_color in the source code. *)
type color =
| Neg_premise_color
| Premise_color
| Goal_color
type update_info =
| Proved of bool
| Proof_status_change of
......@@ -72,8 +80,10 @@ type notification =
(* an informative message, can be an error message *)
| Dead of string
(* server exited *)
| Task of node_ID * string
(* the node_ID's task *)
| Task of node_ID * string * (Loc.position * color) list
(* the node_ID's task together with information that allows to color the
source code corresponding to different part of the task (premise, goal,
etc) *)
| File_contents of string * string
(* File_contents (filename, contents) *)
......
......@@ -51,6 +51,14 @@ type node_type =
| NGoal
| NProofAttempt
(* Used to give colors to the parts of the source code that corresponds to the
following property in the current task. For example, the code corresponding
to the goal of the task will have Goal_color in the source code. *)
type color =
| Neg_premise_color
| Premise_color
| Goal_color
type update_info =
| Proved of bool
| Proof_status_change of
......@@ -78,8 +86,10 @@ type notification =
(* an informative message, can be an error message *)
| Dead of string
(* server exited *)
| Task of node_ID * string
(* the node_ID's task *)
| Task of node_ID * string * (Loc.position * color) list
(* the node_ID's task together with information that allows to color the
source code corresponding to different part of the task (premise, goal,
etc) *)
| File_contents of string * string
(* File_contents (filename, contents) *)
......
......@@ -282,6 +282,17 @@ let print_msg fmt m =
| Error s -> fprintf fmt "%s" s
| Open_File_Error s -> fprintf fmt "%s" s
(* TODO ad hoc printing. Should reuse print_loc. *)
let print_loc fmt (loc: Loc.position) =
let (f,l,b,e) = Loc.get loc in
fprintf fmt "File \"%s\", line %d, characters %d-%d" f l b e
let print_list_loc fmt l =
Pp.print_list
(fun _fmt () -> ())
(fun fmt (loc, _c) -> Format.fprintf fmt "(%a, color)" print_loc loc)
fmt l
let print_notify fmt n =
match n with
| Node_change (ni, nf) ->
......@@ -299,7 +310,9 @@ let print_notify fmt n =
print_msg fmt msg
| Dead s -> fprintf fmt "dead :%s" s
| File_contents (_f, _s) -> fprintf fmt "file contents"
| Task (_ni, _s) -> fprintf fmt "task"
| Task (ni, _s, list_loc) ->
fprintf fmt "task for node_ID %d which contains a list of loc %a"
ni print_list_loc list_loc
module type Protocol = sig
val get_requests : unit -> ide_request list
......@@ -367,6 +380,72 @@ let () =
exit 1
| Some x -> x
(*******************************)
(* Compute color for locations *)
(*******************************)
(* This section is used to get colored source as a function of the task *)
(* These functions append stuff to a list which will then be passed to the
Task notification. *)
let color_loc list ~color ~loc =
let d = get_server_data () in
let (f,l,b,e) = Loc.get loc in
let f = Sysutil.relativize_filename
(Session_itp.get_dir d.cont.controller_session) f in
let loc = Loc.user_position f l b e in
list := (loc, color) :: !list
let rec color_locs list ~color formula =
let b = ref false in
Opt.iter (fun loc -> color_loc list ~color ~loc; b := true) formula.Term.t_loc;
Term.t_fold (fun b subf -> color_locs list ~color subf || b) !b formula
let rec color_t_locs list f =
let premise_tag = function
| { Term.t_node = Term.Tnot _; t_loc = None } -> Neg_premise_color
| _ -> Premise_color
in
match f.Term.t_node with
| Term.Tbinop (Term.Timplies,f1,f2) ->
let b = color_locs list ~color:(premise_tag f1) f1 in
color_t_locs list f2 || b
| Term.Tlet (t,fb) ->
let _,f1 = Term.t_open_bound fb in
let b = color_locs list ~color:(premise_tag t) t in
color_t_locs list f1 || b
| Term.Tquant (Term.Tforall,fq) ->
let _,_,f1 = Term.t_open_quant fq in
color_t_locs list f1
| _ ->
color_locs list ~color:Goal_color f
exception No_loc_on_goal
let color_goal list loc =
match loc with
| None -> raise No_loc_on_goal
| Some loc -> color_loc list ~color:Goal_color ~loc
let get_locations list (task: Task.task) =
let goal_id : Ident.ident = (Task.task_goal task).Decl.pr_name in
color_goal list goal_id.Ident.id_loc;
match task with
| Some
{ Task.task_decl =
{ Theory.td_node =
Theory.Decl { Decl.d_node = Decl.Dprop (Decl.Pgoal, _, f)}}} ->
if not (color_t_locs list f) then
Opt.iter (fun loc -> color_loc list ~color:Goal_color ~loc) goal_id.Ident.id_loc
| _ ->
assert false
let get_locations t =
let l = ref [] in
get_locations l t;
!l
(*********************)
(* File input/output *)
(*********************)
......@@ -715,36 +794,39 @@ let () =
get_node_proved node_id any in
iter_the_files send_node root_node
(* -- send the task -- *)
let task_of_id d id =
let task = get_task d.cont.controller_session id in
let tables = get_tables d.cont.controller_session id in
(* This function also send source locations associated to the task *)
let loc_color_list = get_locations task in
Pp.string_of
(Driver.print_task ~cntexample:false ?name_table:tables d.task_driver)
task
task, loc_color_list
let send_task nid =
let d = get_server_data () in
match any_from_node_ID nid with
| APn id ->
let s = task_of_id d id in
P.notify (Task (nid,s))
let s, list_loc = task_of_id d id in
P.notify (Task (nid, s, list_loc))
| ATh t ->
P.notify (Task (nid, "Theory " ^ (theory_name t).Ident.id_string))
P.notify (Task (nid, "Theory " ^ (theory_name t).Ident.id_string, []))
| APa pid ->
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 = task_of_id d parid in
P.notify (Task (nid,s ^ "\n====================> Prover: " ^ name ^ "\n"))
let s, list_loc = task_of_id d parid in
P.notify (Task (nid,s ^ "\n====================> Prover: " ^ name ^ "\n", list_loc))
| AFile f ->
P.notify (Task (nid, "File " ^ f.file_name))
P.notify (Task (nid, "File " ^ f.file_name, []))
| ATn tid ->
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 = task_of_id d parid in
P.notify (Task (nid, s ^ "\n====================> Transformation: " ^ String.concat " " (name :: args) ^ "\n"))
let s, list_loc = task_of_id d parid in
P.notify (Task (nid, s ^ "\n====================> Transformation: " ^ String.concat " " (name :: args) ^ "\n", list_loc))
(* -------------------- *)
......
......@@ -270,6 +270,59 @@ let convert_message (m: message_notification) =
Obj ["mess_notif", cc m;
"information", String s]
let convert_color (color: color) : Json_base.value =
Json_base.String (
match color with
| Neg_premise_color -> "Neg_premise_color"
| Premise_color -> "Premise_color"
| Goal_color -> "Goal_color")
let convert_loc (loc: Loc.position) : Json_base.value =
let (file, line, col1, col2) = Loc.get loc in
Json_base.Obj ["file", Json_base.String file;
"line", Json_base.Int line;
"col1", Json_base.Int col1;
"col2", Json_base.Int col2]
let convert_loc_color (loc,color: Loc.position * color) : Json_base.value =
let loc = convert_loc loc in
let color = convert_color color in
Json_base.Obj ["loc", loc; "color", color]
let convert_list_loc (l: (Loc.position * color) list) : Json_base.value =
let list_of_loc = List.map convert_loc_color l in
Json_base.Array list_of_loc
exception Notcolor
let parse_color (j: Json_base.value) : color =
match j with
| String "Neg_premise_color" -> Neg_premise_color
| String "Premise_color" -> Premise_color
| String "Goal_color" -> Goal_color
| _ -> raise Notcolor
exception Notposition
let parse_loc (j: Json_base.value) : Loc.position =
match j with
| Obj ["file", String file;
"line", Int line;
"col1", Int col1;
"col2", Int col2] ->
Loc.user_position file line col1 col2
| _ -> raise Notposition
let parse_loc_color (j: Json_base.value): Loc.position * color =
match j with
| Obj ["loc", loc; "color", color] -> (parse_loc loc, parse_color color)
| _ -> raise Notposition
let parse_list_loc (j: Json_base.value): (Loc.position * color) list =
match j with
| Array l -> List.map parse_loc_color l
| _ -> raise Notposition
let print_notification_to_json (n: notification): Json_base.value =
let cc = convert_notification_constructor in
match n with
......@@ -302,10 +355,11 @@ let print_notification_to_json (n: notification): Json_base.value =
| Dead s ->
Obj ["notification", cc n;
"message", String s]
| Task (nid, s) ->
| Task (nid, s, list_loc) ->
Obj ["notification", cc n;
"node_ID", Int nid;
"task", String s]
"task", String s;
"list_loc", convert_list_loc list_loc]
| File_contents (f, s) ->
Obj ["notification", cc n;
"file", String f;
......@@ -575,8 +629,9 @@ let parse_notification constr l =
| "Dead", ["message", String s] ->
Dead s
| "Task", ["node_ID", Int nid;
"task", String s] ->
Task (nid, s)
"task", String s;
"loc_list", l] ->
Task (nid, s, parse_list_loc l)
| "Next_Unproven_Node_Id", [ "node_ID", Int nid1;
"node_ID", Int nid2 ] ->
Next_Unproven_Node_Id (nid1, nid2)
......
......@@ -242,7 +242,8 @@ let treat_notification fmt n =
fprintf fmt "got a Dead notification not yet supported@."
| File_contents _ -> assert false (* TODO *)
| Next_Unproven_Node_Id _ -> assert false (* TODO *)
| Task (id, s) ->
| Task (id, s, _list_loc) ->
(* coloring the source is useless in shell *)
try
let node = Hnode.find nodes id in
node.node_task <- Some s;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment