src/Tools/qed.cc

--- a/src/Tools/qed.cc	Fri Feb 17 13:25:11 1995 +0100
+++ b/src/Tools/qed.cc	Fri Feb 24 11:52:19 1995 +0100
@@ -1,5 +1,5 @@
 // Little utility to convert result() -> qed ... in Isabelle's files
-// Written in 1994 by Carsten Clasohm ([e-mail])
+// Written in 1995 by Carsten Clasohm ([e-mail])
 
 #define LIN_LEN   1000		// maximal length of lines in sourcefile
 
@@ -11,6 +11,18 @@
 #include <unistd.h>
 #include <ctype.h>
 
+// Null terminated list of theorem names that must not be included in the
+// theorem database
+char * excludeName[] = {"temp", "tmp", 0};
+
+int ExcludeThm(char *name)
+{
+    for (int i = 0; excludeName[i]; i++)
+	if (strcmp(name, excludeName[i]) == 0)
+	    return 1;
+    return 0;
+}
+
 main(int argc, char *argv[])
 {
     char l[LIN_LEN];
@@ -41,7 +53,7 @@
 	char *eqPos;
 	char *tmp;
 
-	if ((rPos = strstr(l, "result()")) && (!isalpha(*(rPos-1)))
+	if ((rPos = strstr(l, "result()")) && (!isalnum(*(rPos-1)))
 	    && (valPos = strstr(l, "val ")) && (eqPos = strstr(l, "=")))
 	{                            // does line contain "result()" and "val"?
 	    char name[LIN_LEN];
@@ -49,7 +61,7 @@
 	    assert(eqPos-(valPos+4) > 0);
 	    strncpy(name, valPos+4, eqPos-(valPos+4));
 	    name[eqPos-(valPos+4)] = 0;
-	    if (!isalpha(name[eqPos-(valPos+4)-1]))
+	    if (!isalnum(name[eqPos-(valPos+4)-1]))
 	        name[eqPos-(valPos+4)-1] = 0;
 #ifdef DEBUG
 	    cerr << "Found result: \"" << name << "\"\n";
@@ -57,7 +69,9 @@
 	    char prefix[LIN_LEN];
 	    char arg[LIN_LEN];
 
-	    if ((rPos - eqPos < 5) && (rPos == strstr(l, "result();")))
+	    if (ExcludeThm(name))
+		out << l << '\n';
+	    else if ((rPos - eqPos < 5) && (rPos == strstr(l, "result();")))
 	    {                                              // replace by "qed"?
 		strncpy(prefix, l, valPos-l);
 		prefix[valPos-l] = 0;
@@ -75,8 +89,8 @@
 	    }
 	}
 	else if ((rPos = strstr(l, "prove_goal")) 
-		 && (!isalpha(*(rPos-1))) 
-		 && (!isalpha(*(rPos+10)) || (*(rPos+10) == 'w'))
+		 && (!isalnum(*(rPos-1))) 
+		 && (!isalnum(*(rPos+10)) || (*(rPos+10) == 'w'))
 		 && (valPos = strstr(l, "val ")) 
 		 && (eqPos = strstr(l, "="))
                  && (rPos - eqPos < 5))
@@ -86,22 +100,28 @@
 	    assert(eqPos-(valPos+4) > 0);
 	    strncpy(name, valPos+4, eqPos-(valPos+4));
 	    name[eqPos-(valPos+4)] = 0;
-	    if (!isalpha(name[eqPos-(valPos+4)-1]))
+	    if (!isalnum(name[eqPos-(valPos+4)-1]))
 	        name[eqPos-(valPos+4)-1] = 0;
 #ifdef DEBUG
 	    cerr << "Found prove_goal: \"" << name << "\"\n";
 #endif
-	    char prefix[LIN_LEN];
-	    char arg[LIN_LEN];
+	    if (ExcludeThm(name))
+		out << l << '\n';
+	    else
+	    {
+	        char prefix[LIN_LEN];
+	        char arg[LIN_LEN];
 
-	    strncpy(prefix, l, valPos-l);
-	    prefix[valPos-l] = 0;
-	    out << prefix << "qed_goal" << ((*(rPos+10) == 'w') ? "w " : " ")
-		<< '\"' << name << '\"' << strchr(rPos, ' ') << '\n';
+	        strncpy(prefix, l, valPos-l);
+	        prefix[valPos-l] = 0;
+	        out << prefix << "qed_goal"
+                    << ((*(rPos+10) == 'w') ? "w " : " ")
+		    << '\"' << name << '\"' << strchr(rPos, ' ') << '\n';
+	    }
 	}
 	else if ((rPos = strstr(l, "standard"))
-		 && (!isalpha(*(rPos-1))) 
-		 && (!isalpha(*(rPos+8))) 
+		 && (!isalnum(*(rPos-1))) 
+		 && (!isalnum(*(rPos+8))) 
 		 && (valPos = strstr(l, "val ")) 
 		 && (eqPos = strstr(l, "="))
                  && (rPos - eqPos < 5)
@@ -112,19 +132,24 @@
 	    assert(eqPos-(valPos+4) > 0);
 	    strncpy(name, valPos+4, eqPos-(valPos+4));
 	    name[eqPos-(valPos+4)] = 0;
-	    if (!isalpha(name[eqPos-(valPos+4)-1]))
+	    if (!isalnum(name[eqPos-(valPos+4)-1]))
 	        name[eqPos-(valPos+4)-1] = 0;
 #ifdef DEBUG
 	    cerr << "Found standard: \"" << name << "\"\n";
 #endif
-	    char prefix[LIN_LEN];
-	    char arg[LIN_LEN];
+	    if (ExcludeThm(name))
+		out << l << '\n';
+	    else
+	    {
+	        char prefix[LIN_LEN];
+	        char arg[LIN_LEN];
 
-	    strncpy(prefix, l, valPos-l);
-	    prefix[valPos-l] = 0;
-	    strcpy(l+strlen(l)-1, ");");        // insert ")" before line's ';'
-	    out << prefix << "bind_thm (\"" << name << "\","
-	        << strchr(rPos, ' ') << '\n';
+	        strncpy(prefix, l, valPos-l);
+	        prefix[valPos-l] = 0;
+	        strcpy(l+strlen(l)-1, ");");    // insert ")" before line's ';'
+	        out << prefix << "bind_thm (\"" << name << "\","
+	            << strchr(rPos, ' ') << '\n';
+            }
 	}
 	else                                           // output line unchanged
 	    out << l << '\n';