From c544167584024513648b23052db1aa9dcd993c01 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 28 Jul 2015 15:55:49 +0200
Subject: Make coq-tex aware of lines ending with "}", so as to fix the FAQ.

This is only a heuristic and it might cause the tool to become awfully
confused if a line ends with "}" yet this is not the end of a tactic
block. Fixing it would require a full-blown Coq parser inside coq-tex.

Example of crazy output:

Coq < Goal { True }
Coq < 1 subgoal

  ============================
   {True} + {False}

Coq <    + { False }.
---
 tools/coq_tex.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 7f2fe741e9..fc652f584c 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -68,7 +68,7 @@ let begin_coq_example =
 let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
 let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
 let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
-let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
+let dot_end_line = Str.regexp "\\(\\.\\|}\\)[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
 
 let has_match r s =
   try let _ = Str.search_forward r s 0 in true with Not_found -> false
-- 
cgit v1.2.3