diff --git a/.gitignore b/.gitignore
index c4b33fc92e226858a5f4fb5a212f2a87ea822bb4..ff672161f7281761784339f0b92fe0e34a043f2a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -278,14 +278,19 @@ pvsbin/
 /modules/mach/int/
 
 # Try Why3
-/src/trywhy3/trywhy3.js
 /src/trywhy3/trywhy3.byte
+/src/trywhy3/trywhy3.js
+/src/trywhy3/alt_ergo_worker.byte
+/src/trywhy3/alt_ergo_worker.js
+/src/trywhy3/why3_worker.byte
+/src/trywhy3/why3_worker.js
 /src/trywhy3/index.en.html
 /src/trywhy3/index.fr.html
 /src/trywhy3/index.html
-/src/trywhy3/ace-builds
+/src/trywhy3/ace-builds/
 /src/trywhy3/*.png
 /src/trywhy3/alt-ergo-1.00-private-2015-01-29
+/src/trywhy3/fontawesome/
 
 # jessie3
 /src/jessie/config.log
diff --git a/Makefile.in b/Makefile.in
index 4b0c11f90df04272774276b9a30e45dc5f4c1c2b..2dc8c552817ae9e351f220035296a69888e4040a 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -1504,10 +1504,10 @@ ALTERGOMODS=util/numsNumbers util/numbers \
 	instances/matching \
 	sat/sat_solvers \
 	main/frontend
+ALTERGOCMO=$(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
+TRYWHY3CMO=lib/why3/why3.cma 
 
-TRYWHY3CMO=lib/why3/why3.cma $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
-
-trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
+trywhy3: src/trywhy3/trywhy3.js src/trywhy3/why3_worker.js src/trywhy3/alt_ergo_worker.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
 
 %.fr.html: %.prehtml
 	yamlpp -l fr $< -o $@
@@ -1516,19 +1516,38 @@ trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.h
 	yamlpp -l en $< -o $@
 
 src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
-	js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
-		--file=try_alt_ergo.drv:/ \
+	js_of_ocaml --extern-fs -I . -I src/trywhy3 \
 		--file=drinkers.why:/ \
 		--file=simplearith.why:/ \
 		--file=bin_mult.mlw:/ \
 		--file=fact.mlw:/ \
 		--file=isqrt.mlw:/ \
-		`find theories modules \( -name "*.mlw" -o -name "*.why" \) -printf " --file=%p:/"` \
 		+weak.js +nat.js $^
 
-src/trywhy3/trywhy3.byte: $(TRYWHY3CMO) src/trywhy3/trywhy3.cmo
+src/trywhy3/trywhy3.byte: src/trywhy3/worker_proto.cmo src/trywhy3/trywhy3.cmo
+	$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
+
+
+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 $^
+
+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 $^
+
+src/trywhy3/alt_ergo_worker.byte: $(ALTERGOCMO) src/trywhy3/worker_proto.cmo src/trywhy3/alt_ergo_worker.cmo
 	$(JSOCAMLC) $(BFLAGS) -o $@ -linkpkg $(BLINKFLAGS) $^
 
+src/trywhy3/alt_ergo_worker.cmo: src/trywhy3/worker_proto.cmo
+src/trywhy3/why3_worker.cmo: src/trywhy3/worker_proto.cmo
+src/trywhy3/trywhy3.cmo: src/trywhy3/worker_proto.cmo
+
 src/trywhy3/%.cmo: src/trywhy3/%.ml
 	$(JSOCAMLC) $(BFLAGS) -c $<
 
@@ -1536,7 +1555,11 @@ src/trywhy3/%.cmi: src/trywhy3/%.mli
 	$(JSOCAMLC) $(BFLAGS) -c $<
 
 clean::
-	rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte
+	rm -f src/trywhy3/trywhy3.js src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.cm* \
+	 src/trywhy3/why3_worker.js src/trywhy3/why3_worker.byte src/trywhy3/why3_worker.cm* \
+         src/trywhy3/alt_ergo_worker.js src/trywhy3/alt_ergo_worker.byte src/trywhy3/alt_ergo_worker.cm* \
+         src/trywhy3/worker_proto.cm*	\
+	 src/trywhy3/index.en.html src/trywhy3/index.fr.html
 
 CLEANDIRS += src/trywhy3
 
diff --git a/src/trywhy3/README b/src/trywhy3/README
index 8770a69088229fb0f9aa0f66df39b05c90790e52..23c4e5578c08993f746e80e41bfbbcf58fa929e4 100644
--- a/src/trywhy3/README
+++ b/src/trywhy3/README
@@ -7,6 +7,12 @@ Instructions to build TryWhy3
 
      git clone https://github.com/ajaxorg/ace-builds.git
 
+  ** copy the fontawesome webfont locally :
+     mkdir fontawesome
+     cd fontawesome
+     wget -nd https://www.lri.fr/~kn/trywhy3/fontawesome/fontawesome.css
+     wget -nd https://www.lri.fr/~kn/trywhy3/fontawesome/fontawesome-webfont.woff
+
   ** install Alt-Ergo
 
      - get sources of Alt-Ergo and put them in directory src/trywhy3/ e.g. in
diff --git a/src/trywhy3/alt_ergo_worker.ml b/src/trywhy3/alt_ergo_worker.ml
new file mode 100644
index 0000000000000000000000000000000000000000..c947edc03d38af8b1663160df1b746aeb3efc5bd
--- /dev/null
+++ b/src/trywhy3/alt_ergo_worker.ml
@@ -0,0 +1,53 @@
+open Format
+open Worker_proto
+
+module SAT = (val (Sat_solvers.get_current ()) : Sat_solvers.S)
+module FE = Frontend.Make (SAT)
+
+let print_status fmt _d status steps =
+  match status with
+  | FE.Unsat _dep ->
+    fprintf fmt "Proved (%Ld steps)" steps
+  | FE.Inconsistent -> ()
+    (* fprintf fmt "Inconsistent assumption" *)
+  | FE.Unknown _t | FE.Sat _t ->
+      fprintf fmt "Unknown (%Ld steps)@." steps
+
+
+let report_status report _d status _steps =
+  match status with
+  | FE.Unsat _dep -> report Valid
+  | FE.Inconsistent -> ()
+  | FE.Unknown _t | FE.Sat _t -> report (Unknown "unknown")
+
+let run_alt_ergo_on_task text =
+  let lb = Lexing.from_string text in
+(* from Alt-Ergo, src/main/frontend.ml *)
+  let a = Why_parser.file Why_lexer.token lb in
+  Parsing.clear_parser ();
+  let ltd, _typ_env = Why_typing.file false Why_typing.empty_env a in
+  match Why_typing.split_goals ltd with
+  | [d] ->
+    let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
+    SAT.reset_steps ();
+    let stat = ref (Invalid "no answer from Alt-Ergo") in
+    let f s = stat := s in
+    begin
+      try
+        let _x = Queue.fold (FE.process_decl (report_status f))
+          (SAT.empty (), true, Explanation.empty) d
+        in
+        !stat
+      with Sat_solvers.StepsLimitReached -> Unknown "steps limit reached"
+    end
+  | _ -> Invalid "zero or more than 1 goal to solve"
+
+
+
+
+let () =
+  Options.set_steps_bound 100;
+  Worker.set_onmessage (fun msg ->
+			let (id, text) = unmarshal msg in
+			let result = run_alt_ergo_on_task text in
+			Worker.post_message (marshal (id,result)))
diff --git a/src/trywhy3/index.prehtml b/src/trywhy3/index.prehtml
index e5e918e9597149d3b0bed52a3b7967fd00c00a8f..c368ca13e38ca517bf31acbd70e2aac7831e0f73 100644
--- a/src/trywhy3/index.prehtml
+++ b/src/trywhy3/index.prehtml
@@ -40,6 +40,7 @@
       </div>
     </div>
     <!-- the main page -->
+    <div id="header">
       <div align="right">
         <#fr><a href="index.en.html">English version</a></#fr>
         <#en><a href="index.fr.html">Version fran&ccedil;aise</a></#en>
@@ -72,6 +73,7 @@
           <#fr>utilis&eacute; pour produire cette page</#fr>
       </ul>
     </p>
+    </div>
     <div class="menu-bar">
       <ul>
 	<li><a href="#"><#en>File</#en><#fr>Fichier</#fr></a>
@@ -132,6 +134,10 @@
 	    <li><a href="#" id="prove">
                 <#en>Prove</#en>
                 <#fr>Prouver</#fr>
+            </a></li>
+	    	    <li><a href="#" id="stop">
+                <#en>Stop Alt-ergo</#en>
+                <#fr>Arrêter Alt-ergo</#fr>
             </a></li>
 	  </ul>
 	</li>
diff --git a/src/trywhy3/style.css b/src/trywhy3/style.css
index 1ba5b32d20c4846c3c44d2baa70a9d7eae416069..c522249d1a0a4d5ffce07934984517f14c2caf94 100644
--- a/src/trywhy3/style.css
+++ b/src/trywhy3/style.css
@@ -1,3 +1,11 @@
+@import url(fontawesome/fontawesome.css);
+
+/* fontawesome */
+[class*="fontawesome-"]:before {
+    font-family: 'FontAwesome', sans-serif;
+}
+
+
 body {
     padding:0;
     margin:0;
@@ -132,20 +140,20 @@ body {
 
 #console ul {
     list-style-type: none;
-    padding: 8px;
-    margin: 4px;
+    padding: 0.5em;
+    /*margin: 0.5em; */
 }
 
 #console ul ul {
     list-style-type: disc;
-    padding: 8px;
-    margin: 4px;
+    padding: 0.5em;
+    /*margin: 0.5em;*/
 }
 
 #console ul ul ul {
     list-style-type: none;
-    padding: 0px;
-    margin: 4px;
+    padding: 0.5em;
+    /*margin: 0.5em; */
 }
 
 #editor {
@@ -198,3 +206,17 @@ body {
 #confirm-dialog .btn {
     width:40%;
 }
+
+#header {
+    height: 30vh;
+
+}
+.menu-bar {
+    height: 5vh;
+}
+#editor-panel {
+    height: 65vh;
+}
+#console {
+    overflow: auto;
+}
\ No newline at end of file
diff --git a/src/trywhy3/trywhy3.ml b/src/trywhy3/trywhy3.ml
index 235fb9c1811f280b5584f3c812798c00555488ab..59c573b03568c6657c509aea8a35b79702445903 100644
--- a/src/trywhy3/trywhy3.ml
+++ b/src/trywhy3/trywhy3.ml
@@ -10,322 +10,266 @@
 (********************************************************************)
 
 (* simple helpers *)
+open Worker_proto
 
 let get_opt o = Js.Opt.get o (fun () -> assert false)
 
-let log s = Firebug.console ## log (Js.string s)
 
-
-(* module for generating HTML elements *)
-
-module Html = struct
-
-let d = Dom_html.document
-
-let node x = (x : #Dom.node Js.t :> Dom.node Js.t)
-
-let of_string s = node (d##createTextNode (Js.string s))
-
-let img i =
-  let x = Dom_html.createImg d in
-  x##src <- Js.string i;
-  x##height <- 12;
-  (* X##align <- Js.string "bottom"; *)
-  node x
-
-let img_accept () = img "accept32.png"
-let img_help () = img "help32.png"
-let img_bug () = img "bug32.png"
-
-let par nl =
-  let x = d##createElement (Js.string "p") in
-  List.iter (Dom.appendChild x) nl;
-  node x
-
-let ul nl =
-  let x = d##createElement (Js.string "ul") in
-  List.iter
-    (fun n ->
-      let y =  d##createElement (Js.string "li") in
-      List.iter (Dom.appendChild y) n;
-      Dom.appendChild x (node y))
-    nl;
-  node x
-
-end
-
-
-(* Interface to Why3 and Alt-Ergo *)
-
-let why3_conf_file = "/trywhy3.conf"
-
-open Why3
-open Format
-
-(* reads the config file *)
-let config : Whyconf.config = Whyconf.read_config (Some why3_conf_file)
-(* the [main] section of the config file *)
-let main : Whyconf.main = Whyconf.get_main config
-(* all the provers detected, from the config file *)
-let provers : Whyconf.config_prover Whyconf.Mprover.t =
-  Whyconf.get_provers config
-
-(* One prover named Alt-Ergo in the config file *)
-let alt_ergo : Whyconf.config_prover =
-  if Whyconf.Mprover.is_empty provers then begin
-    eprintf "Prover Alt-Ergo not installed or not configured@.";
-    exit 0
-  end else snd (Whyconf.Mprover.choose provers)
-
-(* builds the environment from the [loadpath] *)
-let env : Env.env = Env.create_env (Whyconf.loadpath main)
-
-let alt_ergo_driver : Driver.driver =
-  try
-    Printexc.record_backtrace true;
-    Driver.load_driver env alt_ergo.Whyconf.driver []
-  with e ->
-    let s = Printexc.get_backtrace () in
-    eprintf "Failed to load driver for alt-ergo: %a@.%s@."
-      Exn_printer.exn_printer e s;
-  exit 1
-
-module SAT = (val (Sat_solvers.get_current ()) : Sat_solvers.S)
-module FE = Frontend.Make (SAT)
-
-let print_status fmt _d status steps =
-  match status with
-  | FE.Unsat _dep ->
-    fprintf fmt "Proved (%Ld steps)" steps
-  | FE.Inconsistent -> ()
-    (* fprintf fmt "Inconsistent assumption" *)
-  | FE.Unknown _t | FE.Sat _t ->
-      fprintf fmt "Unknown (%Ld steps)@." steps
-
-type prover_answer = Valid | Unknown of string | Error of string
-
-let report_status report _d status _steps =
-  match status with
-  | FE.Unsat _dep -> report Valid
-  | FE.Inconsistent -> ()
-  | FE.Unknown _t | FE.Sat _t -> report (Unknown "unknown")
-
-let run_alt_ergo_on_task t =
-  (* printing the task in a string *)
-  Driver.print_task alt_ergo_driver str_formatter t;
-  let text = flush_str_formatter () in
-  let lb = Lexing.from_string text in
-(* from Alt-Ergo, src/main/frontend.ml *)
-  let a = Why_parser.file Why_lexer.token lb in
-  Parsing.clear_parser ();
-  let ltd, _typ_env = Why_typing.file false Why_typing.empty_env a in
-  match Why_typing.split_goals ltd with
-  | [d] ->
-    let d = Cnf.make (List.map (fun (f, _env) -> f, true) d) in
-    SAT.reset_steps ();
-    let stat = ref (Error "no answer from Alt-Ergo") in
-    let f s = stat := s in
-    begin
-      try
-        let _x = Queue.fold (FE.process_decl (report_status f))
-          (SAT.empty (), true, Explanation.empty) d
-        in
-        !stat
-      with Sat_solvers.StepsLimitReached -> Unknown "steps limit reached"
-    end
-  | _ -> Error "zero or more than 1 goal to solve"
-
-let split_trans = Trans.lookup_transform_l "split_goal_wp" env
-
-let why3_prove theories =
-  let theories =
-    Stdlib.Mstr.fold
-      (fun thname th acc ->
-        let tasks = Task.split_theory th None None in
-        let tasks = List.rev_map
-          (fun t ->
-            let (id,expl,_) = Termcode.goal_expl_task ~root:true t in
-            let expl = match expl with
-              | Some s -> s
-              | None -> id.Ident.id_string
-            in
-            let tl = Trans.apply split_trans t in
-            let tasks =
-              List.map
-                (fun task ->
-                  let (id,expl,_) = Termcode.goal_expl_task ~root:false task in
-                  let expl = match expl with
-                    | Some s -> s
-                    | None -> id.Ident.id_string
-                  in
-                  let result = run_alt_ergo_on_task task in
-                  let img,res = match result with
-                    | Valid -> Html.img_accept, expl
-                    | Unknown s -> Html.img_help, expl ^ " (" ^ s ^ ")"
-                    | Error s -> Html.img_bug, expl ^ " (" ^ s ^ ")"
-                  in
-                  [img (); Html.of_string (" " ^ res)])
-                tl
-            in
-            [Html.of_string expl; Html.ul tasks])
-          tasks
-        in
-        let loc =
-          Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
-        in
-        (loc,[ Html.of_string thname; Html.ul tasks]) :: acc)
-      theories []
-  in
-  let s =
-    List.sort
-      (fun (l1,_) (l2,_) -> Loc.compare l2 l1)
-      theories
-  in
-  Html.ul (List.rev_map snd s)
-
-let execute_symbol m fmt ps =
-  match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
-  | None ->
-    fprintf fmt "function '%s' has no definition"
-      ps.Mlw_expr.ps_name.Ident.id_string
-  | Some d ->
-    let lam = d.Mlw_expr.fun_lambda in
-    match lam.Mlw_expr.l_args with
-    | [pvs] when
-        Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
-      begin
-        let spec = lam.Mlw_expr.l_spec in
-        let eff = spec.Mlw_ty.c_effect in
-        let writes = eff.Mlw_ty.eff_writes in
-        let body = lam.Mlw_expr.l_expr in
-        try
-          let res, _final_env =
-            Mlw_interp.eval_global_expr env m.Mlw_module.mod_known
-              m.Mlw_module.mod_theory.Theory.th_known writes body
-          in
-          match res with
-          | Mlw_interp.Normal v -> Mlw_interp.print_value fmt v
-          | Mlw_interp.Excep(x,v) ->
-            fprintf fmt "exception %s(%a)"
-              x.Mlw_ty.xs_name.Ident.id_string Mlw_interp.print_value v
-          | Mlw_interp.Irred e ->
-            fprintf fmt "cannot execute expression@ @[%a@]"
-              Mlw_pretty.print_expr e
-          | Mlw_interp.Fun _ ->
-            fprintf fmt "result is a function"
-        with e ->
-          fprintf fmt
-            "failure during execution of function: %a (%s)"
-            Exn_printer.exn_printer e
-            (Printexc.to_string e)
-    end
-  | _ ->
-    fprintf fmt "Only functions with one unit argument can be executed"
-
-let why3_execute (modules,_theories) =
-  let mods =
-    Stdlib.Mstr.fold
-      (fun _k m acc ->
-        let th = m.Mlw_module.mod_theory in
-        let modname = th.Theory.th_name.Ident.id_string in
-        try
-          let ps =
-            Mlw_module.ns_find_ps m.Mlw_module.mod_export ["main"]
-          in
-          let result = Pp.sprintf "%a" (execute_symbol m) ps in
-          let loc =
-            Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
-          in
-          (loc,[Html.of_string (modname ^ ".main() returns " ^ result)])
-          :: acc
-        with Not_found -> acc)
-      modules []
-  in
-  match mods with
-  | [] -> Html.par [Html.of_string "No main function found"]
-  | _ ->
-    let s =
-      List.sort
-        (fun (l1,_) (l2,_) -> Loc.compare l2 l1)
-        mods
-    in
-    Html.ul (List.rev_map snd s)
-
-
-(* Connecting Why3 calls to the interface *)
-
-let temp_file_name = "/input.mlw"
-
-let () = Sys_js.register_file ~name:temp_file_name ~content:""
-
-let run_why3 f lang global text =
-  let ch = open_out temp_file_name in
-  output_string ch text;
-  close_out ch;
-  try
-    (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
-    let theories = Env.read_file lang env temp_file_name in
-    f theories
-  with
-  | Loc.Located(loc,e') ->
-    let (_,l,b,e) = Loc.get loc in
-    ignore (Js.Unsafe.meth_call global "highlightError"
-	      (Array.map Js.Unsafe.inject [| l-1; b; l-1; e |]));
-    Html.par
-      [Html.of_string
-          (Pp.sprintf
-             "error line %d, columns %d-%d: %a" l b e
-             Exn_printer.exn_printer e')]
-  | e ->
-    Html.par
-      [Html.of_string
-          (Pp.sprintf
-             "unexpected exception: %a (%s)" Exn_printer.exn_printer e
-             (Printexc.to_string e))]
-
-let add_why3_cmd buttonname f input_lang =
-  let handler = Dom.handler
-    (fun _ev ->
+(* the view *)
+module Console =
+  struct
+    let get_buffer () =
       let global = Js.Unsafe.global in
       let editor = Js.Unsafe.get global (Js.string "editor") in
-      let lang = "en"
-(*
-        Js.to_string
-          (Js.Unsafe.meth_call editor "getAttribute"
-             [| Js.Unsafe.inject (Js.string "lang") |])
-*)
-      in
-      let code = Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |]) in
-      log ("Why3 is running, lang = " ^ lang);
-      let answer = run_why3 f input_lang global code in
-      log "Why3 answer given";
-      let console =
+      Js.to_string (Js.Unsafe.meth_call editor "getValue" [| |])
+
+    let get_console () =
         get_opt (Dom_html.document ## getElementById (Js.string "console"))
-      in
-      (* remove the previous answer if any *)
-      Js.Opt.iter (console##lastChild) (Dom.removeChild console);
-      (* put the new answer *)
-      Dom.appendChild console answer;
-      (* give the focus back to the editor *)
-      ignore (Js.Unsafe.meth_call editor "focus" [| |]);
-      Js._false)
+
+    let clear () =
+      (get_console ()) ## innerHTML <- (Js.string "")
+
+    let print cls msg =
+        (get_console ()) ## innerHTML <-
+          (Js.string ("<p class='" ^ cls ^ "'>" ^
+                        msg ^ "</p>"))
+
+    let print_error = print "error"
+
+    let print_msg = print "msg"
+
+    let node_to_html n =
+      Dom_html.element (get_opt (Dom.CoerceTo.element (get_opt n)))
+
+    let print_alt_ergo_output id res =
+      (* see alt_ergo_worker.ml and the Tasks case in print_why3_output *)
+      let doc = Dom_html.document in
+      match Js.Opt.to_option (doc ## getElementById (Js.string id)) with
+        None -> log ("No element with id " ^ id)
+      | Some li ->
+         let span_icon = node_to_html ( li ## firstChild ) in
+         let span_msg = node_to_html ( li ## lastChild ) in
+         match res with
+           Valid ->
+           span_icon ## className <- (Js.string "fontawesome-ok-sign");
+           (span_icon ## style) ## color <- (Js.string "green");
+
+         | Unknown msg ->
+            span_icon ## className <- (Js.string "fontawesome-question-sign");
+            (span_icon ## style) ## color <- (Js.string "orange");
+            span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
+         | Invalid msg ->
+            span_icon ## className <- (Js.string "fontawesome-remove-sign");
+            (span_icon ## style) ## color <- (Js.string "red");
+            span_msg ## innerHTML <- (Js.string (" (" ^ msg ^ ")"))
+
+    let appendChild o c =
+      ignore (o ## appendChild ( (c :> Dom.node Js.t)))
+
+    let print_why3_output o =
+      let doc = Dom_html.document in
+      (* see why3_worker.ml *)
+      match o with
+        Error s -> print_error s
+
+      | ErrorLoc ((l1, b, l2, e), s) ->
+         ignore (Js.Unsafe.meth_call Js.Unsafe.global
+                                     "highlightError"
+                                     (Array.map Js.Unsafe.inject [| l1; b; l2; e |]));
+         print_error s
+      | Result sl ->
+         clear ();
+         let ul = Dom_html.createUl doc in
+         appendChild (get_console()) ul;
+         List.iter (fun (s : string) ->
+                    let li = Dom_html.createLi doc in
+                    li ## innerHTML <- (Js.string s);
+                    appendChild ul li;) sl
+
+
+      | Tasks ((th_id, th_name),
+               (task_id, task_name),
+               (vc_id, vc_expl, vc_code)) ->
+
+         let ul =
+           try
+             Dom_html.getElementById "theory-list"
+           with
+             Not_found ->
+             let ul = Dom_html.createUl doc in
+             ul ## id <- Js.string "theory-list";
+             appendChild (get_console()) ul;
+             ul
+         in
+         let th_ul =
+           try
+             node_to_html ((Dom_html.getElementById th_id) ## lastChild)
+           with
+             Not_found ->
+             let li = Dom_html.createLi doc in
+             li ## id <- Js.string th_id;
+             appendChild ul li;
+             appendChild li (doc ## createTextNode (Js.string th_name));
+             let tul = Dom_html.createUl doc in
+             appendChild li tul;
+             tul
+         in
+         let task_ul =
+           try
+             node_to_html ((Dom_html.getElementById  task_id) ## lastChild)
+           with
+             Not_found ->
+             let li = Dom_html.createLi doc in
+             li ## id <- Js.string task_id;
+             appendChild th_ul li;
+             appendChild li (doc ## createTextNode (Js.string task_name));
+             let tul = Dom_html.createUl doc in
+             appendChild li tul;
+             tul
+         in
+         let li = Dom_html.createLi doc in
+         li ## id <- Js.string vc_id;
+         appendChild task_ul li;
+         let span = Dom_html.createSpan doc in
+         span ## className <- Js.string "fontawesome-cogs pending";
+         (span ## style) ## color <- (Js.string "blue");
+
+         appendChild li (span);
+         appendChild li (doc ## createTextNode (Js.string (" " ^ vc_expl ^ " ")));
+         appendChild li (Dom_html.createSpan doc)
+
+    let set_abort_icon () =
+      let list = Dom_html.document ## getElementsByClassName (Js.string "pending") in
+      List.iter (fun span ->
+                 span ## className <- (Js.string "fontawesome-minus-sign");
+                 (span ## style) ## color <- (Js.string "black"))
+                (Dom.list_of_nodeList list)
+
+  end
+
+let add_button buttonname f =
+  let handler =
+    Dom.handler
+      (fun _ev ->
+       f ();
+       let global = Js.Unsafe.global in
+       let editor = Js.Unsafe.get global (Js.string "editor") in
+       ignore (Js.Unsafe.meth_call editor "focus" [| |]);
+       Js._false)
   in
   let button =
     get_opt (Dom_html.document ## getElementById (Js.string buttonname))
   in
   button ## onclick <- handler
 
+
+let task_queue  = Queue.create ()
+let first_task = ref true
+type 'a status = Free of 'a | Busy of 'a | Absent
+let num_workers = 4
+
+let alt_ergo_workers = Array.make num_workers Absent
+
+let rec init_alt_ergo_worker i =
+  let worker = Worker.create "alt_ergo_worker.js" in
+  worker ## onmessage <-
+    (Dom.handler (fun ev ->
+                  let (id, result) = unmarshal (ev ## data) in
+                  Console.print_alt_ergo_output id result;
+                  alt_ergo_workers.(i) <- Free(worker);
+                  process_task ();
+                  Js._false));
+  Free (worker)
+
+and process_task () =
+  let rec find_free_worker_slot i =
+    if i < num_workers then
+      match alt_ergo_workers.(i) with
+        Free _ as w -> i, w
+      | _ -> find_free_worker_slot (i+1)
+    else -1, Absent
+  in
+  let idx, w = find_free_worker_slot 0 in
+  match w with
+    Free w when not (Queue.is_empty task_queue) ->
+    let task = Queue.take task_queue in
+    alt_ergo_workers.(idx) <- Busy (w);
+    w ## postMessage (marshal task)
+  | _ -> ()
+
+let reset_workers () =
+  Array.iteri
+    (fun i w ->
+     match w with
+       Busy (w)  ->
+                   w ## terminate ();
+                   alt_ergo_workers.(i) <- init_alt_ergo_worker i
+     | Absent -> alt_ergo_workers.(i) <- init_alt_ergo_worker i
+     | Free _ -> ()
+    ) alt_ergo_workers
+
+let push_task task =
+  Queue.add  task task_queue;
+  process_task ()
+
+let init_why3_worker () =
+  let worker = Worker.create "why3_worker.js" in
+  worker ## onmessage <-
+    (Dom.handler (fun ev ->
+                  let msg = unmarshal (ev ## data) in
+                  if !first_task then begin
+                      first_task := false;
+                      Console.clear ()
+                    end;
+                  Console.print_why3_output msg;
+                  let () =
+                    match msg with
+                      Tasks (_,_,(id,_,code)) -> push_task (id,code)
+                    | _ -> ()
+                  in Js._false));
+  (* seems necessary to warm-up the worker and start loading
+     the script premptively *)
+  worker ## postMessage(marshal Init);
+  worker
+
+let why3_worker = ref (init_why3_worker ())
+
+let why3_parse () =
+  Console.clear ();
+  Console.print_msg "Sending buffer to Alt-ergo … ";
+  log_time "Before marshalling in main thread";
+  reset_workers ();
+  first_task := true;
+  let code = Console.get_buffer () in
+  let msg = marshal (ParseBuffer code) in
+  log_time "After marshalling in main thread";
+  !why3_worker ## postMessage (msg)
+
+let why3_execute () =
+  Console.clear ();
+  Console.print_msg "Compiling buffer … ";
+  log_time "Before marshalling in main thread";
+  reset_workers ();
+  let code = Console.get_buffer () in
+  !why3_worker ## postMessage (marshal (ExecuteBuffer code))
+
+
 let () =
-  add_why3_cmd "prove" why3_prove Env.base_language;
-  add_why3_cmd "run" why3_execute Mlw_module.mlw_language
+  add_button "prove" why3_parse ;
+  add_button "run" why3_execute ;
+  add_button "stop" (fun () ->
+                     !why3_worker ## terminate ();
+                     why3_worker := init_why3_worker ();
+                     reset_workers ();
+                     Console.set_abort_icon())
 
 
 (* Predefined examples *)
 
-let add_file_example buttonname file =
+let add_file_example (buttonname, file) =
   let handler = Dom.handler
     (fun _ev ->
-      let text = Sysutil.file_contents file in
+      let text = Sys_js.file_content file in
       let global = Js.Unsafe.global in
       let editor = Js.Unsafe.get global (Js.string "editor") in
       Js.Unsafe.set global (Js.string "loadedBuffer") (Js.string text);
@@ -341,12 +285,16 @@ let add_file_example buttonname file =
   button ## onclick <- handler
 
 let () =
-  add_file_example "drinkers" "/drinkers.why";
+  let files =
+    [
+      "drinkers", "/drinkers.why";
 (*  add_file_example "simplearith" "/simplearith.why";*)
-  add_file_example "bin_mult" "/bin_mult.mlw";
-  add_file_example "fact" "/fact.mlw";
-  add_file_example "isqrt" "/isqrt.mlw";
-  Options.set_steps_bound 100
+      "bin_mult", "/bin_mult.mlw";
+      "fact", "/fact.mlw";
+      "isqrt", "/isqrt.mlw"
+    ]
+  in
+  List.iter add_file_example files;
 
 
 (*
diff --git a/src/trywhy3/why3_worker.ml b/src/trywhy3/why3_worker.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ed841c074d8abed2a8fce25e420a0ae436d1df87
--- /dev/null
+++ b/src/trywhy3/why3_worker.ml
@@ -0,0 +1,230 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+
+(* Interface to Why3 and Alt-Ergo *)
+
+let why3_conf_file = "/trywhy3.conf"
+
+open Why3
+open Format
+open Worker_proto
+
+let () = log_time ("Initialising why3 worker: start ")
+
+
+(* reads the config file *)
+let config : Whyconf.config = Whyconf.read_config (Some why3_conf_file)
+(* the [main] section of the config file *)
+let main : Whyconf.main = Whyconf.get_main config
+(* all the provers detected, from the config file *)
+let provers : Whyconf.config_prover Whyconf.Mprover.t =
+  Whyconf.get_provers config
+
+(* One prover named Alt-Ergo in the config file *)
+let alt_ergo : Whyconf.config_prover =
+  if Whyconf.Mprover.is_empty provers then begin
+    eprintf "Prover Alt-Ergo not installed or not configured@.";
+    exit 0
+  end else snd (Whyconf.Mprover.choose provers)
+
+(* builds the environment from the [loadpath] *)
+let env : Env.env = Env.create_env (Whyconf.loadpath main)
+
+let alt_ergo_driver : Driver.driver =
+  try
+    Printexc.record_backtrace true;
+    Driver.load_driver env alt_ergo.Whyconf.driver []
+  with e ->
+    let s = Printexc.get_backtrace () in
+    eprintf "Failed to load driver for alt-ergo: %a@.%s@."
+      Exn_printer.exn_printer e s;
+  exit 1
+
+let () = log_time ("Initialising why3 worker: end ")
+
+
+
+let split_trans = Trans.lookup_transform_l "split_goal_wp" env
+
+let task_to_string t =
+  ignore (flush_str_formatter ());
+  Driver.print_task alt_ergo_driver str_formatter t;
+  flush_str_formatter ()
+
+let gen_id =
+  let c = ref 0 in
+  fun () -> incr c; "id" ^ (string_of_int !c)
+
+let send msg =
+  Worker.post_message (marshal msg)
+
+let why3_parse_theories theories =
+  let theories =
+    Stdlib.Mstr.fold
+      (fun thname th acc ->
+       let loc =
+         Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
+       in
+       (loc, (thname, th)) :: acc) theories []
+  in
+  let theories = List.sort  (fun (l1,_) (l2,_) -> Loc.compare l1 l2) theories in
+  List.iter
+    (fun (_, (th_name, th)) ->
+     let th_id = gen_id () in
+     let tasks = Task.split_theory th None None in
+     List.iter
+       (fun task ->
+	let (id,expl,_) = Termcode.goal_expl_task ~root:true task in
+        let task_name = match expl with
+          | Some s -> s
+          | None -> id.Ident.id_string
+        in
+	let task_id = gen_id () in
+	List.iter
+	  (fun vc ->
+	   let vc_id = gen_id () in
+	   let id, expl, _ = Termcode.goal_expl_task ~root:false vc in
+	   let expl = match expl with
+             | Some s -> s
+             | None -> id.Ident.id_string
+           in
+	   let msg = Tasks ((th_id, th_name),
+			    (task_id, task_name),
+			    (vc_id, expl, task_to_string vc))
+	   in
+	   send msg)
+	  (Trans.apply split_trans task)
+       ) (List.rev tasks)
+    ) theories
+
+let execute_symbol m fmt ps =
+  match Mlw_decl.find_definition m.Mlw_module.mod_known ps with
+  | None ->
+     fprintf fmt "function '%s' has no definition"
+	     ps.Mlw_expr.ps_name.Ident.id_string
+  | Some d ->
+    let lam = d.Mlw_expr.fun_lambda in
+    match lam.Mlw_expr.l_args with
+    | [pvs] when
+        Mlw_ty.ity_equal pvs.Mlw_ty.pv_ity Mlw_ty.ity_unit ->
+      begin
+        let spec = lam.Mlw_expr.l_spec in
+        let eff = spec.Mlw_ty.c_effect in
+        let writes = eff.Mlw_ty.eff_writes in
+        let body = lam.Mlw_expr.l_expr in
+        try
+          let res, _final_env =
+            Mlw_interp.eval_global_expr env m.Mlw_module.mod_known
+              m.Mlw_module.mod_theory.Theory.th_known writes body
+          in
+          match res with
+          | Mlw_interp.Normal v -> Mlw_interp.print_value fmt v
+          | Mlw_interp.Excep(x,v) ->
+            fprintf fmt "exception %s(%a)"
+              x.Mlw_ty.xs_name.Ident.id_string Mlw_interp.print_value v
+          | Mlw_interp.Irred e ->
+            fprintf fmt "cannot execute expression@ @[%a@]"
+              Mlw_pretty.print_expr e
+          | Mlw_interp.Fun _ ->
+            fprintf fmt "result is a function"
+        with e ->
+          fprintf fmt
+            "failure during execution of function: %a (%s)"
+            Exn_printer.exn_printer e
+            (Printexc.to_string e)
+    end
+  | _ ->
+    fprintf fmt "Only functions with one unit argument can be executed"
+
+let why3_execute (modules,_theories) =
+  let result =
+    let mods =
+      Stdlib.Mstr.fold
+	(fun _k m acc ->
+         let th = m.Mlw_module.mod_theory in
+         let modname = th.Theory.th_name.Ident.id_string in
+         try
+           let ps =
+             Mlw_module.ns_find_ps m.Mlw_module.mod_export ["main"]
+           in
+           let result = Pp.sprintf "%a" (execute_symbol m) ps in
+           let loc =
+             Opt.get_def Loc.dummy_position th.Theory.th_name.Ident.id_loc
+           in
+           (loc, modname ^ ".main() returns " ^ result)
+           :: acc
+         with Not_found -> acc)
+	modules []
+    in
+    match mods with
+    | [] -> Error "No main function found"
+    | _ ->
+       let s =
+	 List.sort
+           (fun (l1,_) (l2,_) -> Loc.compare l2 l1)
+           mods
+       in
+       (Result (List.rev_map snd s) )
+  in
+  send result
+
+let temp_file_name = "/input.mlw"
+
+let () = Sys_js.register_file ~name:temp_file_name ~content:""
+
+let why3_run f lang code =
+  try
+    log_time "Why3 worker : start writing file";
+    let ch = open_out temp_file_name in
+    output_string ch code;
+    close_out ch;
+    log_time "Why3 worker : stop writing file";
+
+    (* TODO: add a function Env.read_string or Env.read_from_lexbuf ? *)
+    log_time "Why3 worker : start parsing file";
+
+    let theories = Env.read_file lang env temp_file_name in
+    log_time "Why3 worker : stop parsing file";
+    f theories
+  with
+  | Loc.Located(loc,e') ->
+     let _, l, b, e = Loc.get loc in
+     send (ErrorLoc ((l-1,b, l-1, e),
+		     Pp.sprintf
+		       "error line %d, columns %d-%d: %a" l b e
+		       Exn_printer.exn_printer e'))
+  | e ->
+     send (Error (Pp.sprintf
+		    "unexpected exception: %a (%s)" Exn_printer.exn_printer e
+		    (Printexc.to_string e)))
+
+
+let () =
+  
+  Worker.set_onmessage
+    (fun ev ->
+
+     log_time ("Entering why3 worker ");
+     let ev = unmarshal ev in
+     log_time ("After unmarshal ");
+     match ev with
+       Init -> ()
+     | ParseBuffer code ->
+       why3_run why3_parse_theories Env.base_language code
+     | ExecuteBuffer code ->
+	why3_run why3_execute Mlw_module.mlw_language code
+    )
+(*
+Local Variables:
+compile-command: "unset LANG; make -C ../.. src/trywhy3/trywhy3.js"
+End:
+*)
diff --git a/src/trywhy3/worker_proto.ml b/src/trywhy3/worker_proto.ml
new file mode 100644
index 0000000000000000000000000000000000000000..6bf07484a33b86004d8f03d7005940d759b66808
--- /dev/null
+++ b/src/trywhy3/worker_proto.ml
@@ -0,0 +1,27 @@
+type command =  ParseBuffer of string
+              | ExecuteBuffer of string
+              | Init
+
+
+type output = Error of string (* msg *)
+             | ErrorLoc of ((int*int*int*int) * string) (* loc * msg *)
+             | Tasks of ((string * string) (* Theory (id, name) *)
+                       * (string * string) (* Task (id, name *)
+                       * (string * string * string)) (* VC (id, expl, code ) *)
+             | Result of string list
+
+type prover_answer = Valid | Unknown of string | Invalid of string
+
+let marshal a =
+  Js.string (String.escaped (Marshal.to_string a [Marshal.No_sharing; Marshal.Compat_32]))
+
+let unmarshal a =
+  Marshal.from_string (Scanf.unescaped (Js.to_string a)) 0
+
+
+
+let log s = ignore (Firebug.console ## log (Js.string s))
+let log_time s =
+  let date = jsnew Js.date_now () in
+  let date_str = string_of_float ((date ## getTime ()) /. 1000.) in
+  log (date_str ^ " : " ^ s)