alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

Updates to the ltl2tgba ajax version.

Browse source 
* wrap/python/ajax/ltl2tgba.html: Remove the auto-update button, and
enable auto-update automatically after the first submission.  Add
tools tips for the "Desired Output" tabs, and the Spot logo.
Add a email icon to encourage feedback.
* wrap/python/ajax/ltl2tgba.css: fix sizes of formula field and
send button.  Set position of mail icon.
* wrap/python/ajax/logos/mail.png: New logo, based on a public
domain SVG icon retrieved today from
http://commons.wikimedia.org/wiki/File:Internet-mail.svg
This commit is contained in:
Alexandre Duret-Lutz 2011-01-26 22:03:14 +01:00
parent c7f3bd5111
commit f3c6f01e8d
4 changed files with 42 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

14
ChangeLog
View file

@ -1,3 +1,17 @@
2011-01-26 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Updates to the ltl2tgba ajax version.
* wrap/python/ajax/ltl2tgba.html: Remove the auto-update button, and
enable auto-update automatically after the first submission. Add
tools tips for the "Desired Output" tabs, and the Spot logo.
Add a email icon to encourage feedback.
* wrap/python/ajax/ltl2tgba.css: fix sizes of formula field and
send button. Set position of mail icon.
* wrap/python/ajax/logos/mail.png: New logo, based on a public
domain SVG icon retrieved today from
http://commons.wikimedia.org/wiki/File:Internet-mail.svg
2011-01-19 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2011-01-19 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* wrap/python/ajax/ltl2tgba.html: Disable the browser spellcheck * wrap/python/ajax/ltl2tgba.html: Disable the browser spellcheck

13
wrap/python/ajax/css/ltl2tgba.css
View file

@ -5,6 +5,13 @@ html {overflow-y:scroll;}
font-size: 1em; font-size: 1em;
} }
input.formula {
width: 700px;
}
div#send {
width: 80px;
}
div.ltl2tgba { div.ltl2tgba {
width: 800px; width: 800px;
position:relative; position:relative;
@ -33,6 +40,12 @@ div.ltl2tgba {
bottom:10px; bottom:10px;
z-index:1; z-index:1;
} }
#mailicon {
position:fixed;
left:10px;
top:84px;
z-index:1;
}
.ltl2tgba div.ui-widget-content { .ltl2tgba div.ui-widget-content {
padding: 3px; padding: 3px;

BIN
wrap/python/ajax/logos/mail.png Normal file
View file

Binary file not shown.
Side by side

After

Width:  |  Height:  |  Size: 3.9 KiB

26
wrap/python/ajax/ltl2tgba.html
View file

@ -13,8 +13,11 @@
<script type="text/javascript" src="js/jquery.tipTip.minified.js"></script> <script type="text/javascript" src="js/jquery.tipTip.minified.js"></script>
<script type="text/javascript"> <script type="text/javascript">
jQuery(document).ready(function(){ jQuery(document).ready(function(){
$.spotvars = {
autoupdate: 0
}
$(".tabs").tabs(); $(".tabs").tabs();
$("#send,#autoupdate").button(); $("#send").button();
$("#results").hide(); $("#results").hide();
$(".tabs a").click(function() {return false;}); $(".tabs a").click(function() {return false;});
$(".rtip").tipTip({maxWidth: "300px", delay: 1000, $(".rtip").tipTip({maxWidth: "300px", delay: 1000,
@ -74,8 +77,7 @@
str, str,
function(response, status, xhr) function(response, status, xhr)
{ {
// $("#autoupdate").attr("checked", true); $.spotvars.autoupdate = 1;
// $("#autoupdate").button("refresh");
if (status == "error") { if (status == "error") {
var msg = "Sorry but there was an error: "; var msg = "Sorry but there was an error: ";
$("#results-body").html(msg + xhr.status + " " $("#results-body").html(msg + xhr.status + " "
@ -89,7 +91,7 @@
);} );}
function autoUpdate() { function autoUpdate() {
if ($("#autoupdate").attr("checked")) if ($.spotvars.autoupdate)
updateResults(); updateResults();
return true; return true;
} }
@ -113,7 +115,7 @@
} }
return false; return false;
}); });
$('#output-tabs').bind("tabsselect", function(event, ui) { $("#output-tabs").bind("tabsselect", function(event, ui) {
switch (ui.panel.id) switch (ui.panel.id)
{ {
case 'tabs-formula': case 'tabs-formula':
@ -149,7 +151,9 @@
</head> </head>
<body> <body>
<div id="spotlogo"> <div id="spotlogo">
<a href="http://spot.lip6.fr/"><img border=0 src="logos/spot64s.png" alt="Spot Logo"></a></div> <a href="http://spot.lip6.fr/"><img border=0 src="logos/spot64s.png" alt="Spot Logo" class="rtip" title="This on-line tool is using the <b>Spot</b> library to process LTL formulas and automata. Please download <b>Spot</b> and install it on your computer if you want to do the same from the command line, or from another program."></a></div>
<div id="mailicon">
<a href="mailto:spot@lrde.epita.fr"><img border=0 src="logos/mail.png" alt="Spot Logo" class="rtip" title="A bug? A question? Please e-mail us at <b>spot@lrde.epita.fr</b>."></a></div>
<div id="lrdelogo"> <div id="lrdelogo">
<a href="http://www.lrde.epita.fr/"><img border=0 src="logos/lrde64.png" alt="LRDE Logo"></a></div> <a href="http://www.lrde.epita.fr/"><img border=0 src="logos/lrde64.png" alt="LRDE Logo"></a></div>
<div id="lip6logo"> <div id="lip6logo">
@ -160,7 +164,7 @@
<div class="ui-widget ui-widget-content ui-corner-all collapsible"> <div class="ui-widget ui-widget-content ui-corner-all collapsible">
<h3 id="ltl-head" class="ui-widget-header ui-corner-all head">LTL Formula to translate<span class="ui-icon ui-icon-circle-arrow-n ltltip">Fold</span></h3> <h3 id="ltl-head" class="ui-widget-header ui-corner-all head">LTL Formula to translate<span class="ui-icon ui-icon-circle-arrow-n ltltip">Fold</span></h3>
<div class="dontcollapse"> <div class="dontcollapse">
<INPUT class="formula" size="60" type="text" name="f" value=""> <div id="send">Send</div> <input type="checkbox" id="autoupdate"><label for="autoupdate" class="btip" title="When <b>Auto-Update</b> is <b>on</b>, the results are updated automatically every time an option or the formula is changed.">Auto-Update</label> <INPUT class="formula" type="text" name="f" value=""> <div id="send" class="btip" title="Submit the formula and all options. You may simply hit <b>enter</b> after typing the formula. After the first submission the form will auto-update itself anytime you change an option.">Send</div>
</div> </div>
<div id="ltl-help"> <div id="ltl-help">
<p>Use alphanumeric identifiers or double-quoted strings for atomic <p>Use alphanumeric identifiers or double-quoted strings for atomic
@ -254,10 +258,10 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
<div id="output-tabs" class="tabs collapsible"> <div id="output-tabs" class="tabs collapsible">
<ul class="head"> <ul class="head">
<li>Desired Output:</li> <li>Desired Output:</li>
<li><a href="#tabs-formula">Formula</a></li> <li><a href="#tabs-formula" class="btip" title="Simplify the formula, but do not convert it as an automaton.">Formula</a></li>
<li><a href="#tabs-monitor">Monitor</a></li> <li><a href="#tabs-monitor" class="btip" title="Create a monitor accepting all finite prefixes compatible with the formula.">Monitor</a></li>
<li><a href="#tabs-automaton">B&uuml;chi Automaton</a></li> <li><a href="#tabs-automaton" class="btip" title="Translate the LTL formula into B&uuml;chi automaton.">B&uuml;chi Automaton</a></li>
<li><a href="#tabs-run">B&uuml;chi Run</a></li> <li><a href="#tabs-run" class="btip" title="Translate the LTL formula into B&uuml;chi automaton, and exhibit an accepting run.">B&uuml;chi Run</a></li>
<li class="ui-icon ui-icon-circle-arrow-n ftip">Fold/li> <li class="ui-icon ui-icon-circle-arrow-n ftip">Fold/li>
</ul> </ul>
<input type="hidden" name="o"> <input type="hidden" name="o">