From f98a30f1ad7c441d8ef9e6e5740752723a43413a Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 6 May 2015 17:58:00 -0700
Subject: Added inductive predicates

---
 Source/DafnyExtension/OutliningTagger.cs | 1 +
 Source/DafnyExtension/TokenTagger.cs     | 1 +
 2 files changed, 2 insertions(+)

(limited to 'Source/DafnyExtension')

diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index c4b88f98..85771e94 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -160,6 +160,7 @@ namespace DafnyLanguage
               }
               if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {
                 var nm =
+                  m is Dafny.InductivePredicate ? "inductive predicate" :
                   m is Dafny.CoPredicate ? "copredicate" :
                   // m is Dafny.PrefixPredicate ? "prefix predicate" :  // this won't ever occur here
                   m is Dafny.Predicate ? "predicate" :
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs
index 0019ce81..af141ad7 100644
--- a/Source/DafnyExtension/TokenTagger.cs
+++ b/Source/DafnyExtension/TokenTagger.cs
@@ -308,6 +308,7 @@ namespace DafnyLanguage
                 case "import":
                 case "in":
                 case "include":
+                case "inductive":
                 case "int":
                 case "invariant":
                 case "iterator":
-- 
cgit v1.2.3