Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

Commit a5c1e25b authored by MARCHE Claude's avatar MARCHE Claude
Browse files

improve log of web interface

parent 4a6dca53
......@@ -540,6 +540,7 @@ let remove_node n =
end
let interpNotif (n: notification) =
Format.kasprintf PE.log_print_msg "interpNotif: %a@\n@." Itp_communication.print_notify n;
match n with
| Reset_whole_tree -> TaskList.clear ()
| Initialized _g ->
......@@ -632,10 +633,6 @@ let getNotification2 () =
log ("ERROR in getNotification2: Json_util.parse_list_notification raised " ^ Printexc.to_string e ^
" on the following notification: " ^ r); []
in
(* TODO: make a nicer log *)
if nl != [] then
PE.printAnswer ("r = |" ^ r ^ "|");
(**)
interpNotifications nl
else
()
......
......@@ -16,7 +16,6 @@ open Stdlib
open Ide_utils
open History
open Itp_communication
open Itp_server
external reset_gc : unit -> unit = "ml_reset_gc"
......
......@@ -131,3 +131,79 @@ let modify_session (r: ide_request) =
| Get_task _ | Save_file_req _ | Get_first_unproven_node _
| Save_req | Exit_req | Get_global_infos
| Interrupt_req | Focus_req _ | Unfocus_req -> false
(* Debugging functions *)
open Format
let print_request fmt r =
match r with
| Command_req (_nid, s) -> fprintf fmt "command \"%s\"" s
| Add_file_req f -> fprintf fmt "open file %s" f
| 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
| Focus_req _nid -> fprintf fmt "focus"
| Unfocus_req -> fprintf fmt "unfocus"
| Remove_subtree _nid -> fprintf fmt "remove subtree"
| Copy_paste _ -> fprintf fmt "copy paste"
| Save_file_req _ -> fprintf fmt "save file"
| Save_req -> fprintf fmt "save"
| Reload_req -> fprintf fmt "reload"
| Exit_req -> fprintf fmt "exit"
| Interrupt_req -> fprintf fmt "interrupt"
| Get_global_infos -> fprintf fmt "get_global_infos"
let print_msg fmt m =
match m with
| Proof_error (_ids, s) -> fprintf fmt "proof error %s" s
| Transf_error (_ids, _tr, _args, _loc, s, _d) -> fprintf fmt "transf error %s" s
| Strat_error (_ids, s) -> fprintf fmt "start error %s" s
| Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s
| Query_Error (_ids, s) -> fprintf fmt "query error %s" s
| Information s -> fprintf fmt "info %s" s
| Task_Monitor _ -> fprintf fmt "task montor"
| Parse_Or_Type_Error (_, _, s) -> fprintf fmt "parse_or_type_error:\n %s" s
| File_Saved s -> fprintf fmt "file saved %s" s
| 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
| Reset_whole_tree -> fprintf fmt "reset whole tree"
| Node_change (ni, nf) ->
begin
match nf with
| Proved b -> fprintf fmt "node change %d: proved=%b" ni b
| Name_change n -> fprintf fmt "node change %d: renamed to '%s'" ni n
| Proof_status_change(st,b,_lim) ->
fprintf fmt "node change %d Proof_status_change res=%a obsolete=%b limits=<TODO>"
ni Controller_itp.print_status st b
end
| New_node (ni, pni, _nt, _nf, _d) -> fprintf fmt "new node = %d, parent = %d" ni pni
| Remove _ni -> fprintf fmt "remove"
| Next_Unproven_Node_Id (ni, nj) -> fprintf fmt "next unproven node_id from %d is %d" ni nj
| Initialized _gi -> fprintf fmt "initialized"
| Saved -> fprintf fmt "saved"
| Message msg ->
print_msg fmt msg
| Dead s -> fprintf fmt "dead :%s" s
| File_contents (_f, _s) -> fprintf fmt "file contents"
| Source_and_ce (_s, _list_loc) -> fprintf fmt "source and ce"
| Task (ni, _s, list_loc) ->
fprintf fmt "task for node_ID %d which contains a list of %d locations"
ni (List.length list_loc) (* print_list_loc list_loc *)
......@@ -141,3 +141,8 @@ type ide_request =
(* Return true if the request modify the session *)
val modify_session: ide_request -> bool
val print_request: Format.formatter -> ide_request -> unit
val print_msg: Format.formatter -> message_notification -> unit
val print_notify: Format.formatter -> notification -> unit
......@@ -262,78 +262,6 @@ let get_exception_message ses id e =
(Pp.sprintf "%a" (bypass_pretty ses id) e), Loc.dummy_position, ""
(* Debugging functions *)
let print_request fmt r =
match r with
| Command_req (_nid, s) -> fprintf fmt "command \"%s\"" s
| Add_file_req f -> fprintf fmt "open file %s" f
| 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
| Focus_req _nid -> fprintf fmt "focus"
| Unfocus_req -> fprintf fmt "unfocus"
| Remove_subtree _nid -> fprintf fmt "remove subtree"
| Copy_paste _ -> fprintf fmt "copy paste"
| Save_file_req _ -> fprintf fmt "save file"
| Save_req -> fprintf fmt "save"
| Reload_req -> fprintf fmt "reload"
| Exit_req -> fprintf fmt "exit"
| Interrupt_req -> fprintf fmt "interrupt"
| Get_global_infos -> fprintf fmt "get_global_infos"
let print_msg fmt m =
match m with
| Proof_error (_ids, s) -> fprintf fmt "proof error %s" s
| Transf_error (_ids, _tr, _args, _loc, s, _d) -> fprintf fmt "transf error %s" s
| Strat_error (_ids, s) -> fprintf fmt "start error %s" s
| Replay_Info s -> fprintf fmt "replay info %s" s
| Query_Info (_ids, s) -> fprintf fmt "query info %s" s
| Query_Error (_ids, s) -> fprintf fmt "query error %s" s
| Information s -> fprintf fmt "info %s" s
| Task_Monitor _ -> fprintf fmt "task montor"
| Parse_Or_Type_Error (_, _, s) -> fprintf fmt "parse_or_type_error:\n %s" s
| File_Saved s -> fprintf fmt "file saved %s" s
| 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
| Reset_whole_tree -> fprintf fmt "reset whole tree"
| Node_change (ni, nf) ->
begin
match nf with
| Proved b -> fprintf fmt "node change %d: proved=%b" ni b
| Name_change n -> fprintf fmt "node change %d: renamed to '%s'" ni n
| Proof_status_change(st,b,_lim) ->
fprintf fmt "node change %d Proof_status_change res=%a obsolete=%b limits=<TODO>"
ni Controller_itp.print_status st b
end
| New_node (ni, pni, _nt, _nf, _d) -> fprintf fmt "new node = %d, parent = %d" ni pni
| Remove _ni -> fprintf fmt "remove"
| Next_Unproven_Node_Id (ni, nj) -> fprintf fmt "next unproven node_id from %d is %d" ni nj
| Initialized _gi -> fprintf fmt "initialized"
| Saved -> fprintf fmt "saved"
| Message msg ->
print_msg fmt msg
| Dead s -> fprintf fmt "dead :%s" s
| File_contents (_f, _s) -> fprintf fmt "file contents"
| Source_and_ce (_s, _list_loc) -> fprintf fmt "source and ce"
| 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
val notify : notification -> unit
......@@ -1394,7 +1322,7 @@ end
P.notify (Message (Error (Pp.string_of
(fun fmt r -> Format.fprintf fmt
"The following request refer to obsolete node_ids:\n %a\n"
print_request r) r)))
Itp_communication.print_request r) r)))
end
else
try (
......
......@@ -11,10 +11,6 @@
open Itp_communication
val print_request: Format.formatter -> ide_request -> unit
val print_msg: Format.formatter -> message_notification -> unit
val print_notify: Format.formatter -> notification -> unit
(* The server part of the protocol *)
module type Protocol = sig
......
......@@ -18,7 +18,6 @@ open Why3
open Unix_scheduler
open Format
open Itp_communication
open Itp_server
(*************************)
(* Protocol of the shell *)
......
......@@ -196,6 +196,7 @@ let string_of_wnl p x =
Buffer.contents b
let sprintf p =
(* useless: this is the same as Format.asprintf *)
let b = Buffer.create 100 in
let fmt = formatter_of_buffer b in
kfprintf (fun fmt -> Format.pp_print_flush fmt (); Buffer.contents b) fmt p
......
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