Review of mktheorytraits, mkrewriter, and recent changes to other mk* scripts. Minor changes only, correcting some documentation and fixing some warnings that were being issued about functions not existing.

1 files changed, 8 insertions, 12 deletions

diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 0b384d518..40bf9992c 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -2,7 +2,7 @@
 #
 # mkexpr
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010  The CVC4 Project
+# Copyright (c) 2010-2011  The CVC4 Project
 #
 # The purpose of this script is to create {expr,expr_manager}.{h,cpp}
 # from template files and a list of theory kinds.  Basically it just
@@ -15,7 +15,7 @@
 # Output is to standard out.
 #
 
-copyright=2010
+copyright=2010-2011
 
 filename=`basename "$1" | sed 's,_template,,'`
 
@@ -91,52 +91,48 @@ function theory {
 function rewriter {
   # rewriter class header
   lineno=${BASH_LINENO[0]}
+  check_theory_seen
 }
 
 function properties {
-    # properties prop*
-    lineno=${BASH_LINENO[0]}
+  # properties prop*
+  lineno=${BASH_LINENO[0]}
+  check_theory_seen
 }
 
 function endtheory {
   # endtheory
   lineno=${BASH_LINENO[0]}
+  check_theory_seen
 }
 
 function sort {
   # sort TYPE ["comment"]
   lineno=${BASH_LINENO[0]}
+  check_theory_seen
 }
 
 function variable {
   # variable K ["comment"]
-
   lineno=${BASH_LINENO[0]}
-
   check_theory_seen
 }
 
 function operator {
   # operator K #children ["comment"]
-
   lineno=${BASH_LINENO[0]}
-
   check_theory_seen
 }
 
 function parameterized {
   # parameterized K #children ["comment"]
-
   lineno=${BASH_LINENO[0]}
-
   check_theory_seen
 }
 
 function constant {
   # constant K T Hasher header ["comment"]
-
   lineno=${BASH_LINENO[0]}
-
   check_theory_seen
 
   includes="${includes}