From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 9 Sep 2013 19:27:22 +0000 (-0400)
Subject: Fix some line-numbering in auto-generated metakind.h.  Thanks to Martin Brain for... 
X-Git-Tag: cvc5-1.0.0~7287^2~23
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d0734cf73454ecfd51556ca84daaba9025b28f8;p=cvc5.git

Fix some line-numbering in auto-generated metakind.h.  Thanks to Martin Brain for reporting this.
---

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 41813abde..e3f1b5c45 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -337,6 +337,7 @@ static inline Kind operatorToKind(::CVC4::expr::NodeValue* nv) {
 
   switch(Kind k CVC4_UNUSED = nv->getKind()) {
 ${metakind_operatorKinds}
+
   default:
     return kind::UNDEFINED_KIND;  /* LAST_KIND */
   };
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index d8192e432..7ffe0230b 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -303,8 +303,9 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > {
 function registerOperatorToKind {
   operatorKind=$1
   applyKind=$2
-  metakind_operatorKinds="${metakind_operatorKinds}    case kind::$applyKind: return kind::$operatorKind;
-";
+  metakind_operatorKinds="${metakind_operatorKinds}
+#line $lineno \"$kf\"
+    case kind::$applyKind: return kind::$operatorKind;";
 }
 
 function register_metakind {
@@ -381,8 +382,8 @@ while [ $# -gt 0 ]; do
     /* from $b */
 "
   metakind_operatorKinds="${metakind_operatorKinds}
-    /* from $b */
-"
+
+    /* from $b */"
   source "$kf"
   if ! $seen_theory; then
     echo "$kf: error: no theory content found in file!" >&2