ltl2tgba.html: Separate the ltl3ba tabs from the others.

Suggested by Joachim Klein.

* wrap/python/ajax/ltl2tgba.html: Name the tab.
* wrap/python/ajax/css/ltl2tgba.css: Give it some space.

wrap/python/ajax/css/ltl2tgba.css

@@ -130,3 +130,7 @@ table.ltltable
     white-space: pre;
     font-size: 1.1em;
 }
+
+#ltl3ba-tab {
+    margin-left: 1em;
+}

wrap/python/ajax/ltl2tgba.html

@@ -571,8 +571,8 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 	      <li><a href="#tabs-tfm" class="btip" title="A tableau construction that uses BDDs to symbolically represent each state of the automaton.  Among the tree algorithms in Spot (Couvreur/FM, Couvreur/LACIM, Tauriainen/TAA) this is the best one, and the only one that has been extended to support PSL operators.">Couvreur/FM</a></li>
 	      <li><a href="#tabs-tla" class="btip" title="Builds a purely symbolic automaton, using BDDs to encode the transition relation.  The translation itself is fast (it uses a number of BDD operations that is linear in the size of the formula), but the resulting symbolic encoding is better used symbolically.  If you develop it explicitly (e.g. to draw it, as on this page) the result can easily have an exponential number of states.">Couvreur/LaCIM</a></li>
 	      <li><a href="#tabs-tta" class="btip" title="An implementation of Heikki Tauriainen's Ph.D. thesis algorithm to translate LTL formulas via very weak alternating automata with transition-based generalized acceptance conditions.">Tauriainen/TAA</a></li>
-	      <li><a href="#tabs-tl3" class="btip" title="An improved version of LTL2BA, overhauled by Tomáš Babiak during his Ph.D., and described at TACAS'12.<br>LTL3BA is not part of Spot.  Options in this tab correspond to options offered by LTL3BA, and have some overlap with the options offered by Spot that are still applied before (LTL simplifications) and after (automata simplifications) LTL3BA is called.">LTL3BA</a></li>
 	      <li><a href="#tabs-tcs" class="btip" title="Compositional suspension.<br>A technique presented at Spin'13. Suspendable formulas are formulas such as <span class='formula'>GFa</span> or <span class='formula'>FGb</span> whose verification can always be postponed by a finite number of step.  In this approach, we extract all suspendable subformulas, translate them separately from the main, skeleton automaton, only to merge them back in the accepting SCC.  This translation uses Couvreur/FM for the intermediate parts.">Comp.Susp.</a></li>
+	      <li id="ltl3ba-tab"><a href="#tabs-tl3" class="btip" title="An improved version of LTL2BA, overhauled by Tomáš Babiak during his Ph.D., and described at TACAS'12.<br>LTL3BA is not part of Spot.  Options in this tab correspond to options offered by LTL3BA, and have some overlap with the options offered by Spot that are still applied before (LTL simplifications) and after (automata simplifications) LTL3BA is called.">LTL3BA</a></li>
 	      <li class="ui-icon ui-icon-circle-arrow-n ftip">Fold</li>
 	    </ul>
 	    <input type="hidden" name="t" value="fm">