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

ITP: fixed dependencies

parent d1bbf7ca
......@@ -1675,27 +1675,6 @@ src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/ide/why3js_ocaml.cmo: src/ide/why3js_ocaml.ml
$(JSOCAMLCW) $(BFLAGS) -c $<
src/ide/why3js_ocaml.byte: $(TRYWHY3CMO) src/ide/why3js_ocaml.cmo
$(JSOCAMLCW) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/ide/why3js_ocaml.js: src/ide/why3js_ocaml.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
src/ide/why3_js.cmo: src/ide/why3_js.ml
$(JSOCAMLCW) $(BFLAGS) -c $<
src/ide/why3_js.byte: $(TRYWHY3CMO) src/ide/why3_js.cmo
$(JSOCAMLCW) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/ide/why3_js.js: src/ide/why3_js.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
opt: lib/why3/why3.cma bin/why3webserver.opt src/ide/why3_js.js
byte: lib/why3/why3.cma bin/why3webserver.byte src/ide/why3_js.js
src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml $(JSOO_DEBUG) +weak.js +nat.js +dynlink.js +toplevel.js $<
......@@ -1720,6 +1699,19 @@ clean::
CLEANDIRS += src/trywhy3
src/ide/why3_js.cmo: src/ide/why3_js.ml
$(JSOCAMLCW) $(BFLAGS) -c $<
src/ide/why3_js.byte: lib/why3/why3.cma src/ide/why3_js.cmo
$(JSOCAMLCW) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/ide/why3_js.js: src/ide/why3_js.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
opt: lib/why3/why3.cma bin/why3webserver.opt src/ide/why3_js.js
byte: lib/why3/why3.cma bin/why3webserver.byte src/ide/why3_js.js
########
# bench
########
......
(* TODO copy of why3js_ocaml.... *)
open Why3
open Itp_communication
......
open Why3
open Itp_communication
let printAnswer s =
let doc = Dom_html.document in
let node = doc##createElement (Js.string "P") in
let textnode = doc##createTextNode (Js.string s) in
Dom.appendChild node textnode;
let answers = doc ## getElementById (Js.string "answers") in
let opt_answers = Js.Opt.to_option answers in
match opt_answers with
| None -> ()
| Some answers ->
Dom.appendChild answers node
let readBody (xhr: XmlHttpRequest.xmlHttpRequest Js.t) =
let data = ref None in
let resType = xhr ## responseType in
printAnswer (Js.to_string resType);
data := Some (xhr ## responseText);
match !data with
| None -> raise Not_found
| Some data -> printAnswer (Js.to_string data); Js.to_string data
(* TEMPORAZRY TODO s todo *)
exception TODO1
exception TODO2
let interpNotif (n: notification) =
let doc = Dom_html.document in
match n with
| Initialized g ->
printAnswer ("Initialized")
| New_node (nid, parent, ntype, name, detached) ->
let pid = ref "session" in
(if (nid != parent) then
pid := "nid" ^ string_of_int parent
else
let ses = doc ## getElementById (Js.string !pid) in
match (Js.Opt.to_option ses) with
| None -> raise TODO1
| Some ses ->
(ses ## innerHTML <- (Js.string ""));
printAnswer "Node 0 reinitialized everything");
let parentnode = doc ## getElementById (Js.string !pid) in
(match (Js.Opt.to_option parentnode) with
| None -> printAnswer !pid; raise TODO2
| Some parentnode ->
let linode = doc ## createElement (Js.string "LI") in
let text = (Json_util.convert_node_type_string ntype) ^ " " ^ name in
let textnode = doc##createTextNode (Js.string text) in
Dom.appendChild linode textnode;
let ulnode = doc ## createElement (Js.string "UL") in
ulnode ## setAttribute (Js.string "id",
Js.string ("nid" ^ string_of_int nid));
Dom.appendChild linode ulnode;
Dom.appendChild parentnode linode;
printAnswer "new_node") (* TODO *)
| _ -> printAnswer "Unsupported" (* TODO *)
(*
<div oncontextmenu="javascript:alert('success!');return false;">
Lorem Ipsum
</div>
el.addEventListener('contextmenu', function(ev) {
ev.preventDefault();
alert('success!');
return false;
}, false);
*)
(* TODO remove this *)
exception NoNotification
let interpNotifications l =
match l with
| [] -> raise NoNotification
| l -> List.iter interpNotif l
let getNotification2 () =
let xhr = XmlHttpRequest.create () in
let onreadystatechange () =
if xhr ## readyState == XmlHttpRequest.DONE then
if xhr ## status == 200 then
let r = readBody xhr in
printAnswer ("r = |" ^ r ^ "|"); (* TODO *)
let nl = Json_util.parse_list_notification r in
interpNotifications nl
(* TODO *)
else
raise NoNotification
(* TODO printAnswer ("Erreur" ^ string_of_int xhr##status)*)
in
(xhr ## onreadystatechange <-
(Js.wrap_callback onreadystatechange));
xhr ## overrideMimeType (Js.string "text/json");
let _ = xhr ## _open (Js.string "GET",
Js.string "http://localhost:6789/getNotifications", Js._true) in
xhr ## send (Js.null)
let sendRequest r =
let r = Js.to_string r in
let xhr = XmlHttpRequest.create () in
let onreadystatechange () =
if xhr ## readyState == XmlHttpRequest.DONE then
if xhr ## status == 200 then
printAnswer (readBody xhr)
else
printAnswer ("Erreur " ^ string_of_int (xhr ## status)) in
xhr ## overrideMimeType (Js.string "text/json");
let _ = xhr ## _open (Js.string "GET",
Js.string ("http://localhost:6789/request?"^r), Js._true) in
xhr ## onreadystatechange <- (Js.wrap_callback onreadystatechange);
xhr ## send (Js.null)
let notifHandler = ref None
let startNotificationHandler () =
if (!notifHandler = None) then
notifHandler := Some (Dom_html.window ## setInterval
(Js.wrap_callback getNotification2, Js.float 1000.0))
let stopNotificationHandler () =
match !notifHandler with
| None -> ()
| Some n -> Dom_html.window ## clearInterval (n); notifHandler := None
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