Commit 296266a2 authored by Kim Nguyễn's avatar Kim Nguyễn

[trywhy3]: * prevent the user from compiling the buffer again while why3/alt-ergo is running.

parent bdc7da81
......@@ -124,8 +124,10 @@ body {
/*** MAIN EDITOR ***/
#why3-editor-container {
position:relative;
flex-grow:2;
}
#why3-tab-container {
flex-grow:1;
position:relative;
margin:0;
padding:0;
......@@ -144,14 +146,14 @@ body {
/*** TABS ***/
#why3-tab-panel {
top:0;
bottom:0;
left:0;
right:0;
padding:0;
margin:0;
}
......
......@@ -95,6 +95,9 @@
<ul>
<li id="why3-split-menu-entry"><span class="fa-share-alt
why3-icon"></span> Split and prove </li>
<li id="why3-prove-menu-entry"><span class="fa-check-square
why3-icon"></span>
Prove (default) </li>
<li id="why3-prove100-menu-entry"><span class="fa-check-square
why3-icon"></span>
Prove (100
......
......@@ -180,6 +180,7 @@ module ContextMenu =
struct
let task_menu = getElement AsHtml.div "why3-task-menu"
let split_menu_entry = getElement AsHtml.li "why3-split-menu-entry"
let prove_menu_entry = getElement AsHtml.li "why3-prove-menu-entry"
let prove100_menu_entry = getElement AsHtml.li "why3-prove100-menu-entry"
let prove1000_menu_entry = getElement AsHtml.li "why3-prove1000-menu-entry"
let clean_menu_entry = getElement AsHtml.li "why3-clean-menu-entry"
......@@ -445,8 +446,6 @@ module ToolBar =
let button_help = getElement AsHtml.button "why3-button-help"
let button_about = getElement AsHtml.button "why3-button-about"
let disable (b : <disabled : bool Js.t Js.prop; ..> Js.t) =
b ## disabled <- Js._true
......@@ -462,6 +461,15 @@ module ToolBar =
Editor.(focus editor);
Js._false)
let disable_compile () =
disable button_execute;
disable button_compile
let enable_compile () =
enable button_execute;
enable button_compile
let save () =
let data : Js.js_string Js.t =
let buffer = JSU.(fun_call (get_global "btoa") [| inject (Editor.get_value ()) |]) in
......@@ -502,7 +510,7 @@ module Panel =
let resize_bar = getElement AsHtml.div "why3-resize-bar"
let reset () =
let edit_style = editor_container ## style in
JSU.(set edit_style (Js.string "flexGrow") (Js.string "1"));
JSU.(set edit_style (Js.string "flexGrow") (Js.string "2"));
JSU.(set edit_style (Js.string "flexBasis") (Js.string ""))
let set_wide b =
main_panel ## classList ## remove (Js.string "why3-wide-view");
......@@ -557,17 +565,30 @@ module Settings =
module Controller =
struct
let task_queue = Queue.create ()
let array_for_all a f =
let rec loop i n =
if i < n then (f a.(i)) && loop (i+1) n
else true
in
loop 0 (Array.length a)
let first_task = ref true
type 'a status = Free of 'a | Busy of 'a | Absent
let num_workers = 4
let alt_ergo_steps = ref 100
let alt_ergo_workers = ref (Array.make num_workers Absent)
let why3_busy = ref false
let why3_worker = ref None
let get_why3_worker () =
match !why3_worker with
Some w -> w
| None -> log ("Why3 Worker not initialized !"); assert false
let alt_ergo_not_running () =
array_for_all !alt_ergo_workers (function Busy _ -> false | _ -> true)
let rec init_alt_ergo_worker i =
let worker = Worker.create "alt_ergo_worker.js" in
worker ## onmessage <-
......@@ -601,7 +622,8 @@ module Controller =
!alt_ergo_workers.(idx) <- Busy (w);
w ## postMessage (marshal (OptionSteps !alt_ergo_steps));
w ## postMessage (marshal task)
| _ -> ()
| _ -> if Queue.is_empty task_queue && alt_ergo_not_running ()
then ToolBar.enable_compile ()
let reset_workers () =
Array.iteri
......@@ -625,23 +647,25 @@ module Controller =
let msg = unmarshal (ev ## data) in
if !first_task then begin
first_task := false;
TaskList.clear ()
TaskList.clear ()
end;
TaskList.print_why3_output msg;
let () =
match msg with
Task (id,_,_,code,_, _, steps) ->
log ("Got task " ^ id);
push_task (Goal (id,code, steps))
| Result _ ->
ToolBar.enable_compile ()
| _ -> ()
in Js._false));
in Js._false));
worker
let () = why3_worker := Some (init_why3_worker ())
let why3_parse () =
ToolBar.disable_compile ();
TaskList.clear ();
TaskList.print_msg "Generating tasks … ";
TaskList.print_msg "<span class='fa fa-cog fa-spin'></span> Generating tasks … ";
reset_workers ();
first_task := true;
let code = Js.to_string (Editor.get_value ()) in
......@@ -649,22 +673,14 @@ module Controller =
(get_why3_worker()) ## postMessage (msg)
let why3_execute () =
ToolBar.disable_compile ();
TaskList.clear ();
TaskList.print_msg "Compiling buffer … ";
log_time "Before marshalling in main thread";
TaskList.print_msg "<span class='fa fa-cog fa-spin'></span> Compiling buffer … ";
reset_workers ();
let code = Js.to_string (Editor.get_value ()) in
(get_why3_worker()) ## postMessage (marshal (ExecuteBuffer code))
let array_for_all a f =
let rec loop i n =
if i < n then (f a.(i)) && loop (i+1) n
else true
in
loop 0 (Array.length a)
let alt_ergo_not_running () =
array_for_all !alt_ergo_workers (function Busy _ -> false | _ -> true)
let why3_transform tr f () =
if alt_ergo_not_running () then
......@@ -685,8 +701,11 @@ module Controller =
(get_why3_worker()) ## terminate ();
why3_worker := Some (init_why3_worker ());
reset_workers ();
TaskList.clear()
end
TaskList.clear ();
ToolBar.enable_compile ()
end
(* Initialisation *)
let () =
ToolBar.(add_action button_open (fun _ -> open_ ## click()));
......@@ -697,6 +716,8 @@ let () =
ToolBar.(add_action button_settings Settings.show);
ContextMenu.(add_action split_menu_entry
Controller.(why3_transform `Split ignore));
ContextMenu.(add_action prove_menu_entry
Controller.(why3_transform (`Prove(-1)) ignore));
ContextMenu.(add_action prove100_menu_entry
Controller.(why3_transform (`Prove(100)) ignore));
ContextMenu.(add_action prove1000_menu_entry
......
......@@ -400,20 +400,27 @@ let why3_run f lang code =
let () =
let free = ref true in
W.set_onmessage
(function
| Transform (`Split, id) -> why3_split id
| Transform (`Prove(steps), id) -> why3_prove ~steps id
| Transform (`Clean, id) -> why3_clean id
| ProveAll -> why3_prove_all ()
| ParseBuffer code ->
Task.clear_table ();
why3_run why3_parse_theories Env.base_language code
| ExecuteBuffer code ->
Task.clear_table ();
why3_run why3_execute Mlw_module.mlw_language code
| SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
(fun msg ->
if !free then begin
free := false;
let () =
match msg with
| Transform (`Split, id) -> why3_split id
| Transform (`Prove(steps), id) -> why3_prove ~steps id
| Transform (`Clean, id) -> why3_clean id
| ProveAll -> why3_prove_all ()
| ParseBuffer code ->
Task.clear_table ();
why3_run why3_parse_theories Env.base_language code
| ExecuteBuffer code ->
Task.clear_table ();
why3_run why3_execute Mlw_module.mlw_language code
| SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
in
free := true;
end
)
(*
Local Variables:
......
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