From e997676c3e7d03e695025e2d2ad9bc222a1102b3 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 20 Aug 2014 21:40:51 +0200
Subject: [PATCH] Support LBT formula in ltl2tgba.html.

Suggested by Joachim Klein.

* wrap/python/ajax/spot.in: Try parse_lbt() when parse() fails.
* NEWS: Mention it.
---
 NEWS                     |  8 +++++++-
 wrap/python/ajax/spot.in | 14 ++++++++++----
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/NEWS b/NEWS
index 2c6cd84ab..a6fbca306 100644
--- a/NEWS
+++ b/NEWS
@@ -1,6 +1,12 @@
 New in spot 1.2.4a (not yet released)
 
-  * Documentation
+  * New feature:
+
+    - The online ltl2tgba translator will automatically attempt to
+      parse a formula using LBT's syntax if it cannot parse it using
+      the normal infix syntax.
+
+  * Documentation:
 
     - The man page for ltl2tgba has some new notes and references
       about TGBA and about monitors.
diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in
index 2057f9a48..c396baa5a 100755
--- a/wrap/python/ajax/spot.in
+++ b/wrap/python/ajax/spot.in
@@ -1,6 +1,6 @@
 #!@PYTHON@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2011, 2012, 2013 Laboratoire de Recherche et
+# Copyright (C) 2011, 2012, 2013, 2014 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -405,9 +405,15 @@ pel = spot.empty_parse_error_list()
 f = spot.parse(formula, pel, env)
 
 if pel:
-    unbufprint('<div class="parse-error">')
-    err = spot.format_parse_errors(spot.get_cout(), formula, pel)
-    unbufprint('</div>')
+    # Try the LBT parser in case someone is throwing LBT formulas at us.
+    pel2 = spot.empty_parse_error_list()
+    g = spot.parse_lbt(formula, pel2, env)
+    if pel2:
+        unbufprint('<div class="parse-error">')
+        err = spot.format_parse_errors(spot.get_cout(), formula, pel)
+        unbufprint('</div>')
+    else:
+        f = g
 
 # Do not continue if we could not parse anything sensible.
 if not f: