Add beginner mode

build.sbt

@@ -18,7 +18,7 @@ lazy val server = (project in file("."))
         // General settings
         name := "ViperServer",
         organization := "viper",
-        version := "3.0.0", // has to be a proper semver
+        version := "3.1.0", // has to be a proper semver
 
         // Fork test to a different JVM than SBT's, avoiding SBT's classpath interfering with
         // classpath used by Scala's reflection.

src/main/scala/viper/server/ViperConfig.scala

@@ -53,6 +53,13 @@ class ViperConfig(args: Seq[String]) extends ScallopConf(args) {
     hidden = false
   )
 
+  val beginnerMode: ScallopOption[Boolean] = opt[Boolean]("beginnerMode",
+    descr = "Enables beginner mode, which disables some advanced features that can be confusing for new users.",
+    default = Some(false),
+    noshort = true,
+    hidden = false
+  )
+
   val SERVER_MODE_LSP = "LSP"
   val SERVER_MODE_HTTP = "HTTP"
   private val server_modes = Array(SERVER_MODE_LSP, SERVER_MODE_HTTP)

src/main/scala/viper/server/frontends/lsp/Receiver.scala

@@ -90,8 +90,8 @@ trait LanguageReceiver extends StandardReceiver with LanguageServer {
     capabilities.setCodeActionProvider(true)
     // Document Color:          [N/A]
     // Color Presentation:      [N/A]
-    // Formatting:              TODO
-    // capabilities.setDocumentFormattingProvider(true)
+    // Formatting:              TODO?
+    capabilities.setDocumentFormattingProvider(true)
     // Range Formatting:        TODO
     // On type Formatting:      [N/A]
     // Rename & Prepare Rename:
@@ -103,8 +103,6 @@ trait LanguageReceiver extends StandardReceiver with LanguageServer {
     // automatically cause all references to be renamed. This would probably be too annoying.
     capabilities.setLinkedEditingRangeProvider(false)
 
-    capabilities.setDocumentFormattingProvider(true)
-
     CompletableFuture.completedFuture(new InitializeResult(capabilities))
   }
 

src/main/scala/viper/server/frontends/lsp/ast/ParseAstLsp.scala

@@ -64,8 +64,8 @@ object HasFoldingRanges {
 }
 
 object HasInlayHints {
-  def apply(p: PProgram): Seq[InlayHint] = p.deepCollect({
-    case n: PCall => PLspCall.getInlayHints(n)
+  def apply(p: PProgram, beginnerMode: Boolean): Seq[InlayHint] = p.deepCollect({
+    case n: PCall if !beginnerMode => PLspCall.getInlayHints(n)
     case n: PLet => PLspLet.getInlayHints(n)
   }).flatten
 }

src/main/scala/viper/server/frontends/lsp/file/RelayActor.scala

@@ -129,13 +129,14 @@ class RelayActor(task: MessageHandler, backendClassName: Option[String]) extends
         task.resetContainers(true)
         task.lastPhase = Some(phase)
 
+        val beginnerMode = coordinator.server.config.beginnerMode()
         task.addCodeLens(true)(HasCodeLens(pProgram))
         task.addDocumentSymbol(true)(HasDocumentSymbol(pProgram).toSeq)
         task.addHoverHint(true)(HasHoverHints(pProgram))
         task.addGotoDefinition(true)(HasGotoDefinitions(pProgram))
         task.addFindReferences(true)(HasReferenceTos(pProgram))
         task.addFoldingRange(true)(HasFoldingRanges(pProgram))
-        task.addInlayHint(true)(HasInlayHints(pProgram))
+        task.addInlayHint(true)(HasInlayHints(pProgram, beginnerMode))
         task.addSemanticHighlight(true)(HasSemanticHighlights(pProgram))
         task.addSignatureHelp(true)(HasSignatureHelps(pProgram))
         task.addSuggestionScopeRange(true)(HasSuggestionScopeRanges(pProgram))