Skip to content

GitLab

why3
why3

Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 4f5c050c authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files
Options

[trywhy3]: * restore undo/redo feature 

           * help button opens a trywhy3_help.html (that needs to be written)
           * disable the code pane while compiling
           * some more tweaks of the CSS and HTML
parent 23e2e9c3
Hide whitespace changes
Inline Side-by-side
Showing with 97 additions and 7 deletions
src/trywhy3/trywhy3.css
View file @ 4f5c050c
......@@ -35,6 +35,7 @@ body {
-ms-user-select: none; /* IE/Edge */
user-select: none; /* non-prefixed version, currently
not supported by any browser */
cursor:default;
}
#why3-top-button-bar {
......@@ -149,6 +150,19 @@ body {
padding:0;
margin:0;
}
#why3-editor-bg {
display:none;
position:absolute;
opacity:0.75;
top:0;
left:0;
width:100%;
height:100%;
z-index:100;
}
#why3-editor-bg:hover {
cursor:progress;
}
/*** TABS ***/
......
src/trywhy3/trywhy3.html
View file @ 4f5c050c
......@@ -17,16 +17,31 @@
<body>
<div id="why3-main-container" class="why3-container">
<div id="why3-top-button-bar" class="why3-widget why3-button-bar">
<div class="why3-separator" style="width:0.1em;"></div>
<div class="why3-button-group">
<button id="why3-button-open" class="why3-button" title="Open file">
<div class="why3-button-group">
<button id="why3-button-open" class="why3-button"
title="Open file (ctrl-o)">
<span class="fa-folder-open"></span>
</button>
<button id="why3-button-save" class="why3-button" title="Save file">
<button id="why3-button-save" class="why3-button"
title="Save file (ctrl-s)">
<span class="fa-cloud-download"></span>
</button>
</div>
<div class="why3-separator" style="width:2em;"></div>
<div class="why3-button-group">
<button id="why3-button-undo" class="why3-button"
title="Undo edit (ctrl-z)">
<span class="fa-undo"></span>
</button>
<button id="why3-button-redo" class="why3-button"
title="Repeat edit (ctrl-y)">
<span class="fa-repeat"></span>
</button>
</div>
<div class="why3-separator" style="width:2em;"></div>
<div class="why3-button-group">
......@@ -69,6 +84,7 @@
<div id="why3-main-panel" class="why3-wide-view">
<div id="why3-editor-container" class="why3-container">
<div id="why3-editor-bg" class="why3-widget"> </div>
<div id="why3-editor" tabindex="-1" ></div>
</div>
<div id="why3-resize-bar" class="why3-widget" ></div>
......@@ -147,7 +163,7 @@
file <a href="https://scm.gforge.inria.fr/anonscm/gitweb?p=why3/why3.git;a=blob_plain;f=LICENSE">LICENSE</a>.
</p>
<p>TryWhy3 relies on the following excellent open source
softwares and resources :
softwares and resources:
</p>
<ul>
<li>A Javascript version of
......
src/trywhy3/trywhy3.ml
View file @ 4f5c050c
......@@ -121,7 +121,10 @@ module Editor =
) [ editor; task_viewer ];
JSU.(meth_call task_viewer "setReadOnly" [| inject Js._true|])
let undo () =
ignore JSU.(meth_call editor "undo" [| |])
let redo () =
ignore JSU.(meth_call editor "redo" [| |])
let get_value ?(editor=editor) () : Js.js_string Js.t =
JSU.meth_call editor "getValue" [| |]
......@@ -173,6 +176,20 @@ module Editor =
let set_on_event e f =
ignore JSU.(meth_call editor "on" [| inject (Js.string e);
inject f|])
let editor_bg = getElement AsHtml.div "why3-editor-bg"
let disable () =
ignore JSU.(meth_call editor "setReadOnly" [| inject Js._true|]);
editor_bg ## style ## display <- Js.string "block"
let enable () =
ignore JSU.(meth_call editor "setReadOnly" [| inject Js._false|]);
editor_bg ## style ## display <- Js.string "none"
end
module Tabs =
......@@ -336,7 +353,14 @@ module TaskList =
let doc = Dom_html.document in
(* see why3_worker.ml *)
match o with
| Idle -> ()
| Idle | Warning [] -> ()
| Warning lst ->
let annot =
List.map (fun ((l1, c1), msg) ->
(l1,c1, Js.string msg, Js.string "warning")) lst
in
Editor.set_annotations annot
| Error s -> print_error s
| ErrorLoc ((l1, b, l2, e), s) ->
......@@ -475,6 +499,10 @@ module ToolBar =
let button_open = getElement AsHtml.button "why3-button-open"
let real_save = getElement AsHtml.a "why3-save-as"
let button_save = getElement AsHtml.button "why3-button-save"
let button_undo = getElement AsHtml.button "why3-button-undo"
let button_redo = getElement AsHtml.button "why3-button-redo"
let button_execute = getElement AsHtml.button "why3-button-execute"
let button_compile = getElement AsHtml.button "why3-button-compile"
let button_stop = getElement AsHtml.button "why3-button-stop"
......@@ -506,16 +534,22 @@ module ToolBar =
let disable_compile () =
Editor.disable ();
ContextMenu.disable ();
ExampleList.disable ();
disable button_open;
disable button_undo;
disable button_redo;
disable button_execute;
disable button_compile
let enable_compile () =
Editor.enable ();
ContextMenu.enable ();
ExampleList.enable ();
enable button_open;
enable button_undo;
enable button_redo;
enable button_execute;
enable button_compile
......@@ -816,10 +850,21 @@ let () =
ToolBar.(add_action button_save save);
KeyBinding.add_global ~ctrl:Js._true 83 ToolBar.save;
ToolBar.(add_action button_undo Editor.undo);
KeyBinding.add_global ~ctrl:Js._true 90 Editor.undo;
ToolBar.(add_action button_redo Editor.redo);
KeyBinding.add_global ~ctrl:Js._true 89 Editor.redo;
ToolBar.(add_action button_execute Controller.why3_execute);
ToolBar.(add_action button_compile Controller.why3_parse);
ToolBar.(add_action button_stop Controller.stop);
ToolBar.(add_action button_settings Dialogs.(show setting_dialog));
ToolBar.(add_action button_help (fun () ->
Dom_html.window ## open_ (Js.string "trywhy3_help.html",
Js.string "_blank",
Js.null)));
ToolBar.(add_action button_about Dialogs.(show about_dialog));
ContextMenu.(add_action split_menu_entry
Controller.(why3_transform `Split ignore));
......
src/trywhy3/why3_worker.ml
View file @ 4f5c050c
......@@ -94,9 +94,20 @@ module Task =
let get_parent_id id = (get_info id).parent_id
let mk_loc (_, a,b,c) = (a,b,c)
let warnings = ref []
let clear_warnings () = warnings := []
let () =
Warning.set_hook (fun ?(loc=(Loc.user_position "" 1 0 0)) msg ->
let _, a,b,c = Loc.get loc in
warnings := ((a-1,b), msg) :: !warnings)
let premise_kind = function
| { Term. t_node = Term.Tnot _; t_loc = None } -> "why3-loc-neg-premise"
| _ -> "why3-loc-premise"
| _ -> "why3-loc-premise"
let collect_locs t =
(* from why 3 ide *)
let locs = ref [] in
......@@ -382,6 +393,7 @@ let why3_run f lang code =
close_out ch;
let theories = Env.read_file lang env temp_file_name in
W.send (Warning !Task.warnings);
f theories
with
| Loc.Located(loc,e') ->
......@@ -406,9 +418,11 @@ let () =
| Transform (`Clean, id) -> why3_clean id
| ProveAll -> why3_prove_all ()
| ParseBuffer code ->
Task.clear_warnings ();
Task.clear_table ();
why3_run why3_parse_theories Env.base_language code
| ExecuteBuffer code ->
Task.clear_warnings ();
Task.clear_table ();
why3_run why3_execute Mlw_module.mlw_language code
| SetStatus (st, id) -> List.iter W.send (Task.set_status id st)
......
src/trywhy3/worker_proto.ml
View file @ 4f5c050c
......@@ -27,6 +27,7 @@ type why3_output = Error of string (* msg *)
(* id, parent id, expl, code, location list, pretty, steps*)
| Result of string list
| UpdateStatus of status * id
| Warning of ((int*int) * string) list
| Idle
type prover_command = OptionSteps of int | Goal of id * string * int
......
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