From 34ba22283de5d262e059eafe2dcca97d052b1dc9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 16 Jun 2004 21:05:58 +0000
Subject: Fix error regexps for matching additional comma printed in position
 [NB: for PGIP patched position.ML].

---
 isar/isar.el | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/isar/isar.el b/isar/isar.el
index 539df682..d3555896 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -211,8 +211,8 @@ See -k option for Isabelle interface script."
    proof-shell-error-regexp             "\364\\*\\*\\*"
    proof-shell-abort-goal-regexp        nil     ; n.a.
 
-   pg-next-error-regexp	  "\\((line \\([0-9]+\\) of \"[^\"]+\")\\)"
-   pg-next-error-filename-regexp "\\((line [0-9]+ of \"\\([^\"]+\\)\")\\)"
+   pg-next-error-regexp	  "\\((line \\([0-9]+\\)[,] of \"[^\"]+\")\\)"
+   pg-next-error-filename-regexp "\\((line [0-9]+[,] of \"\\([^\"]+\\)\")\\)"
 
    ;; matches names of assumptions
    proof-shell-assumption-regexp        isar-id
-- 
cgit v1.2.3