Commit 191ea2b4 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Upgrade trywhy3 to FontAwesome 5.

Note that the old instructions were outdated because FontAwesome's git
repository has been completely restructured. It was not obvious which
files had to be locally installed, so the remote version is now used.
parent c6673f68
......@@ -1740,10 +1740,7 @@ ALTERGOCMO = \
TRYWHY3CMO=lib/why3/why3.cma
TRYWHY3FILES=trywhy3.js trywhy3.html trywhy3.css \
README examples/ \
trywhy3_custom.css gen_index.sh fontawesome/css/font-awesome.min.css \
fontawesome/fonts/FontAwesome.otf fontawesome/fonts/fontawesome-webfont.svg \
fontawesome/fonts/fontawesome-webfont.woff fontawesome/fonts/fontawesome-webfont.eot \
fontawesome/fonts/fontawesome-webfont.ttf fontawesome/fonts/fontawesome-webfont.woff2 \
trywhy3_custom.css gen_index.sh \
ace-builds/src-min-noconflict/ace.js ace-builds/src-min-noconflict/mode-why3.js \
ace-builds/src-min-noconflict/theme-chrome.js $(JS_MAPS)
......
......@@ -11,11 +11,6 @@ Instructions to build TryWhy3
cp mode-why3.js ace-builds/src-min-noconflict
** Download the latest version of Font-Awesome in a directory named 'fontawesome' :
git clone https://github.com/FortAwesome/Font-Awesome.git fontawesome
** install Alt-Ergo
- get sources of Alt-Ergo and put them in directory src/trywhy3/ e.g. in
......
@import url(fontawesome/css/font-awesome.min.css);
/* fontawesome */
[class*="fa-"]:before {
font-family: 'FontAwesome', sans-serif;
}
/****** GLOBAL LAYOUT *********/
body {
padding:0;
......@@ -94,7 +87,7 @@ body {
}
#why3-top-button-bar .why3-button {
font-size:14pt;
width:1.8em;
width:2.1em;
display:inline-block;
height:1.6em;
}
......
......@@ -3,10 +3,11 @@
<head>
<title>Try Why3</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" href="https://use.fontawesome.com/releases/v5.0.13/css/solid.css" integrity="sha384-Rw5qeepMFvJVEZdSo1nDQD5B6wX0m7c5Z/pLNvjkB14W6Yki1hKbSEQaX9ffUbWe" crossorigin="anonymous">
<link rel="stylesheet" href="https://use.fontawesome.com/releases/v5.0.13/css/fontawesome.css" integrity="sha384-GVa9GOgVQgOk+TNYXu7S/InPTfSDTtBalSgkgqQ7sCik56N9ztlkoTr2f/T44oKV" crossorigin="anonymous">
<link rel="stylesheet" type="text/css" href="trywhy3.css" />
<link rel="stylesheet" type="text/css" href="trywhy3_custom.css"/>
<script defer="defer" src="ace-builds/src-min-noconflict/ace.js"
type="text/javascript" charset="utf-8"></script>
......@@ -28,11 +29,11 @@
<div class="why3-button-group">
<button id="why3-button-open" class="why3-button"
title="Open file (ctrl-o)">
<span class="fa-folder-open"></span>
<span class="fas fa-folder-open"></span>
</button>
<button id="why3-button-save" class="why3-button"
title="Save file (ctrl-s)">
<span class="fa-cloud-download"></span>
<span class="fas fa-save"></span>
</button>
</div>
......@@ -40,18 +41,18 @@
<div class="why3-button-group">
<button id="why3-button-undo" class="why3-button"
title="Undo edit (ctrl-z)">
<span class="fa-undo"></span>
<span class="fas fa-undo"></span>
</button>
<button id="why3-button-redo" class="why3-button"
title="Repeat edit (ctrl-y)">
<span class="fa-repeat"></span>
<span class="fas fa-redo"></span>
</button>
</div>
<div class="why3-separator" style="width:2em;"></div>
<div class="why3-button-group">
<span id="why3-example-label" class="fa fa-spin fa-refresh why3-icon"></span>
<span id="why3-example-label" class="fas fa-spin fa-refresh why3-icon"></span>
<select id="why3-select-example"
title="Choose a predefined example">
<option disabled="disabled" selected="selected">&nbsp;</option>
......@@ -62,28 +63,28 @@
<div class="why3-button-group">
<button id="why3-button-compile" class="why3-button" title="Verify">
<span class="fa-cogs"></span>
<span class="fas fa-cogs"></span>
</button>
<button id="why3-button-execute" class="why3-button" title="Execute">
<span class="fa-arrow-circle-right"></span>
<span class="fas fa-arrow-circle-right"></span>
</button>
<button id="why3-button-stop" class="why3-button" title="Interrupt">
<span class="fa-ban"></span>
<span class="fas fa-ban"></span>
</button>
</div>
<div class="why3-button-group why3-flushright">
<button id="why3-button-settings" class="why3-button"
title="Settings…">
<span class="fa-wrench"></span>
<span class="fas fa-wrench"></span>
</button>
<button id="why3-button-help" class="why3-button"
title="Help">
<span class="fa-question-circle"></span>
<span class="fas fa-question-circle"></span>
</button>
<button id="why3-button-about" class="why3-button"
title="About">
<span class="fa-info-circle"></span>
<span class="fas fa-info-circle"></span>
</button>
</div>
......@@ -115,22 +116,22 @@
<!-- context menu -->
<div class="why3-contextmenu why3-widget" id="why3-task-menu">
<ul>
<li id="why3-split-menu-entry"><span class="fa-share-alt
<li id="why3-split-menu-entry"><span class="fas fa-share-alt
why3-icon"></span> Split and prove </li>
<li id="why3-prove-menu-entry"><span class="fa-check-square
<li id="why3-prove-menu-entry"><span class="fas fa-check-square
why3-icon"></span>
Prove (default) </li>
<li id="why3-prove100-menu-entry"><span class="fa-check-square
<li id="why3-prove100-menu-entry"><span class="fas fa-check-square
why3-icon"></span>
Prove (100
steps) </li>
<li id="why3-prove1000-menu-entry"><span class="fa-check-square
<li id="why3-prove1000-menu-entry"><span class="fas fa-check-square
why3-icon"></span>
Prove (1000 steps) </li>
<li id="why3-prove5000-menu-entry"><span class="fa-check-square
<li id="why3-prove5000-menu-entry"><span class="fas fa-check-square
why3-icon"></span>
Prove (5000 steps) </li>
<li id="why3-clean-menu-entry"><span class="fa-unlink why3-icon"></span>
<li id="why3-clean-menu-entry"><span class="fas fa-unlink why3-icon"></span>
Clean </li>
</ul>
</div>
......@@ -194,7 +195,7 @@
<button id="why3-close-dialog-button"
style="float:right;"
class="why3-button"
title="Close"><span class="fa-times"></span></button>
title="Close"><span class="fas fa-times"></span></button>
</div>
</div>
</body>
......
......@@ -341,9 +341,9 @@ module ExampleList =
let set_loading_label b =
select_example ## disabled <- (Js.bool b);
if b then
example_label ## className <- Js.string "fa fa-spin fa-refresh why3-icon"
example_label ## className <- Js.string "fas fa-spin fa-refresh why3-icon"
else
example_label ## className <- Js.string "fa-book why3-icon"
example_label ## className <- Js.string "fas fa-book why3-icon"
let selected_index = ref 0
let unselect () =
......@@ -573,10 +573,10 @@ module TaskList =
let span_msg = getElement AsHtml.span (id ^ "_msg") in
let cls =
match st with
`New -> "fa fa-fw fa-cog fa-spin fa-fw why3-task-pending"
`New -> "fas fa-fw fa-cog fa-spin fa-fw why3-task-pending"
| `Valid -> span_msg ## innerHTML <- Js.string "";
"fa-check-circle why3-task-valid"
| `Unknown -> "fa-question-circle why3-task-unknown"
"fas fa-check-circle why3-task-valid"
| `Unknown -> "fas fa-question-circle why3-task-unknown"
in
span_icon ## className <- Js.string cls
with
......@@ -962,7 +962,7 @@ module Controller =
ToolBar.disable_compile ();
why3_busy := true;
TaskList.clear ();
TaskList.print_msg "<span class='fa fa-cog fa-spin'></span> Generating tasks … ";
TaskList.print_msg "<span class='fas fa-cog fa-spin'></span> Generating tasks … ";
reset_workers ();
first_task := true;
let code = Js.to_string (Editor.get_value ()) in
......@@ -974,7 +974,7 @@ module Controller =
ToolBar.disable_compile ();
why3_busy := true;
TaskList.clear ();
TaskList.print_msg "<span class='fa fa-cog fa-spin'></span> Compiling buffer … ";
TaskList.print_msg "<span class='fas 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))
......
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