fix #1371

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

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

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

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