Commit 2cd6e016 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove the logic for embedded example files.

parent 24c1031e
......@@ -1758,16 +1758,13 @@ trywhy3.tar.gz: $(addprefix src/trywhy3/, $(TRYWHY3_PACK))
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/examples/*.mlw
js_of_ocaml $(JSOO_DEBUG) --extern-fs -I src/trywhy3 \
--file=examples/index.txt:/examples/index.txt \
`find src/trywhy3/examples -name "*.mlw" -printf " --file=examples/%P:/examples/%P"` \
$<
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml $(JSOO_DEBUG) $<
src/trywhy3/trywhy3.byte: $(addprefix src/trywhy3/, bindings.cmo worker_proto.cmo trywhy3.cmo)
$(OCAMLFIND) ocamlc -o $@ -package js_of_ocaml -linkpkg $^
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/try_alt_ergo.drv
src/trywhy3/why3_worker.js: src/trywhy3/why3_worker.byte src/trywhy3/trywhy3.conf src/trywhy3/try_alt_ergo.drv
js_of_ocaml $(JSOO_DEBUG) --extern-fs -I . -I src/trywhy3 \
--file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \
......
......@@ -37,13 +37,6 @@ Instructions to build TryWhy3
ALTERGODIR=src/trywhy3/alt-ergo
* [optional] If you want to build a standalone trywhy3 that can be
run without a web server, 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
......@@ -70,18 +63,9 @@ Customization
* To change the look and feel of the rest of the application, edit
the file `trywhy3_custom.css`.
* To add some predefined examples, put some `.mlw` or `.why` files in the
* To add some predefined examples, put some `.mlw` files in the
`examples/` subdirectory and generate an index as follows:
cp some_file.mlw examples/
cd examples/
../gen_index.sh *.mlw > index.txt
* [optional] If you want trywhy3 to only use its embedded files,
change the variable declaration `var load_embedded_files = false;`
to `var load_embedded_files = true;` in the header section of
`trywhy3.html`.
Note that this is the default behavior when `trywhy3.html` is opened from
a `file://` URL rather than a `http(s)://` URL, regardless of the value of
the `load_embedded_files` variable.
......@@ -12,10 +12,8 @@
type="text/javascript" charset="utf-8"></script>
<script type="text/javascript">
var load_embedded_files = false;
var editor_theme = "ace/theme/chrome";
var task_viewer_mode = "ace/mode/why3";
var library_index = "examples/index.txt";
</script>
<script defer="defer" type="text/javascript"
src="trywhy3.js"></script>
......
......@@ -17,45 +17,26 @@ module Js = Js_of_ocaml.Js
module JSU = Js_of_ocaml.Js.Unsafe
module Dom = Js_of_ocaml.Dom
module File = Js_of_ocaml.File
module Sys_js = Js_of_ocaml.Sys_js
module Worker = Js_of_ocaml.Worker
module Dom_html = Js_of_ocaml.Dom_html
module XmlHttpRequest = Js_of_ocaml.XmlHttpRequest
let int_of_js_string s = int_of_string (Js.to_string s)
let blob_url_of_string s =
let s = Sys_js.read_file ~name:s in
let blob = File.blob_from_string s in
let url = Dom_html.window ##. _URL ## createObjectURL blob in
Js.to_string url
module XHR =
struct
include XmlHttpRequest
let load_embedded_files =
Js.to_bool (get_global "load_embedded_files") ||
Js.to_string (Dom_html.window ##. location ##. protocol) = "file:"
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
xhr ##. onreadystatechange :=
Js.wrap_callback
(fun () ->
if xhr ##. readyState == DONE then
if xhr ##. status = 200 || (xhr ##. status = 0 && load_embedded_files) then
if xhr ##. status = 200 then
let date_str = Js.Opt.get (xhr ## getResponseHeader (Js.string "Last-Modified"))
(fun () -> Js.string "01/01/2100") (* far into the future *)
in
log (Printf.sprintf "File %s has date %s" (Js.to_string url) (Js.to_string date_str));
let document_date = Js.date ## parse (date_str) in
if document_date < date then
cb `UpToDate
......@@ -69,12 +50,12 @@ module XHR =
else
cb `NotFound)
in
let () = xhr ## _open (Js.string "GET") (make_url url) Js._true in
let () = xhr ## _open (Js.string "GET") url Js._true in
xhr ## send (Js.null)
else
cb `NotFound
);
xhr ## _open (Js.string "HEAD") (make_url url) Js._true;
xhr ## _open (Js.string "HEAD") url Js._true;
xhr ## send (Js.null)
end
......
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