src/Tools/qed.cc

 // 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
 
 #include <iostream.h>
 #include <fstream.h>
 #include <string.h>
 #include <assert.h>
 #include <stdio.h>
 #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];
     int lines = 0;

 	char *rPos;
 	char *valPos;
 	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];
 
 	    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";
 #endif
 	    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;
 		out << prefix << "qed \"" << name << "\";" << '\n';
 	    }

 		out << prefix << "bind_thm(\"" << name << "\", "
 		    << arg << ");\n";
 	    }
 	}
 	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))
 	{                                    // replace prove_goal by qed_goal?
 	    char name[LIN_LEN];
 
 	    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)
                  && (l[strlen(l)-1] == ';'))
 	{                                                   // insert bind_thm?
 	    char name[LIN_LEN];
 
 	    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';
 	in.getline(l, LIN_LEN);
     }