diff --git a/NEWS b/NEWS
index 7b3f7da9a..340b50566 100644
--- a/NEWS
+++ b/NEWS
@@ -102,6 +102,32 @@ New in spot 1.99.7a (not yet released)
   * The twa::transition_annotation() and
     twa::compute_support_conditions() methods have been removed.
 
+  * The interface for all functions parsing formulas (LTL, PSL, SERE,
+    etc.) has been changed to use an interface similar to the one used
+    for parsing automata.  These function now return a parsed_formula
+    object that includes both a formula and a list of syntax errors.
+
+    Typically a function written as
+
+       spot::formula read(std::string input)
+       {
+	  spot::parse_error_list pel;
+	  spot::formula f = spot::parse_infix_psl(input, pel);
+	  if (spot::format_parse_errors(std::cerr, input, pel))
+	    exit(2);
+	  return f;
+       }
+
+    should be updated to
+
+       spot::formula read(std::string input)
+       {
+	  spot::parsed_formula pf = spot::parse_infix_psl(input);
+	  if (pf.format_errors(std::cerr))
+	    exit(2);
+	  return pf.f;
+       }
+
   Python:
 
   * The ltsmin interface has been binded in Python.  It also
diff --git a/bin/common_finput.cc b/bin/common_finput.cc
index 1b328848a..adf377625 100644
--- a/bin/common_finput.cc
+++ b/bin/common_finput.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2012, 2013, 2014, 2015, 2016 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -76,14 +76,14 @@ parse_opt_finput(int key, char* arg, struct argp_state*)
   return 0;
 }
 
-spot::formula
-parse_formula(const std::string& s, spot::parse_error_list& pel)
+spot::parsed_formula
+parse_formula(const std::string& s)
 {
   if (lbt_input)
-    return spot::parse_prefix_ltl(s, pel);
+    return spot::parse_prefix_ltl(s);
   else
     return spot::parse_infix_psl
-      (s, pel, spot::default_environment::instance(), false, lenient);
+      (s, spot::default_environment::instance(), false, lenient);
 }
 
 job_processor::job_processor()
@@ -108,17 +108,16 @@ job_processor::process_string(const std::string& input,
 			      const char* filename,
 			      int linenum)
 {
-  spot::parse_error_list pel;
-  auto f = parse_formula(input, pel);
+  auto pf = parse_formula(input);
 
-  if (!f || !pel.empty())
+  if (!pf.f || !pf.errors.empty())
     {
       if (filename)
 	error_at_line(0, 0, filename, linenum, "parse error:");
-      spot::format_parse_errors(std::cerr, input, pel);
+      pf.format_errors(std::cerr);
       return 1;
     }
-  return process_formula(f, filename, linenum);
+  return process_formula(pf.f, filename, linenum);
 }
 
 int
diff --git a/bin/common_finput.hh b/bin/common_finput.hh
index 295b4b871..71a7ceb14 100644
--- a/bin/common_finput.hh
+++ b/bin/common_finput.hh
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2015, 2016 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -44,8 +44,7 @@ extern const struct argp finput_argp;
 
 int parse_opt_finput(int key, char* arg, struct argp_state* state);
 
-spot::formula
-parse_formula(const std::string& s, spot::parse_error_list& error_list);
+spot::parsed_formula parse_formula(const std::string& s);
 
 
 class job_processor
diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc
index ba7b34528..1c84e536c 100644
--- a/bin/ltlcross.cc
+++ b/bin/ltlcross.cc
@@ -837,16 +837,15 @@ namespace
 		   const char* filename,
 		   int linenum)
     {
-      spot::parse_error_list pel;
-      spot::formula f = parse_formula(input, pel);
-
-      if (!f || !pel.empty())
+      auto pf = parse_formula(input);
+      if (!pf.f || !pf.errors.empty())
 	{
 	  if (filename)
 	    error_at_line(0, 0, filename, linenum, "parse error:");
-	  spot::format_parse_errors(std::cerr, input, pel);
+	  pf.format_errors(std::cerr);
 	  return 1;
 	}
+      auto f = pf.f;
 
       int res = process_formula(f, filename, linenum);
 
diff --git a/bin/ltldo.cc b/bin/ltldo.cc
index 2bf71b0cb..3e9450170 100644
--- a/bin/ltldo.cc
+++ b/bin/ltldo.cc
@@ -237,19 +237,18 @@ namespace
 		   const char* filename,
 		   int linenum)
     {
-      spot::parse_error_list pel;
-      spot::formula f = parse_formula(input, pel);
+      spot::parsed_formula pf = parse_formula(input);
 
-      if (!f || !pel.empty())
+      if (!pf.f || !pf.errors.empty())
 	{
 	  if (filename)
 	    error_at_line(0, 0, filename, linenum, "parse error:");
-	  spot::format_parse_errors(std::cerr, input, pel);
+	  pf.format_errors(std::cerr);
 	  return 1;
 	}
 
       inputf = input;
-      process_formula(f, filename, linenum);
+      process_formula(pf.f, filename, linenum);
       return 0;
     }
 
diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc
index 5f6098da5..218ffdfa2 100644
--- a/bin/ltlfilt.cc
+++ b/bin/ltlfilt.cc
@@ -288,11 +288,10 @@ static std::string unabbreviate;
 static spot::formula
 parse_formula_arg(const std::string& input)
 {
-  spot::parse_error_list pel;
-  spot::formula f = parse_formula(input, pel);
-  if (spot::format_parse_errors(std::cerr, input, pel))
+  spot::parsed_formula pf = parse_formula(input);
+  if (pf.format_errors(std::cerr))
     error(2, 0, "parse error when parsing an argument");
-  return f;
+  return pf.f;
 }
 
 static int
@@ -482,20 +481,19 @@ namespace
     process_string(const std::string& input,
 		    const char* filename = nullptr, int linenum = 0)
     {
-      spot::parse_error_list pel;
-      spot::formula f = parse_formula(input, pel);
+      spot::parsed_formula pf = parse_formula(input);
 
-      if (!f || pel.size() > 0)
+      if (!pf.f || !pf.errors.empty())
 	  {
 	    if (!ignore_errors)
 	      {
 		if (filename)
 		  error_at_line(0, 0, filename, linenum, "parse error:");
-		spot::format_parse_errors(std::cerr, input, pel);
+		pf.format_errors(std::cerr);
 	      }
 
 	    if (error_style == skip_errors)
-	      std::cout << input << std::endl;
+	      std::cout << input << '\n';
 	    else
 	      assert(error_style == drop_errors);
 	    check_cout();
@@ -503,7 +501,7 @@ namespace
 	  }
       try
 	{
-	  return process_formula(f, filename, linenum);
+	  return process_formula(pf.f, filename, linenum);
 	}
       catch (const std::runtime_error& e)
 	{
diff --git a/doc/org/tut01.org b/doc/org/tut01.org
index e5363a6b6..9fdfda015 100644
--- a/doc/org/tut01.org
+++ b/doc/org/tut01.org
@@ -119,11 +119,10 @@ Here is how to call the infix parser explicitly:
   int main()
   {
     std::string input = "[]<>p0 || <>[]p1";
-    spot::parse_error_list pel;
-    spot::formula f = spot::parse_infix_psl(input, pel);
-    if (spot::format_parse_errors(std::cerr, input, pel))
+    spot::parsed_formula pf = spot::parse_infix_psl(input);
+    if (pf.format_errors(std::cerr))
       return 1;
-    std::cout << f << '\n';
+    std::cout << pf.f << '\n';
     return 0;
   }
 #+END_SRC
@@ -131,26 +130,27 @@ Here is how to call the infix parser explicitly:
 #+RESULTS:
 : GFp0 | FGp1
 
-So =parse_infix_psl()= processes =input=, and stores any diagnostic in
-=pel=, which is a list of pairs associating each error to a location.
-You could iterate over that list to print it by yourself as you wish,
-or you can call =format_parse_errors()= to do that for you.  Note that
-as its name implies, this parser can read more than LTL formulas (the
-fragment of PSL we support is basically LTL extended with regular
-expressions).
+Note that as its name implies, this parser can read more than LTL
+formulas: the fragment of PSL we support is basically LTL extended
+with regular expressions.
 
-If =pel= is empty, =format_parse_errors()= will do nothing and return
-false.
+The =parse_infix_psl()= function processes =input=, and returns a
+=spot::parsed_formula= object.  In addition to the =spot::formula= we
+desire (stored as the =spot::parsed_formula::f= attribute), the
+=spot::parsed_formula= also stores any diagnostic collected during the
+parsing.  Those diagnostics are stored in the
+=spot::parsed_formula::errors= attribute, but they can conveniently be
+printed by calling the =spot::parsed::format_errors()= method: this
+method returns true if and only if a diagnostic was output, so this is
+usually used to abort the program with an error status as above.
 
-If =pel= is non empty, =format_parse_errors()= will display the errors
-messages and return true.  In the above code, we have decided to
-aborts the execution in this case.
 
-However the parser usually tries to do some error recovery.  For
-instance if you have input =(a U b))= the parser will complain about
-the extra parenthesis (=pel= not empty), but it will still return an
-=f= that is equivalent to =a U b=.  So you could decide to continue
-with the "fixed" formula if you wish.  Here is an example:
+The parser usually tries to do some error recovery, so the =f=
+attribute can be non-null even if some parsing errors where returned.
+For instance if you have input =(a U b))= the parser will complain
+about the extra parenthesis, but it will still return a formula that
+is equivalent to =a U b=.  So you could decide to continue with the
+"fixed" formula if you wish.  Here is an example:
 
 #+BEGIN_SRC C++ :results verbatim :exports both
   #include <string>
@@ -161,14 +161,13 @@ with the "fixed" formula if you wish.  Here is an example:
   int main()
   {
     std::string input = "(a U b))";
-    spot::parse_error_list pel;
-    spot::formula f = spot::parse_infix_psl(input, pel);
+    spot::parsed_formula pf = spot::parse_infix_psl(input);
     // Use std::cout instead of std::cerr because we can only
     // show the output of std::cout in this documentation.
-    (void) spot::format_parse_errors(std::cout, input, pel);
-    if (f == nullptr)
+    (void) pf.format_errors(std::cout);
+    if (pf.f == nullptr)
       return 1;
-    std::cout << "Parsed formula: " << f << '\n';
+    std::cout << "Parsed formula: " << pf.f << '\n';
     return 0;
   }
 #+END_SRC
@@ -185,8 +184,8 @@ with the "fixed" formula if you wish.  Here is an example:
 : Parsed formula: a U b
 
 
-The formula =f= is only returned as null when the parser really cannot
-recover anything.
+The formula =pf.f= would only be returned as null when the parser
+really cannot recover anything.
 
 ** Calling the prefix parser explicitly
 
@@ -202,10 +201,10 @@ of =parse_infix_psl()=.
   int main()
   {
     std::string input = "& & G p0 p1 p2";
-    spot::parse_error_list pel;
-    spot::formula f = spot::parse_prefix_ltl(input, pel);
-    if (spot::format_parse_errors(std::cerr, input, pel))
+    spot::parsed_formula pf = spot::parse_prefix_ltl(input);
+    if (pf.format_errors(std::cerr))
       return 1;
+    spot::formula f = pf.f;
     print_latex_psl(std::cout, f) << '\n';
     print_lbt_ltl(std::cout, f) << '\n';
     print_spin_ltl(std::cout, f, true) << '\n';
@@ -246,11 +245,10 @@ For instance, let's see what happens if a PSL formulas is passed to
   int main()
   {
     std::string input = "{a*;b}<>->(a U (b & GF c))";
-    spot::parse_error_list pel;
-    spot::formula f = spot::parse_infix_psl(input, pel);
-    if (spot::format_parse_errors(std::cerr, input, pel))
+    spot::parsed_formula pf = spot::parse_infix_psl(input);
+    if (pf.format_errors(std::cerr))
       return 1;
-    print_spin_ltl(std::cout, f) << '\n';
+    print_spin_ltl(std::cout, pf.f) << '\n';
     return 0;
   }
 #+END_SRC
@@ -276,10 +274,10 @@ The first is to simply diagnose non-LTL formulas.
   int main()
   {
     std::string input = "{a*;b}<>->(a U (b & GF c))";
-    spot::parse_error_list pel;
-    spot::formula f = spot::parse_infix_psl(input, pel);
-    if (spot::format_parse_errors(std::cerr, input, pel))
+    spot::parsed_formula pf = spot::parse_infix_psl(input);
+    if (pf.format_errors(std::cerr))
       return 1;
+    spot::formula f = pf.f;
     if (!f.is_ltl_formula())
       {
         std::cerr << "Only LTL formulas are supported.\n";
@@ -306,10 +304,10 @@ prepared to reject the formula any way.  In our example, we are lucky
   int main()
   {
     std::string input = "{a*;b}<>->(a U (b & GF c))";
-    spot::parse_error_list pel;
-    spot::formula f = spot::parse_infix_psl(input, pel);
-    if (spot::format_parse_errors(std::cerr, input, pel))
+    spot::parsed_formula pf = spot::parse_infix_psl(input);
+    if (pf.format_errors(std::cerr))
       return 1;
+    spot::formula f = pf.f;
     if (!f.is_ltl_formula())
       {
         spot::tl_simplifier simp;
diff --git a/doc/org/tut02.org b/doc/org/tut02.org
index a75dd988b..d9e307a51 100644
--- a/doc/org/tut02.org
+++ b/doc/org/tut02.org
@@ -85,10 +85,10 @@ destructor.
   int main()
   {
     std::string input = "\"Proc@Here\" U (\"var > 10\" | \"var < 4\")";
-    spot::parse_error_list pel;
-    spot::formula f = spot::parse_infix_psl(input, pel);
-    if (spot::format_parse_errors(std::cerr, input, pel))
+    spot::parsed_formula pf = spot::parse_infix_psl(input);
+    if (pf.format_errors(std::cerr))
       return 1;
+    spot::formula f = pf.f;
     spot::relabeling_map m;
     f = spot::relabel(f, spot::Pnn, &m);
     for (auto& i: m)
diff --git a/doc/org/tut10.org b/doc/org/tut10.org
index 34701ffb1..b25f55bff 100644
--- a/doc/org/tut10.org
+++ b/doc/org/tut10.org
@@ -137,13 +137,12 @@ never claim is done via the =print_never_claim= function.
   int main()
   {
     std::string input = "[]<>p0 || <>[]p1";
-    spot::parse_error_list pel;
-    spot::formula f = spot::parse_infix_psl(input, pel);
-    if (spot::format_parse_errors(std::cerr, input, pel))
+    spot::parsed_formula pf = spot::parse_infix_psl(input);
+    if (pf.format_errors(std::cerr))
       return 1;
     spot::translator trans;
     trans.set_type(spot::postprocessor::BA);
-    spot::twa_graph_ptr aut = trans.run(f);
+    spot::twa_graph_ptr aut = trans.run(pf.f);
     print_never_claim(std::cout, aut) << '\n';
     return 0;
   }
@@ -154,23 +153,23 @@ never claim is done via the =print_never_claim= function.
 never {
 T0_init:
   if
-  :: ((p1)) -> goto accept_S0
-  :: ((true)) -> goto T0_init
-  :: ((p0)) -> goto accept_S2
+  :: (p1) -> goto accept_S0
+  :: (true) -> goto T0_init
+  :: (p0) -> goto accept_S2
   fi;
 accept_S0:
   if
-  :: ((p1)) -> goto accept_S0
+  :: (p1) -> goto accept_S0
   fi;
 accept_S2:
   if
-  :: ((p0)) -> goto accept_S2
-  :: ((!(p0))) -> goto T0_S3
+  :: (p0) -> goto accept_S2
+  :: (!(p0)) -> goto T0_S3
   fi;
 T0_S3:
   if
-  :: ((p0)) -> goto accept_S2
-  :: ((!(p0))) -> goto T0_S3
+  :: (p0) -> goto accept_S2
+  :: (!(p0)) -> goto T0_S3
   fi;
 }
 #+end_example
diff --git a/doc/org/tut20.org b/doc/org/tut20.org
index 1bd63c058..f138f5419 100644
--- a/doc/org/tut20.org
+++ b/doc/org/tut20.org
@@ -122,7 +122,7 @@ State: 4
 
 * C++
 
-Parsing an automaton is almost similar to [[file:tut01.org][parsing an LTL formula]].  The
+Parsing an automaton is similar to [[file:tut01.org][parsing an LTL formula]].  The
 =parse_aut()= function takes a filename and a BDD dictionary (to be
 discussed later on this page).  It returns a shared pointer to a
 structure that has a couple of important fields: =aborted= is a
diff --git a/python/ajax/spotcgi.in b/python/ajax/spotcgi.in
index 0d950f506..935687e91 100755
--- a/python/ajax/spotcgi.in
+++ b/python/ajax/spotcgi.in
@@ -435,19 +435,18 @@ for g in form.getlist('g'):
 formula = form.getfirst('f', '')
 
 env = spot.default_environment.instance()
-pel = spot.empty_parse_error_list()
-f = spot.parse_infix_psl(formula, pel, env)
+pf = spot.parse_infix_psl(formula, env)
 
-if pel:
+if pf.errors:
     # Try the LBT parser in case someone is throwing LBT formulas at us.
-    pel2 = spot.empty_parse_error_list()
-    g = spot.parse_prefix_ltl(formula, pel2, env)
-    if pel2:
+    pg = spot.parse_prefix_ltl(formula, env)
+    if pg.errors:
         unbufprint('<div class="parse-error">')
-        err = spot.format_parse_errors(spot.get_cout(), formula, pel)
+        err = pf.format_errors(spot.get_cout())
         unbufprint('</div>')
+        f = pf.f
     else:
-        f = g
+        f = pg.f
 
 # Do not continue if we could not parse anything sensible.
 if not f:
diff --git a/python/spot/impl.i b/python/spot/impl.i
index b58d9ce81..43bf8966e 100644
--- a/python/spot/impl.i
+++ b/python/spot/impl.i
@@ -692,20 +692,6 @@ bool fnode_instances_check()
   return spot::fnode::instances_check();
 }
 
-spot::parse_error_list
-empty_parse_error_list()
-{
-  parse_error_list l;
-  return l;
-}
-
-spot::parse_aut_error_list
-empty_parse_aut_error_list()
-{
-  parse_aut_error_list l;
-  return l;
-}
-
 spot::twa_graph_ptr
 ensure_digraph(const spot::twa_ptr& a)
 {
diff --git a/spot/parseaut/parseaut.yy b/spot/parseaut/parseaut.yy
index 36ed1be40..3f35edb44 100644
--- a/spot/parseaut/parseaut.yy
+++ b/spot/parseaut/parseaut.yy
@@ -1633,10 +1633,9 @@ nc-formula: nc-formula-or-ident
        auto i = res.fcache.find(*$1);
        if (i == res.fcache.end())
 	 {
-	   spot::parse_error_list pel;
-	   auto f = spot::parse_infix_boolean(*$1, pel, *res.env,
-						   debug_level(), true);
-	   for (auto& j: pel)
+	   auto pf = spot::parse_infix_boolean(*$1, *res.env, debug_level(),
+					       true);
+	   for (auto& j: pf.errors)
 	     {
 	       // Adjust the diagnostic to the current position.
 	       spot::location here = @1;
@@ -1647,8 +1646,9 @@ nc-formula: nc-formula-or-ident
 	       res.h->errors.emplace_back(here, j.second);
 	     }
            bdd cond = bddfalse;
-	   if (f)
-	     cond = spot::formula_to_bdd(f, res.h->aut->get_dict(), res.h->aut);
+	   if (pf.f)
+	     cond = spot::formula_to_bdd(pf.f,
+					 res.h->aut->get_dict(), res.h->aut);
 	   $$ = (res.fcache[*$1] = cond).id();
 	 }
        else
@@ -1814,16 +1814,15 @@ lbtt-acc:               { $$ = 0U; }
 	}
 lbtt-guard: STRING
           {
-	    spot::parse_error_list pel;
-	    auto f = spot::parse_prefix_ltl(*$1, pel, *res.env);
-	    if (!f || !pel.empty())
+	    auto pf = spot::parse_prefix_ltl(*$1, *res.env);
+	    if (!pf.f || !pf.errors.empty())
 	      {
 		std::string s = "failed to parse guard: ";
 		s += *$1;
 		error(@$, s);
 	      }
-	    if (!pel.empty())
-	      for (auto& j: pel)
+	    if (!pf.errors.empty())
+	      for (auto& j: pf.errors)
 		{
 		  // Adjust the diagnostic to the current position.
 		  spot::location here = @1;
@@ -1833,13 +1832,13 @@ lbtt-guard: STRING
 		  here.begin.column += j.first.begin.column - 1;
 		  res.h->errors.emplace_back(here, j.second);
 		}
-	    if (!f)
+	    if (!pf.f)
 	      {
 		res.cur_label = bddtrue;
 	      }
 	    else
 	      {
-		if (!f.is_boolean())
+		if (!pf.f.is_boolean())
 		  {
 		    error(@$,
 			  "non-Boolean transition label (replaced by true)");
@@ -1848,7 +1847,7 @@ lbtt-guard: STRING
 		else
 		  {
 		    res.cur_label =
-		      formula_to_bdd(f, res.h->aut->get_dict(), res.h->aut);
+		      formula_to_bdd(pf.f, res.h->aut->get_dict(), res.h->aut);
 		  }
 	      }
 	    delete $1;
diff --git a/spot/parsetl/fmterror.cc b/spot/parsetl/fmterror.cc
index 470403c56..61df55125 100644
--- a/spot/parsetl/fmterror.cc
+++ b/spot/parsetl/fmterror.cc
@@ -72,11 +72,10 @@ namespace spot
 			    const parse_error_list& error_list)
     {
       bool printed = false;
-      parse_error_list::const_iterator it;
-      for (it = error_list.begin(); it != error_list.end(); ++it)
+      for (auto it: error_list)
 	{
-	  os << ">>> " << ltl_string << std::endl;
-	  const location& l = it->first;
+	  os << ">>> " << ltl_string << '\n';
+	  const location& l = it.first;
 
 	  unsigned n = 1;
 	  for (; n < 4 + l.begin.column; ++n)
@@ -86,7 +85,7 @@ namespace spot
 	  ++n;
 	  for (; n < 4 + l.end.column; ++n)
 	    os << '^';
-	  os << std::endl << it->second << std::endl << std::endl;
+	  os << '\n' << it.second << "\n\n";
 	  printed = true;
 	}
       return printed;
@@ -94,19 +93,17 @@ namespace spot
   }
 
   bool
-  format_parse_errors(std::ostream& os,
-		      const std::string& ltl_string,
-		      const parse_error_list& error_list)
+  parsed_formula::format_errors(std::ostream& os)
   {
-    if (utf8::is_valid(ltl_string.begin(), ltl_string.end()))
+    if (utf8::is_valid(input.begin(), input.end()))
       {
-	parse_error_list fixed = error_list;
-	fix_utf8_locations(ltl_string, fixed);
-	return format_parse_errors_aux(os, ltl_string, fixed);
+	parse_error_list fixed = errors;
+	fix_utf8_locations(input, fixed);
+	return format_parse_errors_aux(os, input, fixed);
       }
     else
       {
-	return format_parse_errors_aux(os, ltl_string, error_list);
+	return format_parse_errors_aux(os, input, errors);
       }
   }
 }
diff --git a/spot/parsetl/parsetl.yy b/spot/parsetl/parsetl.yy
index 7ff2bbb45..d4070e908 100644
--- a/spot/parsetl/parsetl.yy
+++ b/spot/parsetl/parsetl.yy
@@ -1,5 +1,5 @@
 /* -*- coding: utf-8 -*-
-** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
+** Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
 ** de Recherche et Développement de l'Epita (LRDE).
 ** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -120,25 +120,24 @@ using namespace spot;
 	  return nullptr;
 	}
 
-      spot::parse_error_list suberror;
-      formula f;
+      spot::parsed_formula pf;
       switch (type)
 	{
 	case parser_sere:
-	  f = spot::parse_infix_sere(str, suberror, env, debug, true);
+	  pf = spot::parse_infix_sere(str, env, debug, true);
 	  break;
 	case parser_bool:
-	  f = spot::parse_infix_boolean(str, suberror, env, debug, true);
+	  pf = spot::parse_infix_boolean(str, env, debug, true);
 	  break;
 	case parser_ltl:
-	  f = spot::parse_infix_psl(str, suberror, env, debug, true);
+	  pf = spot::parse_infix_psl(str, env, debug, true);
 	  break;
 	}
 
-      if (suberror.empty())
-	return f;
+      if (pf.errors.empty())
+	return pf.f;
 
-      f = env.require(str);
+      auto f = env.require(str);
       if (!f)
 	{
 	  std::string s = "atomic proposition `";
@@ -993,69 +992,65 @@ tlyy::parser::error(const location_type& location, const std::string& message)
 
 namespace spot
 {
-  formula
+  parsed_formula
   parse_infix_psl(const std::string& ltl_string,
-		  parse_error_list& error_list,
 		  environment& env,
 		  bool debug, bool lenient)
   {
-    formula result = nullptr;
+    parsed_formula result(ltl_string);
     flex_set_buffer(ltl_string,
 		    tlyy::parser::token::START_LTL,
 		    lenient);
-    tlyy::parser parser(error_list, env, result);
+    tlyy::parser parser(result.errors, env, result.f);
     parser.set_debug_level(debug);
     parser.parse();
     flex_unset_buffer();
     return result;
   }
 
-  formula
+  parsed_formula
   parse_infix_boolean(const std::string& ltl_string,
-		      parse_error_list& error_list,
 		      environment& env,
 		      bool debug, bool lenient)
   {
-    formula result = nullptr;
+    parsed_formula result(ltl_string);
     flex_set_buffer(ltl_string,
 		    tlyy::parser::token::START_BOOL,
 		    lenient);
-    tlyy::parser parser(error_list, env, result);
+    tlyy::parser parser(result.errors, env, result.f);
     parser.set_debug_level(debug);
     parser.parse();
     flex_unset_buffer();
     return result;
   }
 
-  formula
+  parsed_formula
   parse_prefix_ltl(const std::string& ltl_string,
-		   parse_error_list& error_list,
 		   environment& env,
 		   bool debug)
   {
-    formula result = nullptr;
+    parsed_formula result(ltl_string);
     flex_set_buffer(ltl_string,
 		    tlyy::parser::token::START_LBT,
 		    false);
-    tlyy::parser parser(error_list, env, result);
+    tlyy::parser parser(result.errors, env, result.f);
     parser.set_debug_level(debug);
     parser.parse();
     flex_unset_buffer();
     return result;
   }
 
-  formula
+  parsed_formula
   parse_infix_sere(const std::string& sere_string,
-		   parse_error_list& error_list,
 		   environment& env,
 		   bool debug,
 		   bool lenient)
   {
-    formula result = nullptr;
+    parsed_formula result(sere_string);
     flex_set_buffer(sere_string,
 		    tlyy::parser::token::START_SERE,
 		    lenient);
-    tlyy::parser parser(error_list, env, result);
+    tlyy::parser parser(result.errors, env, result.f);
     parser.set_debug_level(debug);
     parser.parse();
     flex_unset_buffer();
@@ -1065,19 +1060,17 @@ namespace spot
   formula
   parse_formula(const std::string& ltl_string, environment& env)
   {
-    parse_error_list pel;
-    formula f = parse_infix_psl(ltl_string, pel, env);
+    parsed_formula pf = parse_infix_psl(ltl_string, env);
     std::ostringstream s;
-    if (format_parse_errors(s, ltl_string, pel))
+    if (pf.format_errors(s))
       {
-	parse_error_list pel2;
-	formula g = parse_prefix_ltl(ltl_string, pel2, env);
-	if (pel2.empty())
-	  return g;
+	parsed_formula pg = parse_prefix_ltl(ltl_string, env);
+	if (pg.errors.empty())
+	  return pg.f;
 	else
 	  throw parse_error(s.str());
       }
-    return f;
+    return pf.f;
   }
 }
 
diff --git a/spot/tl/parse.hh b/spot/tl/parse.hh
index e5029e546..b1bb4601e 100644
--- a/spot/tl/parse.hh
+++ b/spot/tl/parse.hh
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
+// de Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -45,10 +45,40 @@ namespace spot
   struct parse_error_list {};
 #endif
 
+  /// \brief The result of a formula parser.
+  struct SPOT_API parsed_formula final
+  {
+    /// \brief The parsed formula.
+    ///
+    /// This could be formula(nullptr) in case of a serious parse error.
+    formula f = nullptr;
+
+    /// The input text, before parsing.
+    std::string input;
+
+    /// \brief Syntax errors that occurred during parsing.
+    ///
+    /// Note that the parser does not print any diagnostic.
+    /// Deciding how to output those errors is up to you.
+    ///
+    /// \see format_errors
+    parse_error_list errors;
+
+    parsed_formula(const std::string& str = "")
+      : input(str)
+    {
+    }
+
+    /// \brief Format diagnostics.
+    ///
+    /// \param os Where diagnostics should be output.
+    /// \return \c true iff any diagnostic was output.
+    bool format_errors(std::ostream& os);
+  };
+
+
   /// \brief Build a formula from an LTL string.
   /// \param ltl_string The string to parse.
-  /// \param error_list A list that will be filled with
-  ///        parse errors that occured during parsing.
   /// \param env The environment into which parsing should take place.
   /// \param debug When true, causes the parser to trace its execution.
   /// \param lenient When true, parenthesized blocks that cannot be
@@ -57,59 +87,56 @@ namespace spot
   /// \return A formula built from \a ltl_string, or
   ///         formula(nullptr) if the input was unparsable.
   ///
-  /// Note that the parser usually tries to recover from errors.  It can
-  /// return a non zero value even if it encountered error during the
-  /// parsing of \a ltl_string.  If you want to make sure \a ltl_string
-  /// was parsed succesfully, check \a error_list for emptiness.
+  ///
+  /// Note that the parser usually tries to recover from errors.  The
+  /// field parsed_formula::f in the returned object can be a non-zero
+  /// value even if it encountered error during the parsing of \a
+  /// ltl_string.  If you want to make sure \a ltl_string was parsed
+  /// succesfully, check \a parsed_formula::errors for emptiness.
   ///
   /// \warning This function is not reentrant.
   SPOT_API
-  formula parse_infix_psl(const std::string& ltl_string,
-			  parse_error_list& error_list,
-			  environment& env =
-			  default_environment::instance(),
-			  bool debug = false,
-			  bool lenient = false);
+  parsed_formula parse_infix_psl(const std::string& ltl_string,
+				 environment& env =
+				 default_environment::instance(),
+				 bool debug = false,
+				 bool lenient = false);
 
   /// \brief Build a Boolean formula from a string.
   /// \param ltl_string The string to parse.
-  /// \param error_list A list that will be filled with
-  ///        parse errors that occured during parsing.
   /// \param env The environment into which parsing should take place.
   /// \param debug When true, causes the parser to trace its execution.
   /// \param lenient When true, parenthesized blocks that cannot be
   ///                parsed as subformulas will be considered as
   ///                atomic propositions.
-  /// \return A formula built from \a ltl_string, or
-  ///         formula(nullptr) if the input was unparsable.
+  /// \return A parsed_formula
   ///
-  /// Note that the parser usually tries to recover from errors.  It can
-  /// return a non zero value even if it encountered error during the
-  /// parsing of \a ltl_string.  If you want to make sure \a ltl_string
-  /// was parsed succesfully, check \a error_list for emptiness.
+  /// Note that the parser usually tries to recover from errors.  The
+  /// field parsed_formula::f in the returned object can be a non-zero
+  /// value even if it encountered error during the parsing of \a
+  /// ltl_string.  If you want to make sure \a ltl_string was parsed
+  /// succesfully, check \a parsed_formula::errors for emptiness.
   ///
   /// \warning This function is not reentrant.
   SPOT_API
-  formula parse_infix_boolean(const std::string& ltl_string,
-			      parse_error_list& error_list,
-			      environment& env =
-			      default_environment::instance(),
-			      bool debug = false,
-			      bool lenient = false);
+  parsed_formula parse_infix_boolean(const std::string& ltl_string,
+				     environment& env =
+				     default_environment::instance(),
+				     bool debug = false,
+				     bool lenient = false);
 
   /// \brief Build a formula from an LTL string in LBT's format.
   /// \param ltl_string The string to parse.
-  /// \param error_list A list that will be filled with
-  ///        parse errors that occured during parsing.
   /// \param env The environment into which parsing should take place.
   /// \param debug When true, causes the parser to trace its execution.
   /// \return A formula built from \a ltl_string, or
   ///         formula(nullptr) if the input was unparsable.
   ///
-  /// Note that the parser usually tries to recover from errors.  It can
-  /// return an non zero value even if it encountered error during the
-  /// parsing of \a ltl_string.  If you want to make sure \a ltl_string
-  /// was parsed succesfully, check \a error_list for emptiness.
+  /// Note that the parser usually tries to recover from errors.  The
+  /// field parsed_formula::f in the returned object can be a non-zero
+  /// value even if it encountered error during the parsing of \a
+  /// ltl_string.  If you want to make sure \a ltl_string was parsed
+  /// succesfully, check \a parsed_formula::errors for emptiness.
   ///
   /// The LBT syntax, also used by the lbtt and scheck tools, is
   /// extended to support W, and M operators (as done in lbtt), and
@@ -117,11 +144,10 @@ namespace spot
   ///
   /// \warning This function is not reentrant.
   SPOT_API
-  formula parse_prefix_ltl(const std::string& ltl_string,
-			   parse_error_list& error_list,
-			   environment& env =
-			   default_environment::instance(),
-			   bool debug = false);
+  parsed_formula parse_prefix_ltl(const std::string& ltl_string,
+				  environment& env =
+				  default_environment::instance(),
+				  bool debug = false);
 
   /// \brief A simple wrapper to parse_infix_psl() and parse_prefix_ltl().
   ///
@@ -135,8 +161,6 @@ namespace spot
 
   /// \brief Build a formula from a string representing a SERE.
   /// \param sere_string The string to parse.
-  /// \param error_list A list that will be filled with
-  ///        parse errors that occured during parsing.
   /// \param env The environment into which parsing should take place.
   /// \param debug When true, causes the parser to trace its execution.
   /// \param lenient When true, parenthesized blocks that cannot be
@@ -145,37 +169,19 @@ namespace spot
   /// \return A formula built from \a sere_string, or
   ///         formula(0) if the input was unparsable.
   ///
-  /// Note that the parser usually tries to recover from errors.  It can
-  /// return an non zero value even if it encountered error during the
-  /// parsing of \a ltl_string.  If you want to make sure \a ltl_string
-  /// was parsed succesfully, check \a error_list for emptiness.
+  /// Note that the parser usually tries to recover from errors.  The
+  /// field parsed_formula::f in the returned object can be a non-zero
+  /// value even if it encountered error during the parsing of \a
+  /// ltl_string.  If you want to make sure \a ltl_string was parsed
+  /// succesfully, check \a parsed_formula::errors for emptiness.
   ///
   /// \warning This function is not reentrant.
   SPOT_API
-  formula parse_infix_sere(const std::string& sere_string,
-			   parse_error_list& error_list,
-			   environment& env =
-			   default_environment::instance(),
-			   bool debug = false,
-			   bool lenient = false);
-
-  /// \brief Format diagnostics produced by spot::parse
-  ///        or spot::ratexp
-  ///
-  /// If the string is utf8 encoded, spot::fix_utf8_locations()
-  /// will be used to report correct utf8 locations (assuming the
-  /// output is utf8 aware).  Nonetheless, the supplied \a
-  /// error_list will not be modified.
-  ///
-  /// \param os Where diagnostics should be output.
-  /// \param input_string The string that were parsed.
-  /// \param error_list The error list filled by spot::parse
-  ///        or spot::parse_sere while parsing \a input_string.
-  /// \return \c true iff any diagnostic was output.
-  SPOT_API
-  bool format_parse_errors(std::ostream& os,
-			   const std::string& input_string,
-			   const parse_error_list& error_list);
+  parsed_formula parse_infix_sere(const std::string& sere_string,
+				  environment& env =
+				  default_environment::instance(),
+				  bool debug = false,
+				  bool lenient = false);
 
   /// \brief Fix location of diagnostics assuming the input is utf8.
   ///
diff --git a/tests/core/checkpsl.cc b/tests/core/checkpsl.cc
index 3dde7e3b5..cd5069f4f 100644
--- a/tests/core/checkpsl.cc
+++ b/tests/core/checkpsl.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -60,11 +60,10 @@ main(int argc, char** argv)
       if (s.empty() || s[0] == '#') // Skip comments
 	continue;
 
-      spot::parse_error_list pe;
-      auto fpos = spot::parse_infix_psl(s, pe);
-
-      if (spot::format_parse_errors(std::cerr, s, pe))
+      auto pfpos = spot::parse_infix_psl(s);
+      if (pfpos.format_errors(std::cerr))
 	return 2;
+      auto fpos = pfpos.f;
 
       auto fneg = spot::formula::Not(fpos);
 
diff --git a/tests/core/checkta.cc b/tests/core/checkta.cc
index a5fdb97b7..88f594d15 100644
--- a/tests/core/checkta.cc
+++ b/tests/core/checkta.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement
-// de l'Epita (LRDE).
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -85,11 +85,11 @@ main(int argc, char** argv)
       if (s.empty() || s[0] == '#') // Skip comments
 	continue;
 
-      spot::parse_error_list pe;
-      auto f = spot::parse_infix_psl(s, pe);
+      auto pf = spot::parse_infix_psl(s);
 
-      if (spot::format_parse_errors(std::cerr, s, pe))
+      if (pf.format_errors(std::cerr))
 	return 2;
+      auto f = pf.f;
 
 
       {
diff --git a/tests/core/consterm.cc b/tests/core/consterm.cc
index d11289327..a54ca633b 100644
--- a/tests/core/consterm.cc
+++ b/tests/core/consterm.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2011, 2012, 2015 Laboratoire de Recherche et
-// Dévelopement de l'Epita (LRDE).
+// Copyright (C) 2010, 2011, 2012, 2015, 2016 Laboratoire de Recherche
+// et Dévelopement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -58,12 +58,11 @@ main(int argc, char **argv)
       std::getline(ss, form, ',');
       ss >> expected;
 
-      spot::parse_error_list p1;
-      auto f1 = spot::parse_infix_sere(form, p1);
-      if (spot::format_parse_errors(std::cerr, form, p1))
+      auto pf1 = spot::parse_infix_sere(form);
+      if (pf1.format_errors(std::cerr))
 	return 2;
 
-      bool b = f1.accepts_eword();
+      bool b = pf1.f.accepts_eword();
       std::cout << form << ',' << b << '\n';
       if (b != expected)
 	{
diff --git a/tests/core/emptchk.cc b/tests/core/emptchk.cc
index 75cde5a27..de57168a8 100644
--- a/tests/core/emptchk.cc
+++ b/tests/core/emptchk.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement de
-// l'Epita (LRDE).
+// Copyright (C) 2014, 2015, 2016 Laboratoire de Recherche et
+// Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -89,10 +89,10 @@ main(int argc, char** argv)
 
       int runs = atoi(tokens[0].c_str());
 
-      spot::parse_error_list pe;
-      auto f = spot::parse_infix_psl(tokens[1], pe);
-      if (spot::format_parse_errors(std::cerr, tokens[1], pe))
+      auto pf = spot::parse_infix_psl(tokens[1]);
+      if (pf.format_errors(std::cerr))
 	return 2;
+      auto f = pf.f;
 
       auto d = spot::make_bdd_dict();
 
diff --git a/tests/core/equalsf.cc b/tests/core/equalsf.cc
index 46a1bd633..cb8cee54c 100644
--- a/tests/core/equalsf.cc
+++ b/tests/core/equalsf.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire de
 // Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -95,21 +95,20 @@ main(int argc, char** argv)
 	  return 2;
 	}
 
-      spot::parse_error_list p2;
-      auto f2 = spot::parse_infix_psl(formulas[size - 1], p2);
+      auto pf2 = spot::parse_infix_psl(formulas[size - 1]);
 
-      if (spot::format_parse_errors(std::cerr, formulas[size - 1], p2))
+      if (pf2.format_errors(std::cerr))
 	return 2;
+      auto f2 = pf2.f;
 
       for (unsigned n = 0; n < size - 1; ++n)
 	{
 
-	  spot::parse_error_list p1;
-	  auto f1 = spot::parse_infix_psl(formulas[n], p1);
+	  auto pf1 = spot::parse_infix_psl(formulas[n]);
 
-	  if (check_first &&
-	      spot::format_parse_errors(std::cerr, formulas[n], p1))
+	  if (check_first && pf1.format_errors(std::cerr))
 	    return 2;
+	  auto f1 = pf1.f;
 
 	  int exit_code = 0;
 
diff --git a/tests/core/ikwiad.cc b/tests/core/ikwiad.cc
index dfb6f5de9..56b45ba01 100644
--- a/tests/core/ikwiad.cc
+++ b/tests/core/ikwiad.cc
@@ -908,11 +908,11 @@ checked_main(int argc, char** argv)
 	case TransTAA:
 	case TransCompo:
 	  {
-	    spot::parse_error_list pel;
 	    tm.start("parsing formula");
-	    f = spot::parse_infix_psl(input, pel, env, debug_opt);
+	    auto pf = spot::parse_infix_psl(input, env, debug_opt);
 	    tm.stop("parsing formula");
-	    exit_code = spot::format_parse_errors(std::cerr, input, pel);
+	    exit_code = pf.format_errors(std::cerr);
+	    f = pf.f;
 	  }
 	  break;
 	}
diff --git a/tests/core/kind.cc b/tests/core/kind.cc
index e596f3406..53b543b3e 100644
--- a/tests/core/kind.cc
+++ b/tests/core/kind.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2010, 2012, 2015 Laboratoire de Recherche et
+// Copyright (C) 2010, 2012, 2015, 2016 Laboratoire de Recherche et
 // Developement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -59,9 +59,10 @@ main(int argc, char **argv)
       std::getline(ss, expected);
 
       spot::parse_error_list p1;
-      auto f1 = spot::parse_infix_psl(form, p1);
-      if (spot::format_parse_errors(std::cerr, form, p1))
+      auto pf1 = spot::parse_infix_psl(form);
+      if (pf1.format_errors(std::cerr))
 	return 2;
+      auto f1 = pf1.f;
 
       std::ostringstream so;
       spot::print_formula_props(so, f1, true);
diff --git a/tests/core/length.cc b/tests/core/length.cc
index c5e12be77..2df3ed530 100644
--- a/tests/core/length.cc
+++ b/tests/core/length.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2015 Laboratoire de Recherche et Developement de
-// l'Epita (LRDE).
+// Copyright (C) 2012, 2015, 2016 Laboratoire de Recherche et
+// Developement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
 //
@@ -45,11 +45,10 @@ main(int argc, char **argv)
     }
 
   {
-    spot::parse_error_list p1;
-    auto f1 = spot::parse_infix_psl(argv[1], p1);
-
-    if (spot::format_parse_errors(std::cerr, argv[1], p1))
+    auto pf1 = spot::parse_infix_psl(argv[1]);
+    if (pf1.format_errors(std::cerr))
       return 2;
+    auto f1 = pf1.f;
 
     if (boolone)
       std::cout << spot::length_boolone(f1) << std::endl;
diff --git a/tests/core/ltlprod.cc b/tests/core/ltlprod.cc
index 168d067d2..0aa0d1243 100644
--- a/tests/core/ltlprod.cc
+++ b/tests/core/ltlprod.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2012, 2014, 2015 Laboratoire de Recherche
-// et Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2012, 2014, 2015, 2016 Laboratoire de
+// Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de
 // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
 // Université Pierre et Marie Curie.
@@ -46,17 +46,15 @@ main(int argc, char** argv)
   {
     spot::environment& env(spot::default_environment::instance());
 
-    spot::parse_error_list pel1;
-    auto f1 = spot::parse_infix_psl(argv[1], pel1, env);
-
-    if (spot::format_parse_errors(std::cerr, argv[1], pel1))
+    auto pf1 = spot::parse_infix_psl(argv[1], env);
+    if (pf1.format_errors(std::cerr))
       return 2;
+    auto f1 = pf1.f;
 
-    spot::parse_error_list pel2;
-    auto f2 = spot::parse_infix_psl(argv[2], pel2, env);
-
-    if (spot::format_parse_errors(std::cerr, argv[2], pel2))
+    auto pf2 = spot::parse_infix_psl(argv[2], env);
+    if (pf2.format_errors(std::cerr))
       return 2;
+    auto f2 = pf2.f;
 
     auto dict = spot::make_bdd_dict();
     {
diff --git a/tests/core/ltlrel.cc b/tests/core/ltlrel.cc
index c186fc90c..060ff72a5 100644
--- a/tests/core/ltlrel.cc
+++ b/tests/core/ltlrel.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et Developement
+// Copyright (C) 2013, 2014, 2015, 2016 Laboratoire de Recherche et Developement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -38,11 +38,10 @@ main(int argc, char **argv)
     syntax(argv[0]);
 
   {
-    spot::parse_error_list p1;
-    auto f1 = spot::parse_infix_psl(argv[1], p1);
-
-    if (spot::format_parse_errors(std::cerr, argv[1], p1))
+    auto pf1 = spot::parse_infix_psl(argv[1]);
+    if (pf1.format_errors(std::cerr))
       return 2;
+    auto f1 = pf1.f;
 
     spot::relabeling_map* m = new spot::relabeling_map;
     auto f2 = spot::relabel_bse(f1, spot::Pnn, m);
diff --git a/tests/core/randtgba.cc b/tests/core/randtgba.cc
index 34f39bce6..9066bcb69 100644
--- a/tests/core/randtgba.cc
+++ b/tests/core/randtgba.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire
 // de Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -860,15 +860,14 @@ main(int argc, char** argv)
 		break;
 	      else if (input == "")
 		break;
-              spot::parse_error_list pel;
-              auto f = spot::parse_infix_psl(input, pel, env);
-              if (spot::format_parse_errors(std::cerr, input, pel))
+              auto pf = spot::parse_infix_psl(input, env);
+              if (pf.format_errors(std::cerr))
 		{
 		  exit_code = 1;
 		  break;
 		}
-              formula = spot::ltl_to_tgba_fm(f, dict, true);
-              auto* tmp = spot::atomic_prop_collect(f);
+              formula = spot::ltl_to_tgba_fm(pf.f, dict, true);
+              auto* tmp = spot::atomic_prop_collect(pf.f);
               for (auto i: *tmp)
 		apf->insert(i);
               delete tmp;
diff --git a/tests/core/readltl.cc b/tests/core/readltl.cc
index eb35a930b..4436d996b 100644
--- a/tests/core/readltl.cc
+++ b/tests/core/readltl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2012, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2012, 2015, 2016 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -55,12 +55,13 @@ main(int argc, char** argv)
 
   {
     spot::environment& env(spot::default_environment::instance());
-    spot::parse_error_list pel;
-    auto f = spot::parse_infix_psl(argv[formula_index], pel, env, debug);
-
-    exit_code =
-      spot::format_parse_errors(std::cerr, argv[formula_index], pel);
 
+    auto f = [&]()
+    {
+      auto pf = spot::parse_infix_psl(argv[formula_index], env, debug);
+      exit_code = pf.format_errors(std::cerr);
+      return pf.f;
+    }();
 
     if (f)
       {
diff --git a/tests/core/reduc.cc b/tests/core/reduc.cc
index 0e073043c..aae223adb 100644
--- a/tests/core/reduc.cc
+++ b/tests/core/reduc.cc
@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*_
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016 Laboratoire
 // de Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -178,17 +178,17 @@ main(int argc, char** argv)
 	  }
 	while (input == "");
 
-	spot::parse_error_list p1;
-	f1 = spot::parse_infix_psl(input, p1);
-	if (spot::format_parse_errors(std::cerr, input, p1))
+	auto pf1 = spot::parse_infix_psl(input);
+	if (pf1.format_errors(std::cerr))
 	  return 2;
+	f1 = pf1.f;
       }
     else
       {
-	spot::parse_error_list p1;
-	f1 = spot::parse_infix_psl(argv[2], p1);
-	if (spot::format_parse_errors(std::cerr, argv[2], p1))
+	auto pf1 = spot::parse_infix_psl(argv[2]);
+	if (pf1.format_errors(std::cerr))
 	  return 2;
+	f1 = pf1.f;
       }
 
     if (argc == 4)
@@ -199,10 +199,10 @@ main(int argc, char** argv)
 	    exit(2);
 	  }
 
-	spot::parse_error_list p2;
-	f2 = spot::parse_infix_psl(argv[3], p2);
-	if (spot::format_parse_errors(std::cerr, argv[3], p2))
+	auto pf2 = spot::parse_infix_psl(argv[3]);
+	if (pf2.format_errors(std::cerr))
 	  return 2;
+	f2 = pf2.f;
       }
 
     {
diff --git a/tests/core/safra.cc b/tests/core/safra.cc
index 0e1c63555..b7e476696 100644
--- a/tests/core/safra.cc
+++ b/tests/core/safra.cc
@@ -111,13 +111,12 @@ int main(int argc, char* argv[])
   spot::twa_graph_ptr res;
   if (in_ltl)
     {
-      spot::parse_error_list pel;
-      spot::formula f = spot::parse_infix_psl(input, pel);
-      if (spot::format_parse_errors(std::cerr, input, pel))
+      auto pf = spot::parse_infix_psl(input);
+      if (pf.format_errors(std::cerr))
         return 2;
       spot::translator trans(dict);
       trans.set_pref(spot::postprocessor::Deterministic);
-      auto tmp = trans.run(f);
+      auto tmp = trans.run(pf.f);
       res = spot::tgba_determinize(tmp, pretty_print, scc_opt,
 				   use_bisim, use_stutter);
     }
diff --git a/tests/core/syntimpl.cc b/tests/core/syntimpl.cc
index 7dbe87d50..d5c29723b 100644
--- a/tests/core/syntimpl.cc
+++ b/tests/core/syntimpl.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de
-// Recherche et Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014, 2015, 2016
+// Laboratoire de Recherche et Développement de l'Epita (LRDE).
 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6
 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
 // Pierre et Marie Curie.
@@ -45,20 +45,18 @@ main(int argc, char** argv)
   int exit_return = 0;
 
   {
-    spot::parse_error_list p1;
-    auto ftmp1 = spot::parse_infix_psl(argv[2], p1);
+    auto ftmp1 = spot::parse_infix_psl(argv[2]);
 
-    if (spot::format_parse_errors(std::cerr, argv[2], p1))
+    if (ftmp1.format_errors(std::cerr))
       return 2;
 
-    spot::parse_error_list p2;
-    auto ftmp2 = spot::parse_infix_psl(argv[3], p2);
+    auto ftmp2 = spot::parse_infix_psl(argv[3]);
 
-    if (spot::format_parse_errors(std::cerr, argv[3], p2))
+    if (ftmp2.format_errors(std::cerr))
       return 2;
 
-    spot::formula f1 = spot::negative_normal_form(ftmp1);
-    spot::formula f2 = spot::negative_normal_form(ftmp2);
+    spot::formula f1 = spot::negative_normal_form(ftmp1.f);
+    spot::formula f2 = spot::negative_normal_form(ftmp2.f);
 
     std::string f1s = spot::str_psl(f1);
     std::string f2s = spot::str_psl(f2);
diff --git a/tests/core/tostring.cc b/tests/core/tostring.cc
index 5b7477118..8ca878299 100644
--- a/tests/core/tostring.cc
+++ b/tests/core/tostring.cc
@@ -1,6 +1,6 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2008, 2009, 2012, 2015 Laboratoire de Recherche et
-// Développement de l'Epita (LRDE).
+// Copyright (C) 2008, 2009, 2012, 2015, 2016 Laboratoire de Recherche
+// et Développement de l'Epita (LRDE).
 // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
 // et Marie Curie.
@@ -40,11 +40,10 @@ main(int argc, char **argv)
     syntax(argv[0]);
 
   {
-    spot::parse_error_list p1;
-    auto f1 = spot::parse_infix_psl(argv[1], p1);
-
-    if (spot::format_parse_errors(std::cerr, argv[1], p1))
+    auto pf1 = spot::parse_infix_psl(argv[1]);
+    if (pf1.format_errors(std::cerr))
       return 2;
+    auto f1 = pf1.f;
 
     // The string generated from an abstract tree should be parsable
     // again.
@@ -52,10 +51,10 @@ main(int argc, char **argv)
     std::string f1s = spot::str_psl(f1);
     std::cout << f1s << '\n';
 
-    auto f2 = spot::parse_infix_psl(f1s, p1);
-
-    if (spot::format_parse_errors(std::cerr, f1s, p1))
+    auto pf2 = spot::parse_infix_psl(f1s);
+    if (pf2.format_errors(std::cerr))
       return 2;
+    auto f2 = pf2.f;
 
     // This second abstract tree should be equal to the first.
 
diff --git a/tests/ltsmin/modelcheck.cc b/tests/ltsmin/modelcheck.cc
index 14d7b03a5..1cf1b75f2 100644
--- a/tests/ltsmin/modelcheck.cc
+++ b/tests/ltsmin/modelcheck.cc
@@ -192,9 +192,9 @@ checked_main(int argc, char **argv)
 
   tm.start("parsing formula");
   {
-    spot::parse_error_list pel;
-    f = spot::parse_infix_psl(argv[2], pel, env, false);
-    exit_code = spot::format_parse_errors(std::cerr, argv[2], pel);
+    auto pf = spot::parse_infix_psl(argv[2], env, false);
+    exit_code = pf.format_errors(std::cerr);
+    f = pf.f;
   }
   tm.stop("parsing formula");
 
diff --git a/tests/python/alarm.py b/tests/python/alarm.py
index 563396a0b..30af57206 100755
--- a/tests/python/alarm.py
+++ b/tests/python/alarm.py
@@ -1,6 +1,6 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2012, 2014, 2015  Laboratoire de Recherche et Développement
-# de l'Epita
+# Copyright (C) 2012, 2014, 2015, 2016 Laboratoire de Recherche et
+# Développement de l'Epita
 #
 # This file is part of Spot, a model checking library.
 #
@@ -43,8 +43,7 @@ P_Rbt2.moins || P_Rbt2.stop))-> G((F "map[0]==1") && (F "map[1]==1")
 "map[9]==3")))"""
 
 e = spot.default_environment.instance()
-p = spot.empty_parse_error_list()
-f = spot.parse_infix_psl(f, p, e)
+pf = spot.parse_infix_psl(f, e)
 d = spot.make_bdd_dict()
 
 spot.unblock_signal(signal.SIGALRM)
@@ -58,9 +57,9 @@ if child != 0:
     # If the child returns, before we get the alarm it's a bug.
     exit(1)
 
-# This is expected to take WAY more that 2s.
+# This is expected to take WAY more than 2s.
 print("Before")
-spot.ltl_to_tgba_fm(f, d, True)
+spot.ltl_to_tgba_fm(pf.f, d, True)
 print("After")
 
 exit(1)
diff --git a/tests/python/interdep.py b/tests/python/interdep.py
index 4a767ebef..57acffa1f 100755
--- a/tests/python/interdep.py
+++ b/tests/python/interdep.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2010, 2012, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
 # Développement de l'EPITA.
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6
 # (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -29,12 +29,11 @@ import sys
 simp = spot.tl_simplifier()
 
 e = spot.default_environment.instance()
-p = spot.empty_parse_error_list()
-f = spot.parse_infix_psl('GFa', p, e)
+pf = spot.parse_infix_psl('GFa', e)
 d = simp.get_dict()
-a = spot.ltl_to_tgba_fm(f, d)
-g = spot.parse_infix_boolean('b&c', p, e)
-b = simp.as_bdd(g)
+a = spot.ltl_to_tgba_fm(pf.f, d)
+g = spot.parse_infix_boolean('b&c', e)
+b = simp.as_bdd(g.f)
 buddy.bdd_printset(b); spot.nl_cout()
 del g
 
@@ -54,5 +53,5 @@ del it
 del s0
 del b
 del c
-del f
+del pf
 del simp
diff --git a/tests/python/ltl2tgba.py b/tests/python/ltl2tgba.py
index 596cf88bd..83d4055dd 100755
--- a/tests/python/ltl2tgba.py
+++ b/tests/python/ltl2tgba.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -83,11 +83,11 @@ cout = spot.get_cout()
 cerr = spot.get_cerr()
 
 e = spot.default_environment.instance()
-p = spot.empty_parse_error_list()
 
-f = spot.parse_infix_psl(args[0], p, e, debug_opt)
-if spot.format_parse_errors(cerr, args[0], p):
+pf = spot.parse_infix_psl(args[0], e, debug_opt)
+if pf.format_errors(cerr):
     exit_code = 1
+f = pf.f
 
 dict = spot.make_bdd_dict()
 
@@ -128,5 +128,6 @@ if f:
 else:
     exit_code = 1
 
+del pf
 del dict
 assert spot.fnode_instances_check()
diff --git a/tests/python/ltlparse.py b/tests/python/ltlparse.py
index f30f7ea27..de4bff9d6 100755
--- a/tests/python/ltlparse.py
+++ b/tests/python/ltlparse.py
@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2009, 2010, 2012, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2009, 2010, 2012, 2014, 2015, 2016 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 # Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
 # département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -24,22 +24,21 @@ import sys
 import spot
 
 e = spot.default_environment.instance()
-p = spot.empty_parse_error_list()
 
 l = ['GFa', 'a U (((b)) xor c)', '!(FFx <=> Fx)', 'a \/ a \/ b \/ a \/ a'];
 
 for str1 in l:
-    f = spot.parse_infix_psl(str1, p, e, False)
-    if spot.format_parse_errors(spot.get_cout(), str1, p):
+    pf = spot.parse_infix_psl(str1, e, False)
+    if pf.format_errors(spot.get_cout()):
         sys.exit(1)
-    str2 = str(f)
-    del f
+    str2 = str(pf.f)
+    del pf
     sys.stdout.write(str2 + "\n")
     # Try to reparse the stringified formula
-    f = spot.parse_infix_psl(str2, p, e)
-    if spot.format_parse_errors(spot.get_cout(), str2, p):
+    pf = spot.parse_infix_psl(str2, e)
+    if pf.format_errors(spot.get_cout()):
         sys.exit(1)
-    sys.stdout.write(str(f) + "\n")
-    del f
+    sys.stdout.write(str(pf.f) + "\n")
+    del pf
 
 assert spot.fnode_instances_check()