Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

trywhy3.ml 1.64 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57

module D = Dom_html

let d = D.document

let node x = (x : #Dom.node Js.t :> Dom.node Js.t)

let (<|) e l = List.iter (fun c -> Dom.appendChild e c) l; node e

let html_of_string (s:string) =
  d##createElement (Js.string "p") <|
      [node (d##createTextNode (Js.string s))]

let replace_child p n =
  Js.Opt.iter (p##firstChild) (fun c -> Dom.removeChild p c);
  Dom.appendChild p n

let temp_file_name = "/input.mlw"

open Why3

let run textbox preview _ =
  let text = Js.to_string (textbox##value) in
  Sys_js.register_file ~name:temp_file_name ~content:text;
  let env = Env.create_env [] in
  let answer =
    try
      let _x = Env.read_file Env.base_language env temp_file_name in
      "parsing OK"
    with e ->
      Pp.sprintf
        "exception raised in parsing: %a" Exn_printer.exn_printer e
  in
  replace_child preview (html_of_string answer);
  Js._false

let onload (_event : #Dom_html.event Js.t) : bool Js.t =
  let body =
    Js.Opt.get (d##getElementById(Js.string "trywhy3"))
      (fun () -> assert false) in
  let textbox = D.createTextarea d in
  textbox##rows <- 20; textbox##cols <- 100;
  let go = D.createButton ~name:(Js.string "go") d in
  go##textContent <- Js.some (Js.string "Go");
  let preview = D.createDiv d in
  preview##style##border <- Js.string "1px black";
  preview##style##padding <- Js.string "5px";
  Dom.appendChild body textbox;
  Dom.appendChild body (D.createBr d);
  Dom.appendChild body go;
  Dom.appendChild body (D.createBr d);
  Dom.appendChild body preview;
  replace_child preview (html_of_string "(Answer)");
  go##onclick <- D.handler (run textbox preview);
  Js._false

let _ = D.window##onload <- D.handler onload