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 51226732 authored by MARCHE Claude's avatar MARCHE Claude

Json: add a concrete datatype

parent 6de885b6
......@@ -9,7 +9,7 @@
<h1>Test</h1>
<p>
<button id="b1" onClick="sendRequest('list-provers');">List provers</button>
<button id="b2" onClick="sendRequest('bouton2');">Button 2</button>
<button id="b2" onClick="sendRequest('session');">Button 2</button>
<button id="b3" onclick="startNotificationHandler()">Start notification handler</button>
<button id="b4" onclick="stopNotificationHandler()">Stop notification handler</button>
</p>
......
......@@ -31,31 +31,44 @@ let interp_request args =
| "list-provers" -> (Command_req (root_node,"list-provers"))
| _ -> invalid_arg "Why3web.interp_request"
let print_message_notification fmt n =
open Json
let message_notification n =
match n with
| Error _s -> ()
| Open_File_Error _s -> ()
| Proof_error(_nid,_s) -> ()
| Transf_error(_nid,_s) -> ()
| Strat_error(_nid,_s) -> ()
| Replay_Info(_s) -> ()
| Query_Info(nid,s) -> fprintf fmt "kind=\"query_info\", node=\"%d\", text=\"%s\"" nid s
| Query_Error(nid,s) -> fprintf fmt "kind=\"query_error\", node=\"%d\", text=\"%s\"" nid s
| Help s -> fprintf fmt "kind=\"help\", text=\"%s\"" s
| Information s -> fprintf fmt "kind=\"information\", text=\"%s\"" s
| Task_Monitor(_a,_b,_c) -> ()
let print_notification fmt n =
| Error s -> Obj ["message_kind",String "Error"; "msg",String s]
| Open_File_Error s -> Obj ["message_kind",String "Open_File_Error"; "msg", String s]
| Proof_error(nid,s) -> Obj ["message_kind",String "Proof_error"; "nid", Int nid; "msg", String s]
| Transf_error(nid,s) -> Obj ["message_kind",String "Transf_error"; "nid", Int nid; "msg", String s]
| Strat_error(nid,s) -> Obj ["message_kind",String "Strat_error"; "nid", Int nid; "msg", String s]
| Replay_Info s -> Obj ["message_kind",String "Replay_info"; "msg", String s]
| Query_Info(nid,s) -> Obj ["message_kind",String "Query_info"; "nid", Int nid; "msg", String s]
| Query_Error(nid,s) -> Obj ["message_kind",String "Query_error"; "nid", Int nid; "msg", String s]
| Help s -> Obj ["message_kind",String "Help"; "msg", String s]
| Information s -> Obj ["message_kind",String "Information"; "msg", String s]
| Task_Monitor(a,b,c) ->
Obj ["message_kind",String "Task_Monitor"; "a", Int a; "b", Int b; "c", Int c]
let notification n =
match n with
| Node_change(_nid,_info) -> ()
| New_node(_nid,_nid',_nodetype,_info) -> ()
| Remove(_nid) -> ()
| Initialized(_ginfo) -> ()
| Saved -> ()
| Message n -> fprintf fmt "{ notification=\"message=\"; %a }"
print_message_notification n
| Dead _s -> ()
| Task(_nid,_task) -> ()
| Node_change(nid,_info) ->
Obj ["notification",String "Node_change"; "nid", Int nid; "info",String "TODO"]
| New_node(nid,parent,_nodetype,_info) ->
Obj ["notification",String "New_node"; "nid", Int nid; "parent", Int parent;
"nodetype", String "TODO"; "info",String "TODO"]
| Remove nid ->
Obj ["notification",String "Remove"; "nid", Int nid]
| Initialized _ginfo ->
Obj ["notification",String "Initialized"; "ginfo", String "TODO"]
| Saved ->
Obj ["notification",String "Saved"]
| Message n ->
Obj ["notification",String "Message"; "msg", message_notification n]
| Dead s ->
Obj ["notification",String "Dead"; "msg", String s]
| Task(nid,_task) ->
Obj ["notification",String "Task"; "nid", Int nid; "task", String "TODO"]
let print_notification fmt n = Json.print fmt (notification n)
let handle_script s args =
match s with
......@@ -131,7 +144,7 @@ let usage_str = sprintf
let () =
let config, base_config, env =
let config, _base_config, env =
Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str
in
if Queue.is_empty files then
......
......@@ -100,7 +100,7 @@ module Task =
let clear_warnings () = warnings := []
let () =
Warning.set_hook (fun ?(loc=(Loc.user_position "" 1 0 0)) msg ->
let _, a,b,c = Loc.get loc in
let _, a,b,_ = Loc.get loc in
warnings := ((a-1,b), msg) :: !warnings)
......@@ -139,7 +139,7 @@ module Task =
let task_to_string t =
ignore (flush_str_formatter ());
Driver.print_task alt_ergo_driver str_formatter None t;
Driver.print_task alt_ergo_driver str_formatter t;
flush_str_formatter ()
let gen_id =
......
......@@ -9,6 +9,8 @@
(* *)
(********************************************************************)
open Format
let string fmt s =
let b = Buffer.create (2 * String.length s) in
Buffer.add_char b '"';
......@@ -19,18 +21,18 @@ let string fmt s =
| c -> Buffer.add_char b c
done;
Buffer.add_char b '"';
Format.fprintf fmt "%s" (Buffer.contents b)
fprintf fmt "%s" (Buffer.contents b)
let int fmt d = Format.fprintf fmt "%d" d
let bool fmt b = Format.fprintf fmt "%b" b
let float fmt f = Format.fprintf fmt "%f" f
let int fmt d = fprintf fmt "%d" d
let bool fmt b = fprintf fmt "%b" b
let float fmt f = fprintf fmt "%f" f
(* TODO check that you can print a floating point number like this in JSON *)
let print_json_field key value_pr fmt value =
Format.fprintf fmt "%a : %a " string key value_pr value
fprintf fmt "%a:%a" string key value_pr value
let list pr fmt l =
if l = [] then Format.fprintf fmt "[]"
if l = [] then fprintf fmt "[]"
else
Pp.print_list_delim ~start:Pp.lsquare ~stop:Pp.rsquare ~sep:Pp.comma
pr fmt l
......@@ -40,7 +42,29 @@ let print_map_binding key_to_str value_pr fmt binding =
print_json_field (key_to_str key) value_pr fmt value
let map_bindings key_to_str value_pr fmt map_bindings =
if map_bindings = [] then Format.fprintf fmt "{}"
if map_bindings = [] then fprintf fmt "{}"
else
Pp.print_list_delim ~start:Pp.lbrace ~stop:Pp.rbrace ~sep:Pp.comma
(print_map_binding key_to_str value_pr) fmt map_bindings
type value =
| Obj of (string * value) list
| Array of value list
| String of string
| Int of int
| Float of float
| Bool of bool
| Null
let rec print fmt v =
match v with
| Obj l -> map_bindings (fun s -> s) print fmt l
| Array l -> list print fmt l
| String s -> string fmt s
| Int i -> int fmt i
| Float f -> float fmt f
| Bool b -> bool fmt b
| Null -> fprintf fmt "null"
let parse _s = failwith "Json.parse not yet implemented"
......@@ -42,3 +42,16 @@ val print_json_field :
string -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a -> unit
(* given a field name, a value and a printer for the value, print a json
mapping (field assignment). Do not print anything else. *)
type value =
| Obj of (string * value) list
| Array of value list
| String of string
| Int of int
| Float of float
| Bool of bool
| Null
val print : Format.formatter -> value -> unit
val parse : string -> value
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