# HG changeset patch # User clasohm # Date 793623139 -3600 # Node ID cc80f53b28c61446ca89d4208bf46a9ed6aa52a2 # Parent 77795af993153305d11219b7894bf81d45c476e5 added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum) diff -r 77795af99315 -r cc80f53b28c6 src/Tools/Makefile --- a/src/Tools/Makefile Fri Feb 17 13:25:11 1995 +0100 +++ b/src/Tools/Makefile Fri Feb 24 11:52:19 1995 +0100 @@ -9,5 +9,3 @@ qed: $(OBJS) g++ -o qed $(OBJS) - -qed.o: qed.cc diff -r 77795af99315 -r cc80f53b28c6 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 (clasohm@informatik.tu-muenchen.de) +// Written in 1995 by Carsten Clasohm (clasohm@informatik.tu-muenchen.de) #define LIN_LEN 1000 // maximal length of lines in sourcefile @@ -11,6 +11,18 @@ #include #include +// 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';