Documenting compilation errors

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -1394,7 +1394,7 @@ public override void Compile(Program program, ConcreteSyntaxTree wrx) {
 
  var wIter = CreateIterator(iter, wr);
  if (iter.Body == null) {
- Error(iter.tok, "Iterator {0} has no body", wIter, iter.FullName);
+ Error(iter.tok, "iterator {0} has no body", wIter, iter.FullName);
  } else {
  TrStmtList(iter.Body.Body, wIter);
  }
@@ -1589,7 +1589,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
  if (member is Method m && member.FullDafnyName == name) {
  mainMethod = m;
  if (!IsPermittedAsMain(program, mainMethod, out string reason)) {
- ReportError(program.Reporter, mainMethod.tok, "The method \"{0}\" is not permitted as a main method ({1}).", null, name, reason);
+ ReportError(program.Reporter, mainMethod.tok, "The method '{0}' is not permitted as a main method ({1}).", null, name, reason);
  mainMethod = null;
  return false;
  } else {
@@ -1618,7 +1618,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
  hasMain = true;
  } else {
  // more than one main in the program
- ReportError(program.Reporter, m.tok, "More than one method is marked \"{{:main}}\". First declaration appeared at {0}.", null,
+ ReportError(program.Reporter, m.tok, "More than one method is marked '{{:main}}'. First declaration appeared at {0}.", null,
  ErrorReporter.TokenToString(mainMethod.tok));
  hasMain = false;
  }
@@ -1629,7 +1629,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
  }
  if (hasMain) {
  if (!IsPermittedAsMain(program, mainMethod, out string reason)) {
- ReportError(program.Reporter, mainMethod.tok, "This method marked \"{{:main}}\" is not permitted as a main method ({0}).", null, reason);
+ ReportError(program.Reporter, mainMethod.tok, "This method marked '{{:main}}' is not permitted as a main method ({0}).", null, reason);
  mainMethod = null;
  return false;
  } else {
@@ -1658,7 +1658,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
  hasMain = true;
  } else {
  // more than one main in the program
- ReportError(program.Reporter, m.tok, "More than one method is declared as \"{0}\". First declaration appeared at {1}.", null,
+ ReportError(program.Reporter, m.tok, "More than one method is declared as '{0}'. First declaration appeared at {1}.", null,
  DefaultNameMain, ErrorReporter.TokenToString(mainMethod.tok));
  hasMain = false;
  }
@@ -1670,7 +1670,7 @@ public static bool HasMain(Program program, out Method mainMethod) {
 
  if (hasMain) {
  if (!IsPermittedAsMain(program, mainMethod, out string reason)) {
- ReportError(program.Reporter, mainMethod.tok, "This method \"Main\" is not permitted as a main method ({0}).", null, reason);
+ ReportError(program.Reporter, mainMethod.tok, "This method 'Main' is not permitted as a main method ({0}).", null, reason);
  return false;
  } else {
  return true;
@@ -3220,7 +3220,7 @@ protected internal void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSy
  var s0 = (AssignStmt)s.S0;
  if (s0.Rhs is HavocRhs) {
  if (DafnyOptions.O.ForbidNondeterminism) {
- Error(s0.Rhs.Tok, "nondeterministic assignment forbidden by the --enforce-determinism option", wr);
+ Error(s0.Rhs.Tok, "nondeterministic assignment forbidden by --enforce-determinism", wr);
  }
  // The forall statement says to havoc a bunch of things. This can be efficiently compiled
  // into doing nothing.
@@ -5125,22 +5125,19 @@ private ConcreteSyntaxTree MaybeInjectSubsetConstraint(IVariable boundVar, Type
  IToken tok, ConcreteSyntaxTree wr, bool isReturning = false, bool elseReturnValue = false,
  bool isSubfiltering = false) {
  if (!boundVarType.Equals(collectionElementType, true) &&
- boundVarType.NormalizeExpand(true) is UserDefinedType
- {
+ boundVarType.NormalizeExpand(true) is UserDefinedType {
  TypeArgs: var typeArgs,
  ResolvedClass:
- SubsetTypeDecl
- {
+ SubsetTypeDecl {
  TypeArgs: var typeParametersArgs,
  Var: var variable,
  Constraint: var constraint
  }
  }) {
- if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType
- {
- ResolvedClass:
+ if (variable.Type.NormalizeExpandKeepConstraints() is UserDefinedType {
+ ResolvedClass:
  SubsetTypeDecl
-  } normalizedVariableType) {
+ } normalizedVariableType) {
  wr = MaybeInjectSubsetConstraint(boundVar, normalizedVariableType, collectionElementType,
  inLetExprBody, tok, wr, isReturning, elseReturnValue, true);
  }

docs/DafnyRef/Statements.md

@@ -928,7 +928,7 @@ has the same meaning as
 
 <!-- %no-check -->
 ```dafny
-if exists x :| P { var x :| P; S } else { T }
+if exists x :: P { var x :| P; S } else { T }
 ```
 
 The identifiers bound by ``BindingGuard`` are ghost variables

docs/DafnyRef/Types.md

@@ -715,7 +715,7 @@ type parameter `A` is declared to be restricted to auto-init types,
 the program does not need to explicitly assign any value to the
 out-parameter `a`.
 
-### 8.1.3. Nonempty types: `T(00)`
+### 8.1.3. Nonempty types: `T(00)` {#sec-nonempty-types}
 
 Auto-init types are important in compiled contexts. In ghost contexts, it
 may still be important to know that a type is nonempty. Dafny supports

docs/HowToFAQ/Errors-CommandLine.md

@@ -5,7 +5,8 @@
 
 ## Error: Invalid argument _argument_ to option _option_
 
-```bash <!-- %check-error -->
+<!-- %check-cli -->
+```bash 
 dafny resolve --function-syntax:2 mod.dfy
 ```
 
@@ -17,7 +18,8 @@ in the help document (`dafny -?` or `dafny <command> -h`).
 
 ## Error: Invalid argument _argument_ to option --quantifier-syntax
 
-```bash <!-- %check-error -->
+<!-- %check-cli -->
+```bash 
 dafny resolve --quantifier-syntax:2 null.dfy
 ```