Add an UTF-8 option to the web interface.

* wrap/python/ajax/ltl2tgba.html: Add the checkbox.
* wrap/python/ajax/css/ltl2tgba.css: Add the necessary class.
* wrap/python/ajax/protocol.txt: Add the new option.
* wrap/python/ajax/spot.in: Handle it.
* wrap/python/ajax/README: Add a few lines to explain
how to run the CGI script from the command line for debugging.

wrap/python/ajax/README

@@ -21,6 +21,7 @@ to http://localhost:8000/ltl2tgba.html and you should be OK.
 After you have killed the server process (e.g. with Control-C),
 you may want to erase the spotimg/ directory.
 
+
 Installing on a real web server
 ===============================
 
@@ -50,7 +51,7 @@ Installing on a real web server
 
 3) In the directory where you have installed spot.py,
    create a subdirectory called spotimg/.  This is where
-   the script will output its images and other temporary
+   the script will cache its images and other temporary
    files.  (If you want to change this name, see the imgdir
    variable at the top of the script.)
 
@@ -58,9 +59,21 @@ Installing on a real web server
    will run the script when the HTTP server processes the
    request.
 
-   spot.py purges old files (>15min) from this directory
-   each time it runs.
+   spot.py purges old files at most once every hour.
 
 4) Copy the directories css/, js/, and logos/ along with ltl2tgba.html
    to there destination.  You may have to adjust a few paths at the
    top of the html page.
+
+
+Debugging
+=========
+
+The hash string displayed in the web browser is the query string sent
+to the CGI script, so you can simulate the call from the command line
+with a command like this:
+
+  % export QUERY_STRING="f=a+U+b&r=br&r=lf&r=si&r=eu&o=a&ff=o&mf=d&af=t&ra=t&rf=p&t=fm&fm=od&fm=sm&la=sp&ta=lc&as=ps&ec=Cou99&eo="
+  % export SCRIPT_NAME=spot.py
+  % export SERVER_SOFTWARE=SimpleHTTP
+  % ./spot.py

wrap/python/ajax/css/ltl2tgba.css

@@ -84,6 +84,10 @@ table.ltltable
     text-transform: capitalize;
 }
 
+.floatright {
+    float: right;
+}
+
 .ltl2tgba .head .ui-icon {
     float: right;
     margin: 1px 0px;

wrap/python/ajax/ltl2tgba.html

@@ -382,7 +382,11 @@ an identifier: <span class="formula">aUb</span> is an atomic proposition, unlike
 	      <label class="rtip" title="Try to reduce the formula by testing inclusion between automata built for various subformulas.  This can be rather slow on large formulas.">
 		<INPUT type="checkbox" name="r" value="lc">
 		language containment
-	      </label><br>
+	      </label>
+	      <label class="rtip floatright" title="Encode all formula using UTF-8 characters.">
+		<INPUT type="checkbox" name="g" value="8">
+		UTF-8 output
+	      </label>
 	    </div>
 	  </div>
 	  <div id="output-tabs" class="tabs collapsible shadow">

wrap/python/ajax/protocol.txt

@@ -74,3 +74,7 @@ Automaton simplifications (pick many)
   as=ps   Prune SCC
   as=wd   WDBA minimiztion
   as=ds   Direct Simulation reduction
+
+Global options
+
+  g=8     Enable UTF-8 output.

wrap/python/ajax/spot.in

@@ -135,8 +135,10 @@ os.dup2(fd, sys.stdout.fileno())
 # allowed to send strings to sys.stdout.  Always use the following
 # method instead.
 def unbufprint(s):
-    sys.stdout.write(s.encode("utf-8"))
-
+    if sys.getdefaultencoding() != 'ascii':
+        sys.stdout.write(s.encode("utf-8"))
+    else:
+        sys.stdout.write(s)
 
 def finish(kill = False):
     # Output the result and exit.
@@ -262,6 +264,8 @@ def render_dot_maybe(dotsrc, dont_run_dot):
     # This way we can cache two different requests that generate
     # the same automaton (e.g., when changing a simplification
     # option that has no influence).
+    if sys.getdefaultencoding() != 'ascii':
+        dotsrc = dotsrc.encode('utf-8')
     autprefix = (imgdir + '/' + hashlib.sha1(dotsrc).hexdigest())
     dotname = autprefix + '.txt'
     if not os.access(dotname, os.F_OK):
@@ -279,13 +283,10 @@ However you may download the <a href="''' + cgi.escape(autprefix)
     else:
         render_dot(autprefix)
 
-def render_automaton(automaton, dont_run_dot, issba, deco = False):
+def render_automaton(automaton, dont_run_dot, issba, deco = None):
     dotsrc = spot.ostringstream()
-    if not deco:
-        spot.dotty_reachable(dotsrc, automaton, issba)
-    else:
-        spot.dotty_reachable(dotsrc, automaton, issba, deco)
-    render_dot_maybe(dotsrc.str().encode('utf-8'), dont_run_dot)
+    spot.dotty_reachable(dotsrc, automaton, issba, deco)
+    render_dot_maybe(dotsrc.str(), dont_run_dot)
 
 def render_formula(f):
     dotsrc = spot.ostringstream()
@@ -318,6 +319,13 @@ def print_stats(automaton):
         return "Automaton has too much transitions per state"
     return False
 
+def format_formula(f, kind='div'):
+    if utf8:
+        s = spot.to_utf8_string(f)
+    else:
+        s = str(f)
+    return '<%s class="formula spot-format">%s</%s>' % (kind, s, kind)
+
 form = cgi.FieldStorage()
 
 output_type = form.getfirst('o', 'v');
@@ -333,6 +341,13 @@ os.setpgrp()
 signal.signal(signal.SIGALRM, alarm_handler)
 reset_alarm()
 
+# Global options
+utf8 = False
+for g in form.getlist('g'):
+    if g == '8':
+        utf8 = True
+        spot.enable_utf8()
+
 formula = form.getfirst('f', '')
 
 env = spot.default_environment.instance()
@@ -376,14 +391,18 @@ if output_type == 'f':
     formula_format = form.getfirst('ff', 'o')
     # o = Spot, i = Spin, g = GraphViz, p = properties
     if formula_format == 'o':
-        unbufprint('<div class="formula spot-format">%s</div>' % f)
+        unbufprint(format_formula(f))
     elif formula_format == 'i':
         unbufprint('<div class="formula spin-format">'
                    + spot.to_spin_string(f) + '</div>')
     elif formula_format == 'g':
         render_formula(f)
     elif formula_format == 'p':
-        unbufprint('Properties for <span class="formula spot-format">%s</span><ul>\n' % f)
+        if utf8:
+            s = spot.to_utf8_string(f)
+        else:
+            s = str(f)
+        unbufprint('Properties for ' + format_formula(f, 'span') + '<ul>\n')
         for p in spot.list_formula_props(f):
             unbufprint('<li>%s</li>\n' % p)
 
@@ -412,9 +431,9 @@ if output_type == 'f':
 translator = form.getfirst('t', 'fm')
 
 if f.is_psl_formula() and not f.is_ltl_formula() and translator != 'fm':
-    print ('''<div class="error">The PSL formula
-<span class="formula spot-format">%s</span>
-cannot be translated using this algorithm.  Please use Couveur/FM.''' % f);
+    print ('''<div class="error">The PSL formula %s
+cannot be translated using this algorithm.  Please use Couveur/FM.'''
+           % format_formula(f, 'span'));
     finish()
 
 dict = spot.bdd_dict()
@@ -513,6 +532,9 @@ if degen or neverclaim:
 else:
     degen = automaton
 
+if utf8:
+    spot.tgba_enable_utf8(automaton)
+
 # Buchi Automaton Output
 if output_type == 'a':
     if buchi_type == 'i':