Commit dd57d2e7 authored by MARCHE Claude's avatar MARCHE Claude

Try Why3: version francaise

parent 016365db
...@@ -271,7 +271,10 @@ pvsbin/ ...@@ -271,7 +271,10 @@ pvsbin/
# Try Why3 # Try Why3
/src/trywhy3/trywhy3.js /src/trywhy3/trywhy3.js
/src/trywhy3/trywhy3.byte /src/trywhy3/trywhy3.byte
/src/trywhy3/theories.ml /src/trywhy3/index.en.html
/src/trywhy3/index.fr.html
/src/trywhy3/ace-builds
/src/trywhy3/alt-ergo-0.99.1
# jessie3 # jessie3
/src/jessie/config.log /src/jessie/config.log
......
...@@ -1436,6 +1436,14 @@ ALTERGOMODS=util/numbers util/version util/options parsing/why_parser parsing/wh ...@@ -1436,6 +1436,14 @@ ALTERGOMODS=util/numbers util/version util/options parsing/why_parser parsing/wh
TRYWHY3CMO=lib/why3/why3.cma TRYWHY3CMO=lib/why3/why3.cma
# $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS))) # $(addprefix $(ALTERGODIR)/src/, $(addsuffix .cmo,$(ALTERGOMODS)))
trywhy3: src/trywhy3/trywhy3.js src/trywhy3/index.en.html src/trywhy3/index.fr.html
%.fr.html: %.prehtml
yamlpp -l fr $< -o $@
%.en.html: %.prehtml
yamlpp -l en $< -o $@
src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte src/trywhy3/trywhy3.js: src/trywhy3/trywhy3.byte
js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \ js_of_ocaml --extern-fs -I . -I src/trywhy3 --file=trywhy3.conf:/ \
--file=try_alt_ergo.drv:/ \ --file=try_alt_ergo.drv:/ \
......
<html xmlns="http://www.w3.org/1999/xhtml" <html xmlns="http://www.w3.org/1999/xhtml"
style="font-family:Verdana,Arial,Sans-Serif"> style="font-family:Verdana,Arial,Sans-Serif">
<head> <head>
<title>Try Why3</title> <title>
<#en>Try Why3</#en><#fr>Essayez Why3</#fr>
</title>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" type="text/css" href="style.css" /> <link rel="stylesheet" type="text/css" href="style.css" />
<!-- color customisation --> <!-- color customisation -->
...@@ -20,72 +22,138 @@ ...@@ -20,72 +22,138 @@
<input type="file" id="file-selector" /> <input type="file" id="file-selector" />
<div id="background-shadow"> <div id="background-shadow">
<div id="confirm-dialog" > <div id="confirm-dialog" >
The content of the current buffer will be lost.<br/> <#en>The content of the current buffer will be lost</#en>
<#fr>Le contenu actuel du programme sera perdu</#fr>
<br/>
<div style="width:70%; display:inline-block;"> <div style="width:70%; display:inline-block;">
<button class="btn" <button class="btn"
onclick="confirmReplace();">Confirm</button> onclick="confirmReplace();">
<#en>Confirm</#en>
<#fr>Confirmer</#fr>
</button>
<button class="btn" <button class="btn"
onclick="cancelReplace();">Cancel</button> onclick="cancelReplace();">
<#en>Cancel</#en>
<#fr>Annuler</#fr>
</button>
</div> </div>
</div> </div>
</div> </div>
<!-- the main page --> <!-- the main page -->
<h1 style="background-color:#356aa0;color:#fff">Try Why3</h1> <div align="right">
<p>Type some program in the text area below, then select <#fr><a href="index.en.html">English version</a></#fr>
'Prove all' in the Why3 menu to generate proof obligations.</p> <#en><a href="index.fr.html">Version fran&ccedil;aise</a></#en>
<p>Related links </div>
<h1 style="background-color:#356aa0;color:#fff">
<#en>Try Why3</#en><#fr>Essayez Why3</#fr>
</h1>
<p>
<#en>
Type some program in the text area below, then select
'Prove all' in the Why3 menu to generate proof obligations.
</#en>
<#fr>
Tapez un programme dans la zone de texte ci-dessous, puis
s&eacute;lectionnez 'Prouver' dans le menu Why3 pour engendrer
les obligations de preuve.
</#fr>
</p>
<p><#en>Related links</#en><#fr>Liens utiles</#fr>
<ul> <ul>
<li>The <a href="http://why3.lri.fr/">Why3 home page</a> <li><#en>The</#en><#fr>La</#fr>
<li>The <a href="http://ocsigen.org/js_of_ocaml/">Js_of_ocaml</a> <a href="http://why3.lri.fr/">
compiler used to produce this page <#en>Why3 home page</#en>
<#fr>page principale de Why3</#fr>
</a>
<li><#en>The</#en><#fr>Le compilateur</#fr>
<a href="http://ocsigen.org/js_of_ocaml/">
Js_of_ocaml</a>
<#en>compiler used to produce this page</#en>
<#fr>utilis&eacute; pour produire cette page</#fr>
</ul> </ul>
</p> </p>
<div class="menu-bar"> <div class="menu-bar">
<ul> <ul>
<li><a href="#">File</a> <li><a href="#"><#en>File</#en><#fr>Fichier</#fr></a>
<ul> <ul>
<li><a href="#" onclick="openFile();">Open file…</a></li> <li><a href="#" onclick="openFile();">
<li><a href="#" onclick="saveFile();">Save file as…</a></li> <#en>Open</#en><#fr>Ouvrir</#fr>
</a></li>
<li><a href="#" onclick="saveFile();">
<#en>Save as</#en><#fr>Enregister sous</#fr>
</a></li>
</ul> </ul>
</li> </li>
<li><a href="#">Edit</a> <li><a href="#"><#en>Edit</#en><#fr>Edition</#fr></a>
<ul> <ul>
<li><a href="#" onclick="editor.undo();">Undo</a></li> <li><a href="#" onclick="editor.undo();">
<li><a href="#" onclick="editor.redo();">Redo</a></li> <#en>Undo</#en><#fr>Annuler</#fr>
<li><a href="#" onclick="clearBuffer();">Clear buffer</a></li> </a></li>
<li><a href="#" onclick="editor.redo();">
<#en>Redo</#en><#fr>R&eacute;tablir</#fr>
</a></li>
<li><a href="#" onclick="clearBuffer();">
<#en>Clear buffer</#en><#fr>Tout effacer</#fr>
</a></li>
</ul> </ul>
</li> </li>
<li><a href="#">Examples</a> <li><a href="#"><#en>Examples</#en><#fr>Exemples</#fr></a>
<ul> <ul>
<li><a href="#"><div id="drinkers">Drinker's paradox</div></a></li> <li><a href="#"><div id="drinkers">
<li><a href="#"><div id="simplearith">Simple Arithmetic</div></a></li> <#en>Drinker's paradox</#en>
<li><a href="#"><div id="isqrt">Integral square root</div></a></li> <#fr>Paradoxe des buveurs</#fr>
</div></a></li>
<li><a href="#"><div id="simplearith">
<#en>Simple Arithmetic</#en>
<#fr>Arithm&eacute;tique simple</#fr>
</div></a></li>
<li><a href="#"><div id="isqrt">
<#en>Integral square root</#en>
<#fr>Racine carr&eacute;e enti&egrave;re</#fr>
</div></a></li>
</ul> </ul>
</li> </li>
<li><a href="#">Why3</a> <li><a href="#">Why3</a>
<ul> <ul>
<li><a href="#" id="run">Run main function</a></li> <li><a href="#" id="run">
<li><a href="#" id="prove">Prove all</a></li> <#en>Run main function</#en>
<#fr>Ex&eacute;cuter la fonction main</#fr>
</a></li>
<li><a href="#" id="prove">
<#en>Prove</#en>
<#fr>Prouver</#fr>
</a></li>
</ul> </ul>
</li> </li>
<li><a href="#">Preferences</a> <li><a href="#">
<#en>Preferences</#en>
<#fr>Pr&eacute;f&eacute;rences</#fr>
</a>
<ul> <ul>
<li><a href="#" <li><a href="#"
onclick="document.getElementById('radio-wide').click();" onclick="document.getElementById('radio-wide').click();"
> >
<input id="radio-wide" type="radio" name="view" <input id="radio-wide" type="radio" name="view"
value="wide" checked="checked" onchange="widescreenView();" value="wide" checked="checked" onchange="widescreenView();"
/>Split Vertically</a> />
<#en>Split Vertically</#en>
<#fr>S&eacute;paration verticale</#fr>
</a>
</li> </li>
<li><a href="#" <li><a href="#"
onclick="document.getElementById('radio-std').click();" onclick="document.getElementById('radio-std').click();"
> >
<input id="radio-std" type="radio" name="view" value="std" <input id="radio-std" type="radio" name="view" value="std"
onchange="standardView();" onchange="standardView();"
/>Split Horizontally</a></li> />
<#en>Split Horizontally</#en>
<#fr>S&eacute;paration horizontale</#fr>
</a></li>
</ul> </ul>
</li> </li>
<li style="float:right;"><a href="#">Help</a></li> <li style="float:right;"><a href="#">
<#en>Help</#en><#fr>Aide</#fr>
</a></li>
</ul> </ul>
</div> </div>
<div id="editor-panel"> <div id="editor-panel">
......
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