Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 7e27cce9 authored by MARCHE Claude's avatar MARCHE Claude

webserver: display the session

parent 51226732
......@@ -4,17 +4,32 @@
<head>
<title>Why3</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" type="text/css" href="why3.css" />
<link rel="stylesheet" type="text/css" href="why3_custom.css"/>
</head>
<body id="body" style="background-color:#e0e0a0">
<h1>Test</h1>
<p>
<button id="b1" onClick="sendRequest('list-provers');">List provers</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>
<div id="answers" style="overflow:auto">
<p>Answer zone</p>
<div id="why3-main-panel" class="why3-wide-view">
<div id="why3-editor-container" class="why3-container">
<div id="why3-editor-bg" class="why3-widget"> </div>
<div id="why3-editor" tabindex="-1" ></div>
<p>Editor</p>
</div>
<div id="why3-resize-bar" class="why3-widget" ></div>
<div id="why3-task-list">
<p>Task list</p>
<ul id="session">
</ul>
</div>
<div id="why3-resize-bar" class="why3-widget" ></div>
<div id="answers" style="overflow:auto">
<p>Answer zone</p>
</div>
</div>
<script type="text/javascript" src="why3ide.js"></script>
</body>
......
......@@ -19,13 +19,55 @@ function readBody(xhr) {
return data;
}
function interpNotif(n) {
if (n != null) {
switch (n["notification"]) {
case "None": break;
case "Initialized" :
printAnswer("got initialized: TODO");
break;
case "New_node" :
/*
printAnswer("got new node: nid = " + n.nid + " parent = " + n.parent + " type = " + n.nodetype);
*/
var pid ='session';
if (n.parent != n.nid) {
pid = "nid"+n.parent;
}
else {
var session = document.getElementById(pid);
session.innerHTML = "";
}
var parent = document.getElementById(pid);
var linode = document.createElement("LI");
var textnode = document.createTextNode(n.nodetype + " " + n.name);
linode.appendChild(textnode);
var ulnode = document.createElement("UL");
ulnode.setAttribute('id',"nid"+n.nid);
linode.appendChild(ulnode);
parent.appendChild(linode);
break;
default:
printAnswer("unsupported notification: " + n["notification"]);
}
}
}
function getNotification () {
var req = new XMLHttpRequest();
req.open('GET', 'http://localhost:6789/getNotifications', true);
req.onreadystatechange = function (aEvt) {
if (req.readyState == XMLHttpRequest.DONE) {
if(req.status == 200)
printAnswer("" + readBody(req));
if(req.status == 200) {
var r = readBody(req);
/* printAnswer("r = |" + r + "|"); */
var a = JSON.parse(r);
if (a != null) {
var l = a.length;
/* printAnswer("length = " + l); */
for (var n=0; n < l; n++) interpNotif(a[n])
}
}
else
printAnswer("Erreur " + req.status);
}
......
......@@ -48,13 +48,22 @@ let message_notification n =
| Task_Monitor(a,b,c) ->
Obj ["message_kind",String "Task_Monitor"; "a", Int a; "b", Int b; "c", Int c]
let nodetype t =
match t with
| NRoot -> "root"
| NFile -> "file"
| NTheory -> "theory"
| NTransformation -> "transformation"
| NGoal -> "goal"
| NProofAttempt -> "proofattempt"
let notification n =
match n with
| Node_change(nid,_info) ->
Obj ["notification",String "Node_change"; "nid", Int nid; "info",String "TODO"]
| New_node(nid,parent,_nodetype,_info) ->
| New_node(nid,parent,nt,name) ->
Obj ["notification",String "New_node"; "nid", Int nid; "parent", Int parent;
"nodetype", String "TODO"; "info",String "TODO"]
"nodetype", String (nodetype nt); "name",String name]
| Remove nid ->
Obj ["notification",String "Remove"; "nid", Int nid]
| Initialized _ginfo ->
......@@ -68,8 +77,6 @@ let notification n =
| 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
| "request" ->
......@@ -82,8 +89,11 @@ let handle_script s args =
end
| "getNotifications" ->
let n = P.get_notifications () in
(* if n <> [] then *)
Pp.sprintf "getNotifications: %a@." (Pp.print_list Pp.space print_notification) n
let n =
if n = [] then [Obj ["notification",String "None"]]
else List.map notification n
in
Pp.sprintf "%a@." Json.print (Array n)
| _ -> "bad request"
let plist fmt l =
......@@ -101,6 +111,7 @@ let handler (addr,req) script cont fmt =
eprintf "script: `%s'@." script;
eprintf "cont: `%s'@." cont;
let ans = handle_script script cont in
eprintf "answer: `%s'@." ans;
Wserver.http_header fmt "HTTP/1.0 200 OK";
fprintf fmt "Access-Control-Allow-Origin: *\n";
fprintf fmt "\n"; (* end of header *)
......
......@@ -58,8 +58,8 @@ type value =
let rec print fmt v =
match v with
| Obj l -> map_bindings (fun s -> s) print fmt l
| Array l -> list print fmt l
| Obj l -> if l <> [] then map_bindings (fun s -> s) print fmt l else fprintf fmt "{null}"
| Array l -> if l <> [] then list print fmt l else fprintf fmt "[null]"
| String s -> string fmt s
| Int i -> int fmt i
| Float f -> float fmt f
......
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