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 d5116397 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

[trywhy3] : allow trywhy3 to be run from a file:/// url (i.e. by opening

	  trywhy3.html from the local filesystem instead of loading it
	  from a web server). Only tested with firefox and chrome.
parent 935f9cf7
......@@ -1525,7 +1525,7 @@ ALTERGOMODS=util/numsNumbers util/numbers \
main/frontend
ALTERGOCMO=$(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
TRYWHY3CMO=lib/why3/why3.cma
TRYWHY3FILES=trywhy3.js why3_worker.js alt_ergo_worker.js trywhy3.html trywhy3.css \
TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
README examples/ \
trywhy3_custom.css gen_index.sh fontawesome/css/font-awesome.min.css \
fontawesome/fonts/FontAwesome.otf fontawesome/fonts/fontawesome-webfont.svg \
......@@ -1539,8 +1539,13 @@ trywhy3_package: trywhy3
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml +weak.js +nat.js $^
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js
js_of_ocaml -I src/trywhy3 \
--file=why3_worker.js:/ \
--file=alt_ergo_worker.js:/ \
--file=examples/index.txt:/ \
`find src/trywhy3/examples \( -name "*.mlw" -o -name "*.why" \) -printf " --file=examples/%P:/"` \
+weak.js +nat.js $<
src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
......@@ -1550,14 +1555,14 @@ src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
+weak.js +nat.js $^
+weak.js +nat.js $<
src/trywhy3/why3_worker.byte: $(TRYWHY3CMO) src/trywhy3/worker_proto.cmo src/trywhy3/why3_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
src/trywhy3/alt_ergo_worker.js: src/trywhy3/alt_ergo_worker.byte
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $^
js_of_ocaml +weak.js +nat.js +dynlink.js +toplevel.js $<
src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) src/trywhy3/worker_proto.cmo src/trywhy3/alt_ergo_worker.cmo
$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
......
......@@ -40,7 +40,15 @@ Instructions to build TryWhy3
ALTERGODIR=src/trywhy3/alt-ergo-1.00-private-2015-01-29
** compile with
** [optional] If you want to build a standalone trywhy3 that can be
run without a Webserver, the example files must be present at
compile time. See the step 'To add predefined examples' in the
'customization' section below and populate the examples/
directory of the trywhy3 source directory accordingly *before*
building trywhy3.
** compile with
make trywhy3
......@@ -54,9 +62,11 @@ Instructions to build TryWhy3
You may want to add a symlink from index.html to trywhy3.html (or rename the file).
* customization
** install a file trywhy3_help.html that will be shown when clicking the help button.
** install a file trywhy3_help.html that will be shown when clicking
the help button.
** To change the theme used by the ace editor widget, add the
relevant theme-*.js file to the ace-builds/src-min-noconflict/
......@@ -73,3 +83,9 @@ Instructions to build TryWhy3
cp some_file.mlw examples/
cd examples/
../gen_index.sh *.mlw > index.txt
** [optional] If you want trywhy3 to only use its embedded files
(e.g. to run it simply by opening trywhy3.html with a web browser
instead of putting it on a webserver), change the variable
declaration 'var load_embedded_files = false;' to
'var load_embedded_files = true;' in the header section of trywhy3.html.
\ No newline at end of file
......@@ -6,10 +6,12 @@
<link rel="stylesheet" type="text/css" href="trywhy3.css" />
<link rel="stylesheet" type="text/css" href="trywhy3_custom.css"/>
<script defer="defer" src="ace-builds/src-min-noconflict/ace.js"
type="text/javascript" charset="utf-8"></script>
<script type="text/javascript">
var load_embedded_files = false;
var editor_theme = "ace/theme/chrome";
var editor_mode = "ace/mode/why3";
var library_index = "examples/index.txt";
......
......@@ -24,10 +24,29 @@ let get_global ident =
let int_of_js_string s = int_of_string (Js.to_string s)
let blob_url_of_string s =
let s = JSU.inject (Js.string (Sys_js.file_content s)) in
let _Blob = get_global "Blob" in
let blob =
jsnew _Blob (Js.array [| s |])
in
let _URL = JSU.(get (get_global "window") (Js.string "URL")) in
let url : Js.js_string Js.t =
JSU.(meth_call _URL "createObjectURL" [| JSU.inject blob |])
in
Js.to_string url
module XHR =
struct
include XmlHttpRequest
let load_embedded_files = Js.to_bool (get_global "load_embedded_files")
let make_url =
if load_embedded_files then
fun u ->
Js.string (blob_url_of_string ("/" ^ (Js.to_string u)))
else fun u -> u
let update_file ?(date=0.) cb url =
let xhr = create () in
......@@ -35,7 +54,7 @@ module XHR =
Js.wrap_callback
(fun () ->
if xhr ## readyState == DONE then
if xhr ## status = 200 then
if xhr ## status = 200 || (xhr ## status = 0 && load_embedded_files) then
let date_str = Js.Opt.get (xhr ## getResponseHeader (Js.string "Last-Modified"))
(fun () -> Js.string "01/01/2100") (* far into the future *)
in
......@@ -53,12 +72,12 @@ module XHR =
else
cb `NotFound)
in
let () = xhr ## _open (Js.string "GET", url, Js._true) in
let () = xhr ## _open (Js.string "GET", (make_url url), Js._true) in
xhr ## send (Js.null)
else
cb `NotFound
);
xhr ## _open (Js.string "HEAD", url, Js._true);
xhr ## _open (Js.string "HEAD", (make_url url), Js._true);
xhr ## send (Js.null)
end
......@@ -848,7 +867,7 @@ module Controller =
let rec init_alt_ergo_worker i =
let worker = Worker.create "alt_ergo_worker.js" in
let worker = Worker.create (blob_url_of_string "/alt_ergo_worker.js") in
worker ## onmessage <-
(Dom.handler (fun ev ->
let (id, result) as res = unmarshal (ev ## data) in
......@@ -898,7 +917,7 @@ module Controller =
process_task ()
let init_why3_worker () =
let worker = Worker.create "why3_worker.js" in
let worker = Worker.create (blob_url_of_string "/why3_worker.js") in
worker ## onmessage <-
(Dom.handler (fun ev ->
let msg = unmarshal (ev ## data) in
......@@ -1059,7 +1078,7 @@ let () =
Session.save_num_steps !Controller.alt_ergo_steps;
Session.save_view_mode (if Panel.is_wide () then Js.string "wide"
else Js.string "column");
(Js.string "Do you wish to quit TryWhy3 (your current session will be saved to your browser local storage) ?"))
)
......
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