From 1c3270d819e95cdf222b564e34d657a2dfd38a0e Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 12 Dec 2024 00:20:09 +0100
Subject: [PATCH] fix #1371

---
 tools/Holmake/HolLex                     |  2 ++
 tools/Holmake/tests/gh1371/Holmakefile   |  4 ++++
 tools/Holmake/tests/gh1371/bugScript.sml | 13 +++++++++++++
 tools/Holmake/tests/gh1371/doit.sh       | 13 +++++++++++++
 4 files changed, 32 insertions(+)
 create mode 100644 tools/Holmake/tests/gh1371/Holmakefile
 create mode 100644 tools/Holmake/tests/gh1371/bugScript.sml
 create mode 100755 tools/Holmake/tests/gh1371/doit.sh

diff --git a/tools/Holmake/HolLex b/tools/Holmake/HolLex
index 9235010454..14a460cbfe 100644
--- a/tools/Holmake/HolLex
+++ b/tools/Holmake/HolLex
@@ -118,6 +118,8 @@ fun parseDecls (STATE {parseError, pardepth, ...}) continue pos test = let
       | CloseParen p => cont (p, ")") false
       | EndTok p => cont (p, "End") true
       | QED p => cont (p, "QED") true
+      | ProofLine pt => cont pt false
+      | TerminationTok p => cont (p, "Termination") false
       | EOF p => (finish p, NONE, p, SOME tk)
       | _ => raise Unreachable
     end
diff --git a/tools/Holmake/tests/gh1371/Holmakefile b/tools/Holmake/tests/gh1371/Holmakefile
new file mode 100644
index 0000000000..a85c04e147
--- /dev/null
+++ b/tools/Holmake/tests/gh1371/Holmakefile
@@ -0,0 +1,4 @@
+gh1371.log: doit.sh bugScript.sml
+	$(tee ./doit.sh $(protect $(HOLDIR)/bin/unquote), $@)
+
+EXTRA_CLEANS = gh1371.log
diff --git a/tools/Holmake/tests/gh1371/bugScript.sml b/tools/Holmake/tests/gh1371/bugScript.sml
new file mode 100644
index 0000000000..5b3f719d4e
--- /dev/null
+++ b/tools/Holmake/tests/gh1371/bugScript.sml
@@ -0,0 +1,13 @@
+val _ = new_theory "bug"
+
+Theorem foo:
+  foo
+Proof
+  foo [``]
+QED
+
+Theorem bar:
+  bar
+Proof
+  bar
+QED
diff --git a/tools/Holmake/tests/gh1371/doit.sh b/tools/Holmake/tests/gh1371/doit.sh
new file mode 100755
index 0000000000..ac3146cfb3
--- /dev/null
+++ b/tools/Holmake/tests/gh1371/doit.sh
@@ -0,0 +1,13 @@
+#!/bin/bash
+
+ulimit -t 2
+unquote=$1
+
+echo "Running unquote"
+$unquote < bugScript.sml
+
+retcode=$?
+echo
+echo "unquote completed with code $retcode"
+
+exit $retcode