From 81d3ee48f0554af071bd49fe9a520189adb4f6b5 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Sat, 2 Jun 2012 11:06:19 +0200
Subject: [PATCH] ltl2tgba.html: Display a loading logo for delayed results.

* wrap/python/ajax/css/loading.gif: New file.
* wrap/python/ajax/css/ltl2tgba.css (.loading): New class.
* wrap/python/ajax/ltl2tgba.html: Display loading.gif after 200ms if
the answer hasn't arrived
* wrap/python/ajax/spot.in: Do not suggest not to draw the automaton
on timeout.
* wrap/python/ajax/js/jquery.ba-dotimeout.min.js: New file.
* wrap/python/ajax/Makefile.am: Distribute it.
---
 wrap/python/ajax/Makefile.am                  |   5 ++--
 wrap/python/ajax/css/loading.gif              | Bin 0 -> 4176 bytes
 wrap/python/ajax/css/ltl2tgba.css             |   6 +++++
 .../python/ajax/js/jquery.ba-dotimeout.min.js |   9 +++++++
 wrap/python/ajax/ltl2tgba.html                |  22 +++++++++++++++---
 wrap/python/ajax/spot.in                      |   2 +-
 6 files changed, 38 insertions(+), 6 deletions(-)
 create mode 100644 wrap/python/ajax/css/loading.gif
 create mode 100644 wrap/python/ajax/js/jquery.ba-dotimeout.min.js

diff --git a/wrap/python/ajax/Makefile.am b/wrap/python/ajax/Makefile.am
index 48aad3e39..d881b3921 100644
--- a/wrap/python/ajax/Makefile.am
+++ b/wrap/python/ajax/Makefile.am
@@ -23,8 +23,9 @@
 nodist_noinst_SCRIPTS = spot.py
 EXTRA_DIST = $(srcdir)/spot.in README ltl2tgba.html css/ltl2tgba.css	\
   css/tipTip.css js/jquery.tipTip.minified.js js/jquery.ba-bbq.min.js	\
-  logos/lip6sys64.png logos/lrde64.png logos/spot64s.png		\
-  logos/mail.png css/ui-lightness/jquery-ui-1.8.13.custom.css		\
+  js/jquery.ba-dotimeout.min.js logos/lip6sys64.png logos/lrde64.png	\
+  logos/spot64s.png logos/mail.png					\
+  css/ui-lightness/jquery-ui-1.8.13.custom.css				\
   css/ui-lightness/images/ui-icons_222222_256x240.png			\
   css/ui-lightness/images/ui-bg_glass_100_f6f6f6_1x400.png		\
   css/ui-lightness/images/ui-bg_glass_100_fdf5ce_1x400.png		\
diff --git a/wrap/python/ajax/css/loading.gif b/wrap/python/ajax/css/loading.gif
new file mode 100644
index 0000000000000000000000000000000000000000..e15844396f9b8c4d915f5cf595e2a22014a24426
GIT binary patch
literal 4176
zcmZ?wbhEHbRA5kG_{PBS|Nnmm28Lh1em#2h=+dQ2SFT)n_wL=FKYzY``?h1pj+~qv
z7Z(>lKfjKSj%(Mhefjd`*s)_iK0YigEOK&k4<0;t_3G8UdGnSnTlVSGr>?FpDJdy4
zGqYX0cHO&o@7AqbRaI3sHZ~d>8ag^UD^{#1D=XvU<5N;nTD59bSXkJbH*eb7+7uKN
zczAf$tXU%?BXi=!2{AD-E-o%LHMN$OmP3aQ+1c3%2?>>yluVj5X~KjF5)u+UJw4mD
zZ8I=1*t2KPlqpl3oSbglxUpo(k^=`0oH}*t%$YM$QBf)?Dt&!@b#-+`MMVt_4ICUC
z`}XZyw{BfcP0h4v(=swLva+(aY}s<>&YgsWgiV_^ZP>7(qN3v5xpPfTO%V|hMn*<Q
zjvRUN<jId8KR$f;@a)+$EiJ92q@=jGxEC*86ciLNP!A~n=k{|A33hf2a5d61U}j`s
zU{L%g<y@4SSdyBeP@Y+mp^%uBSdo*Tn4*`NmzK|<_>+Z`i-Cbb2jm7&Br>r7Z(wL@
zZfR|6@96C6?&<AiZ{yHp>TA<vF=5qgW|A>xnc5<!#be6D>o|eK(t&eflc>D5&=xg$
zQFeAd8_`x#S^iEYPK7PUq&X)r>}=8WcJt%t;1^RowpHv>JBzd`7h4C1xYBhYMfEA|
zqUSGmu(R;!T<38)^-AtwCz~?2l$joPOF~8H3kEiR-H-`49x}@ubmUM-QJC0xn1T7F
zjN#)c3QcW74Dox45)Lx8Ix>q)**$T6V5_>Y&zk~|1jn7Mdu0L*oV*>+G4Y%-JaLnQ
zd5RRb8xKpuf`cr{dIc#tDGeNg?WbilZX_fzcTVQ#4th|a)X3bE$ZuPbsK~Bg-8sW-
zS962YF%|)Pv!kj>jmLsYRT3naja2m7rS!~FoUbst@+2#|X*f4HN(T$6X1FeFTG7;W
zW{blQ289J2lT_4;k^&f;JvlX9xXZ3ASbV&PaaYd)jf;nwc9gqiNz63bdZC%c*e>El
zfx{f0WH%cQs|O1`8Bcexgshmr-#9^ei<gT!i@6Bn-95U0e7$EK<55++DK3=IuzRrs
z?#OCp7Yzx~WN+>5>*E*j)X?zO=kK4{%VgpvB_t%}Ccrdn8H1>|@PY-xo}$ZJ+4xvQ
znH=4G)+}&y+}Om<$E(2;;p^hITS#^9eg<Zh)k0Ppex8>W=&f%O747L~vXR~`ENP=*
zu)r+ZdFe_|=9wH$il<aWU88t-j9EDD1TL~Tp>p7qMVNL`g3|;g)~0-hJXX!AolTSc
zg%S)J9{AkrR_9UD@Mu_=tjxpOCcx>m;F|s976S{zO$@E9(FWYI5<&}ER`9AT9CKng
z$i&#iUzecm$TWE~pPQ3L1M36EzNNm_RUJyrE;bD8v%X9@kmSt0aJfK<p_gC-qk8C^
ztb1oV#TZU0vhX~)qVk}DfrtOqyVBE)oFeth<t(05rylH54&1~cH{}phr=Y5QXut%&
zLxLK9va%a4Eq3Wu6J5MvR)b3Mk!=a?GbS8J^-|-pa4~4ysNlGgnYD#O^TM{~NgUq$
zvW^M5o)X>5VB=x9QHe{`Ni=JwRYN0_-v*nihF1rZH=R^eaA=fB+LzoaqgWgu+q2hW
z;?FPa>`b^Ltd)Vit+T6>UDP$!k-vL#8#|vjx2c=5=#+U3BL3P!LaGkBli2wsIOg#)
zvodoq**W+u5wenJmT(cXQ0HUnmhj_>=CTphjoGm@kVQRONlltdKfZGdx2mcY52vr-
zIX!=ILDe04Tp^uoyjDBZEFHDnm*@!kNvfR_;+7E*^_s}SrpGJE6S5(p<zTy>=(Hon
z+ZG<(;Kboq(5cwS$)VoCr*VYg0ppbF9T5y43pWO^igH)EoG^3<6c;gjQu|^7hhwXn
zZd-^z2FGDhWm~759ga(;DzZp83B8Rx&?z7%vW)AHgG0vzCS6;_8B5omoF-t@<M1QI
zBXpZ1+t!c_g{6+&!P^*Y914>X0$7D!dTH)BJ&mm^wpk$J!KK{h)(!Ku3NpM_F!3q7
z>0CKt{nCMppU<jL&i9ru8*`L5zm)^SNg?@38cP)(sG2V13p6>vz_If}vyADKfEg@_
z%$mXhN!nfu8QfZwCO73Y20nUxmtCZdPpH6^OXOmgoJHrPN@E5d<wYur4p-DYy*M;j
zURs|xxI@|U-fFdw2FFfiix=DHE3m~ZkgH}EYjP}WQT2#Yz!Q_~Ozf>)-91fgEWy4a
zoxM|A`NgB99lTklOq<H?!lNoAlq4y-po=4cqlrT|X_=5}ARm*ctAHc_G-h2%aYrT&
zKcy|(SXs1qxC3=HdquURrEEQA+2xWAwn~fXN4PIj6%1bA?aIByl#_wOmy4T6OwPu1
zi;$G(s&0ML88dDrxL#=FlGU&gxUi_*E?Q0^G$3J7OQ!~lglS~JsVSY3|3qXf79Kh=
zNo}7P?}basZ7dQR7E7W_E;zQ%>|(Jvk=WA6r05v*AZ9Cv^8~%{0-ciusRz^zWZ8JO
zmM}Cm$?5qpI6lf}=+kwJl2G7Uz{Dy3%PfXLA%Ux7I?q-kA=L@~@;s~`bXp`{H0v<7
z^Pgm}a9}>#qRiDafmf)p)lSxvW$A;94D1tE_R2lU$mC*cR%{knV(_7JMY}9_RZd4y
zs!pUE`)-SwP7H^$1K7Q^R|P2a<hgY?ltyfFXjJ!hoS<^R=EVU~z2!Pfa;79Sa$Vn0
z>vDnd$tfR3%^YDSH<yN`BDx+NoSF|@nYk5NS=n0`9BTGw3z6x(@bvpzNB)QaX1D*L
zPK@mO9pMTE|8ye~@Wmvk#$%9hbaCYGn%K&36DY`KBQa?bJFA<4kU^j;d-KxS9Q@1K
z?WBd)JJ>KWaLBqk&gx|66Bl!tz^*T-Dx}I2%f!aX#S^G3+9?}hYZNH3RMg%fiCavR
z!#Ub&A$Qn>c4yP|wqnmkWyE|hNZ1>#7t%Jq(8lg^SV-D$j&KQAL!*rQyPXwA41rwS
z8cHTF0yYRR$#HubXfir^=+%jKT#yL37{JQSW9D+hG4NvJq;{5&io{m-Mn;K*Jf@im
z$A!3A1VpNK77H|qY4~IaENnQilHElo;^y|v&4NkmeNsFa6Q(m6D(LY{VOe;5Z<3o;
zN$UoOCT`J~6XimMrR!Zpw3=*GRvt{~x-ge{QBSoho2MS5Y|S2nfGJ^3S}{%y9zhEp
zFfv*R${Gl;IB{#(N3qPjIzxbo$#T(xfP{mN=PtE2B?x}xI>w|}$S?ci!y)f97BMq}
zo$6f-na;9yIu1@-Cot+Zzi-@7v`3&(S6F0)?UW?XFX5)kLexVZ9_saJVcElW?&%sn
z<t0M4Kc@X-4RCav_hmz%lQYYmrM3(cg_m*!Fz^LREIhz@_N_`oE#HiwMrPK44}qCX
zE0}J#$&^WO;K`<-$ZcZhkMHVlm(X_#7Gat&gFV*G*1?i_#svNVH6hh#7xrfMRTJ2!
zH}i`bEpua8#V(@nBD%JNEjHY71Cwi-0*{y|13QZsx1h1(zE&pAXa!HXW)8k!fxQfx
z9$SQ@og_LWc!h<y?XI+naH$FjX-A!I=g<|j<=QS3ni0^&DxS);KH|kE2SFx|AhRn6
zoEWYxWaco4@cGhkKva%Ts_oQ~R|lJWl?4?!ik=?fW^Un2Ska)M%D^bFsNm&99<|L}
zPH85Bl352Pmn{o$5NJu@;F6Sg=v8T0G;gn*I-6jC0Ats_0LMiUsZ34m+nHjQ^!X^V
zbnr<iowO^_5IKL9nO|&?%gw+g%g#D7vHg&^xQLsPNi<-YjeyGGCOL&XgPM@-0bJbD
zZ#+3BrmS<2WBJ3x5S(zmL7#QefeSi{hbEjdZ#Os*&?ea`&$FW;V8Q~=&}-bY4y5&@
zaJ4au8f4E)cyg#$bXKB^;(`|rU2PWi+0!O2be*bfrRK6@g3=TQInxO5hQ^}@C&+S5
z^7+Z-=`fkYC*t)C$IVXdTrZc1v<T^Ch%s~M3Vao3;5SKZ;Z!}q(8M)QSK>6cq|3r1
ztg;$m9)z-PS9cGSsH`S?&*UanNiH$bDLouw(oz}%lV*3$RZ`_PS<E0IBEsJzk+`9m
z#nUZdR+Fe$5SO237h8CgjYKnt2&*Vl6MHO=fu5Vo*$x&rcP_^+eq}`=AyXTUPG&7Z
z59Y4(JbG$@uB+Ra_+%Wfb+Y-X_#f+LXF22jrQr}m)Dj`BH)ah@jg1TneybEzyr#&@
zh1nJ`I9^}I?$>Z&!Uo2!Mn~o{mrNzYz*Zi;LsL7PQUkh#tvR;1q&#4^;MAK^krKL4
zW+k)!qAvoCi;fyPGnPwLF+6nVlXGU}T<{?Ih$xe~IHy2^f-7rF^Q)B+2U4A<XeVCe
zU#c-_LGo!XkE$sg%MWt&*0gB#7z8yt_VEeuUvLmySJ)vV%GdBQNQ8ljPta}JjReIA
zMV8>KBN;l5%wp^&Arc2gmM~43FI1xOlA)A?`I1nW&dj7EE}cR#Ap#pOEdJQSzlFE5
zBB`nK46B&Y35C52SlN~JybdrJDd{P)I4>%gDWJqOMNy?>f>>hW0TE4&o`?k#I1Yc1
zv|P4h*2bnUZDJe=4i4fhF30%TM3)4dW46)R5S|w#VBq1vy)@yVnDmte2Lv*7RXS?J
z3obMUcCp}VG=cJPS9cEsdpvvZBnEyKJK2eoyB+;C0z_wZyJ#rNGq>=w@%Q%6Y!Vgo
zw~=TT)#cS)(8VNc$Gnb7Q)EjMlQWMR4<|<#n^?5&kq!>O7$Ir#)t&sl)-Go{*;%;+
zRan+_NQmC*;+V$rrj?zEgNgmc?r$&o?80J2n4Dy*3|PEb6g0{z4s3tHz{bPK$e|#V
z+RDPI>hk2m)f01DW$YZ5Zn*Gx(Mb*$2_>#3*CP{kWdwMBJUH~kRZk{F%E}<+psS%h
zPe?|>p=B%rzDi~)2`=uO0#0%^JA@XtcuH`IZSpcy;_BkzdspfZl+45<$+OHOJEYNL
zI^Tl_6>|d`U0Ye@S+z7$OU_?t=3@1$xgo^L-nh4wCFI2dbHOI@z`iLB2VK3}GhNCw
zPJG}E<dSjEVVcR*cY%>TLPb6>z#+9&-72SRLx7^I08>a9=ZA-%A2G=-<qSO$@I`4d
zuX0n&gr-N%!aN*pAxC!{aR1=QVPSCLpv$3GYRX~<CL}1G>SmV>$uZcN*m=!)+ai|)
zhbCsmS!z2Y3>p?Rw5o~;6wJ*O6*%B1%y(m%OOE(ghE_%fg#bp@UR|XFtrHJiaxPbO
lIpA!=<Qj26$f4k11FJ|&28VuljKCzn78WK3Yf%3ai~-`fbCCc5

literal 0
HcmV?d00001

diff --git a/wrap/python/ajax/css/ltl2tgba.css b/wrap/python/ajax/css/ltl2tgba.css
index 471053d56..28b3038b2 100644
--- a/wrap/python/ajax/css/ltl2tgba.css
+++ b/wrap/python/ajax/css/ltl2tgba.css
@@ -119,6 +119,12 @@ table.ltltable
     color: red;
 }
 
+.ltl2tgba .loading {
+    display: block;
+    margin: 0 auto;
+    text-align: center;
+}
+
 .ltl2tgba .neverclaim, .ltl2tgba .accrun {
     font-family: monospace;
     white-space: pre;
diff --git a/wrap/python/ajax/js/jquery.ba-dotimeout.min.js b/wrap/python/ajax/js/jquery.ba-dotimeout.min.js
new file mode 100644
index 000000000..02d9349c2
--- /dev/null
+++ b/wrap/python/ajax/js/jquery.ba-dotimeout.min.js
@@ -0,0 +1,9 @@
+/*
+ * jQuery doTimeout: Like setTimeout, but better! - v1.0 - 3/3/2010
+ * http://benalman.com/projects/jquery-dotimeout-plugin/
+ * 
+ * Copyright (c) 2010 "Cowboy" Ben Alman
+ * Dual licensed under the MIT and GPL licenses.
+ * http://benalman.com/about/license/
+ */
+(function($){var a={},c="doTimeout",d=Array.prototype.slice;$[c]=function(){return b.apply(window,[0].concat(d.call(arguments)))};$.fn[c]=function(){var f=d.call(arguments),e=b.apply(this,[c+f[0]].concat(f));return typeof f[0]==="number"||typeof f[1]==="number"?this:e};function b(l){var m=this,h,k={},g=l?$.fn:$,n=arguments,i=4,f=n[1],j=n[2],p=n[3];if(typeof f!=="string"){i--;f=l=0;j=n[1];p=n[2]}if(l){h=m.eq(0);h.data(l,k=h.data(l)||{})}else{if(f){k=a[f]||(a[f]={})}}k.id&&clearTimeout(k.id);delete k.id;function e(){if(l){h.removeData(l)}else{if(f){delete a[f]}}}function o(){k.id=setTimeout(function(){k.fn()},j)}if(p){k.fn=function(q){if(typeof p==="string"){p=g[p]}p.apply(m,d.call(n,i))===true&&!q?o():e()};o()}else{if(k.fn){j===undefined?e():k.fn(j===false);return true}else{e()}}}})(jQuery);
\ No newline at end of file
diff --git a/wrap/python/ajax/ltl2tgba.html b/wrap/python/ajax/ltl2tgba.html
index 26fdbb24e..ed87a94da 100644
--- a/wrap/python/ajax/ltl2tgba.html
+++ b/wrap/python/ajax/ltl2tgba.html
@@ -12,6 +12,7 @@
     <script type="text/javascript" src="http://ajax.googleapis.com/ajax/libs/jqueryui/1.8.13/jquery-ui.min.js"></script>
     <script type="text/javascript" src="js/jquery.tipTip.minified.js"></script>
     <script type="text/javascript" src="js/jquery.ba-bbq.min.js"></script>
+    <script type="text/javascript" src="js/jquery.ba-dotimeout.min.js"></script>
     <script type="text/javascript">
     jQuery(document).ready(function(){
         $.spotvars = { autoupdate: false,
@@ -156,11 +157,13 @@
                 .addClass("ui-icon-circle-arrow-s");
             ui.siblings('[class!="dontcollapse"]').hide('fast', callback);
         }
-        function unfold(ui) {
+        function unfold(ui, noshowsiblings) {
             var icon = ui.children(".ui-icon");
             icon.removeClass("ui-icon-circle-arrow-s")
                 .addClass("ui-icon-circle-arrow-n");
-            ui.siblings('[class!="dontcollapse"]').show('fast');
+            if (!noshowsiblings) {
+              ui.siblings('[class!="dontcollapse"]').show('fast');
+            }
         }
 
         function foldToggle(ui) {
@@ -185,6 +188,14 @@
         }
 
         function updateResults() {
+            // If the answer takes more that 200ms to arrive,
+            // display a busy indicator.
+	    $.doTimeout('res-update', 200, function(){
+              $("#results-body").hide();
+              $("#results-loading").show();
+              $("#results").show();
+              unfold($("#results-head"), true);
+            })
 	    // don't read window.location.hash, because
 	    // it has been %-decoded by firefox, which
 	    // cause problems when formulae include '&'.
@@ -193,13 +204,16 @@
 		.load("/cgi-bin/spot.py",
                       fragment,
                       function(response, status, xhr) {
+			  $.doTimeout('res-update');
 			  if (status == "error") {
 			      var msg = "Sorry but there was an error: ";
 			      $("#results-body").html(msg + xhr.status + " "
 						      + xhr.statusText);
 			  }
+			  $("#results-loading").hide();
+			  $("#results-body").show();
 			  $("#results").show();
-			  unfold($("#results-head"));
+			  unfold($("#results-head"), true);
 			  fold($("#ltl-head"), function() {
 			    if ($.spotvars.scrolldown)
 			      $('html,body').animate({scrollTop: $("#results-head").offset().top}, 'slow');
@@ -610,7 +624,9 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
       </FORM>
 	  <div id="results" class="ui-widget ui-widget-content ui-corner-all collapsible shadow">
 	    <h3 id="results-head" class="ui-widget-header ui-corner-all head">Results<span class="ui-icon ui-icon-circle-arrow-n restip">Fold</span></h3>
+	    <div id="results-loading" class="dontcollapse"><img src="css/loading.gif" class="loading" border=0 alt="loading..."></div>
 	    <div id="results-body">
+	      Loading...
 	    </div>
 	  </div>
     </div>
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 3af5fe4e5..1199ebd96 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -215,7 +215,7 @@ import buddy
 def alarm_handler(signum, frame):
     unbufprint("""<p><font color="red">The script was aborted because
 it has been running for too long.</font>  Please try a shorter formula,
-or different options (not drawing automata usually helps).
+or different options.
 If you want to benchmark big formulae it is
 better to install Spot on your own computer.</p>\n""")
     finish(kill = True)