1 files changed, 28 insertions, 0 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 98273d86..d605b860 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -5559,6 +5559,34 @@ namespace Microsoft.Dafny {
     }
   }
 
+  /// <summary>
+  /// An AutoGeneratedExpression is simply a wrapper around an expression.  This expression tells the generation of hover text (in the Dafny IDE)
+  /// that the expression was no supplied directly in the program text and should therefore be ignored.  In other places, an AutoGeneratedExpression
+  /// is just a parenthesized expression, which means that it works just the like expression .E that it contains.
+  /// (Ironically, AutoGeneratedExpression, which is like the antithesis of concrete syntax, inherits from ConcreteSyntaxExpression, which perhaps
+  /// should rather have been called SemanticsNeutralExpressionWrapper.)
+  /// </summary>
+  public class AutoGeneratedExpression : ParensExpression
+  {
+    public AutoGeneratedExpression(IToken tok, Expression e)
+      : base(tok, e) {
+      Contract.Requires(tok != null);
+      Contract.Requires(e != null);
+    }
+
+    /// <summary>
+    /// This maker method takes a resolved expression "e" and wraps a resolved AutoGeneratedExpression
+    /// around it.
+    /// </summary>
+    public static AutoGeneratedExpression Create(Expression e) {
+      Contract.Requires(e != null);
+      var a = new AutoGeneratedExpression(e.tok, e);
+      a.type = e.Type;
+      a.ResolvedExpression = e;
+      return a;
+    }
+  }
+
   public class ChainingExpression : ConcreteSyntaxExpression
   {
     public readonly List<Expression> Operands;