Commit 26f1a663 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

[trywhy3]: * replace some menu entries with icons.

	   * update the installation instruction for Font-Awesome.
parent 021ab53c
......@@ -7,11 +7,15 @@ Instructions to build TryWhy3
git clone https://github.com/ajaxorg/ace-builds.git
** copy the fontawesome webfont locally :
** Download the latest version of Font-Awesome :
https://fortawesome.github.io/Font-Awesome/
Create a directory fontawesome:
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
copy in that directory the directory fonts and css of the Font-Awesome distribution.
** install Alt-Ergo
......
@import url(fontawesome/fontawesome.css);
@import url(fontawesome/css/font-awesome.min.css);
/* fontawesome */
[class*="fontawesome-"]:before {
[class*="fa-"]:before {
font-family: 'FontAwesome', sans-serif;
}
......@@ -57,7 +57,7 @@ body {
#editor-panel {
position:absolute;
top:18pt;
top:48pt;
bottom:0pt;
display:block;
box-sizing: border-box;
......@@ -97,7 +97,7 @@ body {
height:100%;
width:100%;
font-size: large;
}
.tab-header.alert {
......@@ -154,7 +154,28 @@ body {
}
/* CSS MENU BAR */
#tool-bar {
background-color:#ddd;
position: absolute;
top: 18pt;
margin:0;
height:30pt;
width:100%;
padding:0;
line-height:30pt;
}
#tool-bar button {
color: #333;
margin-top:1pt;
margin-left:5pt;
background-image: linear-gradient(to bottom, #eee, #ccc);
border-radius:3pt;
border: solid 1pt #aaa;
font-size:14pt;
width: 28pt;
height:28pt;
vertical-align:top;
}
.menu-bar {
position:absolute;
top:0pt;
......
<!-- This document was automatically generated with yamlpp
(see http://www.lri.fr/~filliatr/yamlpp.en.html),
with the following command:
yamlpp -l en src/trywhy3/index.prehtml -o src/trywhy3/index.en.html -->
<html xmlns="http://www.w3.org/1999/xhtml"
style="font-family:Verdana,Arial,Sans-Serif">
<head>
......@@ -59,24 +53,6 @@ yamlpp -l en src/trywhy3/index.prehtml -o src/trywhy3/index.en.html -->
<li onclick="clearBuffer();">Clear buffer</li>
</ul>
</li>
<li><span>Examples</span>
<ul>
<li id="drinkers">Drinker's paradox</li>
<li id="bin_mult">Binary Multiplication</li>
<li id="fact">Factorial</li>
<li id="isqrt">Integral square root</li>
</ul>
</li>
<li><span>Why3</span>
<ul>
<li id="run">Execute Buffer</li>
<li id="prove_all">Prove All with Alt-Ergo</li>
<li id="prove">Prove Goal</li>
<li id="split_prove">Split Goal and Prove</li>
<li id="clean">Clean Goal</li>
<li id="stop">Stop Alt-ergo</li>
</ul>
</li>
<li><span>Preferences</span>
<ul>
<li onclick="document.getElementById('radio-wide').click();">
......@@ -104,6 +80,36 @@ yamlpp -l en src/trywhy3/index.prehtml -o src/trywhy3/index.en.html -->
<li style="float:right;"><span>Help</span></li>
</ul>
</div>
<div id="tool-bar">
<button id="button-execute" title="Execute buffer">
<span class="fa-arrow-circle-right"></span>
</button>
<button id="button-compile" title="Compile buffer">
<span class="fa-cogs"></span>
</button>
<button id="button-prove-all" title="Prove all tasks">
<span style="font-size:50%"
class="fa-check-square"></span><span style="font-size:50%"
class="fa-check-square"></span>
<span style="font-size:50%"
class="fa-check-square"></span><span style="font-size:50%"
class="fa-check-square"></span>
</button>
<button id="button-prove" title="Prove selected task">
<span class="fa-check-square"></span>
</button>
<button id="button-split" title="Split and prove task">
<span class="fa-share-alt"></span>
</button>
<button id="button-clean" title="Clean task">
<span class="fa-unlink"></span>
</button>
<button id="button-stop" title="Interrupt">
<span class="fa-ban"></span>
</button>
<span style="margin-left:5em;" class="fa-book"></span>
<select id="select-example" ></select>
</div>
<div id="editor-panel" class="wide-view">
<div id="editor" title="Editor" tabindex="-1" ></div><!--
Don't leave white-spaces between editor and console div's
......
......@@ -291,9 +291,9 @@ module Console =
let span_icon = Dom_html.getElementById (id ^ "_icon") in
let cls =
match st with
`New -> "fontawesome-cogs task-pending"
| `Valid -> "fontawesome-ok-sign task-valid"
| `Unknown -> "fontawesome-question-sign task-unknown"
`New -> "fa fa-fw fa-cog fa-spin fa-fw task-pending"
| `Valid -> "fa fa-fw fa-check-circle task-valid"
| `Unknown -> "fa fa-fw fa-question-circle task-unknown"
in
span_icon ## className <- Js.string cls
with
......@@ -302,7 +302,7 @@ module Console =
let set_abort_icon () =
let list = Dom_html.document ## getElementsByClassName (Js.string "task-pending") in
List.iter (fun span ->
span ## className <- (Js.string "fontawesome-minus-sign task-abort"))
span ## className <- (Js.string "fa fa-fw fa-minus-circle task-abort"))
(Dom.list_of_nodeList list)
end
......@@ -442,16 +442,17 @@ let why3_transform tr f () =
let () =
add_button "prove_all" why3_parse ;
add_button "run" why3_execute ;
add_button "stop" (fun () ->
(get_why3_worker()) ## terminate ();
why3_worker := Some (init_why3_worker ());
reset_workers ();
Console.set_abort_icon());
add_button "prove" (why3_transform `Prove (fun _ -> ()));
add_button "split_prove" (why3_transform `Split (fun _ -> ()));
add_button "clean" (why3_transform `Clean Console.clean_task);
add_button "button-execute" why3_execute ;
add_button "button-compile" why3_parse ; (* todo : change *)
add_button "button-prove-all" why3_parse ;
add_button "button-prove" (why3_transform `Prove (fun _ -> ()));
add_button "button-split" (why3_transform `Split (fun _ -> ()));
add_button "button-clean" (why3_transform `Clean Console.clean_task);
add_button "button-stop" (fun () ->
(get_why3_worker()) ## terminate ();
why3_worker := Some (init_why3_worker ());
reset_workers ();
Console.set_abort_icon());
let input_threads = get_opt Dom_html.(CoerceTo.input
(getElementById "input-num-threads"))
......
Supports Markdown
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