5 files changed, 37 insertions, 21 deletions
diff --git a/contrib/depgraph b/contrib/depgraph
index e85bcd694..2c4eba595 100755
--- a/contrib/depgraph
+++ b/contrib/depgraph
@@ -88,6 +88,7 @@ for path in $paths; do
     if [ -n "$target" -a "$target" != "$package" ]; then continue; fi
     for inc in $incs; do
       case "$inc" in
+        base/tls.h) inc=base/tls.h.in ;;
         expr/expr.h) inc=expr/expr_template.h ;;
         expr/expr_manager.h) inc=expr/expr_manager_template.h ;;
         expr/kind.h) inc=expr/kind_template.h ;;
@@ -95,7 +96,6 @@ for path in $paths; do
         theory/theoryof_table.h) inc=theory/theoryof_table_template.h ;;
         util/integer.h) inc=util/integer.h.in ;;
         util/rational.h) inc=util/rational.h.in ;;
-        util/tls.h) inc=util/tls.h.in ;;
         cvc4autoconfig.h) inc=cvc4autoconfig.h.in ;;
       esac
       incpath=
diff --git a/contrib/new-theory b/contrib/new-theory
index 8f9714372..0d9e45647 100755
--- a/contrib/new-theory
+++ b/contrib/new-theory
@@ -119,6 +119,15 @@ function copyaltskel {
     > "src/theory/$dir/$dest"
 }
 
+function copyoptions {
+  src="$1"
+  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
+  echo "Creating src/options/$dest..."
+  sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
+    contrib/optionsskel/$src \
+    > "src/options/$dest"
+}
+
 # copy files from the skeleton, with proper replacements
 if $alternate; then
   alternate01=1
@@ -131,6 +140,11 @@ else
     copyskel "$file"
   done
 fi
+# Copy the options file independently
+for file in `ls contrib/optionsskel`; do
+  copyoptions "$file"
+done
+
 
 echo
 echo "Adding $dir to THEORIES to src/Makefile.theories..."
@@ -158,19 +172,18 @@ perl -e '
     while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp \\\n\ttheory/'"$dir"'/theory_'"$dir"'_rewriter.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'_type_rules.h\n"; last; } else { print; } }
   }
   while(<>) { print; last if /^EXTRA_DIST = /; }
-  while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/kinds \\\n\ttheory/'"$dir"'/options_handlers.h\n"; last; } else { print; } }
+  while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/kinds\n"; last; } else { print; } }
   while(<>) { print; }' src/Makefile.am > src/Makefile.am.new-theory
 if ! mv -f src/Makefile.am.new-theory src/Makefile.am; then
   echo "ERROR: cannot replace src/Makefile.am !" >&2
   exit 1
 fi
 
-echo "Adding ../theory/$dir/options.cpp to OPTIONS_FILES_SRCS"
-echo "  and nodist_liboptions_la_SOURCES to src/options/Makefile.am..."
-if grep -q '^	\.\./theory/'"$dir"'/options\.cpp\>' src/options/Makefile.am &>/dev/null; then
+echo "Adding ${dir}_options to src/options/Makefile.am..."
+if grep -q '^	${dir}_options' src/options/Makefile.am &>/dev/null; then
   echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
 else
-  awk '!/^OPTIONS_FILES_SRCS = \\|^nodist_liboptions_la_SOURCES = / {print$0} /^OPTIONS_FILES_SRCS = \\|^nodist_liboptions_la_SOURCES = / {while(/\\ *$/){print $0;getline} print $0,"\\";print "\t../theory/'"$dir"'/options.cpp","\\";print "\t../theory/'"$dir"'/options.h";}' src/options/Makefile.am > src/options/Makefile.am.new-theory
+  awk -v name="$dir" -f contrib/new-theory.awk src/options/Makefile.am > src/options/Makefile.am.new-theory
   if ! cp -f src/options/Makefile.am src/options/Makefile.am~; then
     echo "ERROR: cannot copy src/options/Makefile.am !" >&2
     exit 1
diff --git a/contrib/new-theory.awk b/contrib/new-theory.awk
new file mode 100755
index 000000000..6c523f259
--- /dev/null
+++ b/contrib/new-theory.awk
@@ -0,0 +1,17 @@
+#!/bin/awk -v name=theory_new -f
+#
+
+# The do nothing rule
+!/^OPTIONS_SRC_FILES = \\|^OPTIONS_TEMPS = \\|^OPTIONS_OPTIONS_FILES = \\|^OPTIONS_SEDS = \\|^OPTIONS_HEADS = \\|^OPTIONS_CPPS = \\/ {print$0}
+# Add the name to the correct locations.
+/^OPTIONS_SRC_FILES = \\/{print $0; printf "\t%s_options \\\n", name;}
+/^OPTIONS_TEMPS = \\/{print $0; printf "\t%s_options.tmp \\\n", name;}
+/^OPTIONS_OPTIONS_FILES = \\/{print $0; printf "\t%s_options.options \\\n", name;}
+/^OPTIONS_SEDS = \\/{print $0; printf "\t%s_options.sed \\\n", name;}
+/^OPTIONS_HEADS = \\/{print $0; printf "\t%s_options.h \\\n", name;}
+/^OPTIONS_CPPS = \\/{print $0; printf "\t%s_options.cpp \\\n", name;}
+# Add the rule for name_options.
+END{printf "%s_options:;\n", name}
+# Add the rules for name_options.tmp
+END{printf ".PHONY: %s_options.tmp\n", name}
+END{printf "%s_options.tmp:\n\techo \"$@\" \"$(@:.tmp=)\"\n\t$(AM_V_GEN)(cp \"@srcdir@/$(@:.tmp=)\" \"$@\" || true)\n", name}
diff --git a/contrib/theoryskel/options b/contrib/optionsskel/DIR_options
index f627dc4a0..de160df6d 100644
--- a/contrib/theoryskel/options
+++ b/contrib/optionsskel/DIR_options
@@ -3,6 +3,6 @@
 # See src/options/base_options for a description of this file format
 #
 
-module $id "theory/$dir/options.h" $camel
+module $id "options/$dir_options.h" $camel
 
 endmodule
diff --git a/contrib/theoryskel/options_handlers.h b/contrib/theoryskel/options_handlers.h
deleted file mode 100644
index d384e84d9..000000000
--- a/contrib/theoryskel/options_handlers.h
+++ /dev/null
@@ -1,14 +0,0 @@
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
-#define __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__$id__OPTIONS_HANDLERS_H */