From bf2bc9f4146a68be2ad4d82ad31171f18639c4bb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Mon, 12 Feb 2024 20:34:48 +0100 Subject: [PATCH] More cleanup --- .../frontends/lsp/file/FileContent.scala | 15 - .../server/frontends/lsp/file/Manager.scala | 26 +- .../lsp/file/utility/Containers.scala | 220 ---------- .../lsp/file/utility/ContainersBackup.scala | 386 ------------------ .../lsp/file/utility/Conversions.scala | 1 - 5 files changed, 3 insertions(+), 645 deletions(-) delete mode 100644 src/main/scala/viper/server/frontends/lsp/file/utility/ContainersBackup.scala diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala index d2cac71..481c793 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileContent.scala @@ -30,25 +30,12 @@ case class FileContent(path: Path) extends DiskLoader { } val fileContent = new ArrayBuffer[String] - // val lineToChar = new ArrayBuffer[Int] def set(newContent: String): Unit = { fileContent.clear() fileContent.addAll(newContent.split("\n", -1)) - // var idx = 0 - // fileContent.foreach(line => { - // lineToChar.addOne(idx) - // idx += line.length + 1 - // }) } - // def rpToCharRange(rp: RangePosition): CharRange = { - // CharRange( - // lineToChar(rp.start.line) + rp.start.column, - // lineToChar(rp._end.line) + rp._end.column, - // ) - // } - override def loadContent(path: Path): Try[String] = if (this.path == path) Success(fileContent.mkString("\n")) else super.loadContent(path) @@ -95,13 +82,11 @@ case class FileContent(path: Path) extends DiskLoader { normalize(pos).flatMap(nPos => { val start = iterBackward(nPos).drop(1).takeWhile { case (c, _) => Common.isIdentChar(c) }.length val startPos = new Position(nPos.getLine, nPos.getCharacter - start) - // println("startPos: " + startPos.toString() + " " + nPos.toString()) if (!Common.isIdentStartChar(getCharAt(startPos))) return None val end = iterForward(nPos).takeWhile { case (c, _) => Common.isIdentChar(c) }.length val endPos = new Position(nPos.getLine, nPos.getCharacter + end) if (start == 0 && end == 0 || inComment(nPos)) None else { val ident = fileContent(nPos.getLine).slice(startPos.getCharacter, endPos.getCharacter) - // println("got: " + ident) Some((ident, new Range(startPos, endPos))) } }) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala index b0f26b8..5aadd64 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala @@ -6,39 +6,19 @@ package viper.server.frontends.lsp.file -import java.net.URI -import java.nio.file.{Path, Paths} -import akka.actor.{Actor, Props, Status} -import org.eclipse.lsp4j.{Diagnostic, DiagnosticSeverity, DocumentSymbol, FoldingRange, Position, PublishDiagnosticsParams, Range, SymbolKind} -import viper.server.core.VerificationExecutionContext +import java.nio.file.Path +import org.eclipse.lsp4j.{PublishDiagnosticsParams, Range} import viper.server.frontends.lsp.ClientCoordinator -import viper.server.frontends.lsp.VerificationState._ -import viper.server.frontends.lsp.VerificationSuccess._ -import viper.server.vsi.VerJobId -import viper.silver.ast -import viper.silver.ast.{AbstractSourcePosition, HasLineColumn} -import viper.silver.reporter._ -import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage} import scala.jdk.CollectionConverters._ -import scala.collection.mutable.{ArrayBuffer, HashMap} -import scala.concurrent.Future -import org.eclipse.lsp4j.ParameterInformation -import org.eclipse.lsp4j.jsonrpc.messages.Tuple.Two -import viper.server.vsi.AstJobId +import scala.collection.mutable.ArrayBuffer import viper.server.frontends.lsp.file.FileContent -import viper.server.frontends.lsp.file.ProgressCoordinator import viper.server.frontends.lsp.Lsp4jSemanticHighlight import VerificationPhase._ import org.eclipse.lsp4j import viper.silver.ast.utility.lsp -import viper.server.frontends.lsp.file.utility.LspContainer -import ch.qos.logback.classic.Logger -import viper.server.frontends.lsp.file.utility.StageContainer -import viper.silver.ast.utility.lsp.GotoDefinition import viper.server.frontends.lsp.Common -import viper.silver.ast.utility.lsp.DocumentSymbol case class Diagnostic(backendClassName: Option[String], position: lsp.RangePosition, message: String, severity: lsp4j.DiagnosticSeverity, cached: Boolean, errorMsgPrefix: Option[String]) extends lsp.HasRangePositions with lsp.BelongsToFile { override def rangePositions: Seq[lsp.RangePosition] = Seq(position) diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala index 6ba57a7..0ad54a3 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala @@ -15,12 +15,7 @@ import ch.qos.logback.classic.Logger import scala.collection.mutable.HashMap import viper.silver.ast.utility.lsp import viper.silver.ast.utility.lsp.SelectionBoundScopeTrait -import viper.silver.ast.utility.lsp.SelectionBoundScope -import viper.silver.ast.utility.lsp.SelectionBoundBoth -import viper.silver.ast.utility.lsp.SelectionBoundKeyword -import viper.silver.ast.utility.lsp.SelectionBound import viper.silver.ast.utility.lsp.SelectionBoundKeywordTrait -import viper.server.frontends.lsp.file.VerificationPhase._ trait StageContainer[K, V, I] { var resetCount: Int = 0 @@ -38,9 +33,6 @@ trait StageContainer[K, V, I] { def all(): Iterator[V] def filterInPlace(p: V => Boolean): Unit } -// trait StageProjectContainer[K, V] extends StageContainer[K, V] { -// def get(uri: String, k: K): Seq[V] -// } case class StageArrayContainer[V]() extends StageContainer[Unit, V, Int] { private val array: ArrayBuffer[V] = ArrayBuffer() @@ -57,25 +49,11 @@ case class StageArrayContainer[V]() extends StageContainer[Unit, V, Int] { override def all(): Iterator[V] = array.iterator def filterInPlace(p: V => Boolean): Unit = array.filterInPlace(p) } -// case class StageArrayContainer[V]() extends StageArrayContainerTrait[V] object StageArrayContainer { type ArrayContainer[V <: HasRangePositions with BelongsToFile, U] = LspContainer[StageArrayContainer[V], Unit, V, Int, U] implicit def default[V]: () => StageArrayContainer[V] = () => StageArrayContainer() } -// case class StageArrayProjectContainer[V <: BelongsToFile](uriToStage: String => StageArrayContainer[V])(implicit root: String) extends StageArrayContainerTrait[V] { -// override def add(v: V): Unit = { -// val uri = v.file.toUri().toString() -// if (uri == root) super.add(v) else uriToStage(uri).add(v) -// } -// override def get(uri: String, k: Unit): Seq[V] = if (uri == root) super.get(uri, k) else uriToStage(uri).get(uri, k) -// } -// object StageArrayProjectContainer { -// type ArrayProjectContainer[V <: HasRangePositions with BelongsToFile, U, T <: Translates[V, U, Unit]] = LspProjectContainer[StageArrayProjectContainer[V], Unit, V, U, T] - -// def default[V <: BelongsToFile](uriToStage: String => StageArrayContainer[V])(implicit root: String): StageArrayProjectContainer[V] = StageArrayProjectContainer[V](uriToStage) -// } - case class StageRangeContainer[V <: SelectableInBound]() extends StageContainer[(Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean), V, (Option[String], Int)] { // Has a `scope` bound val localKeyword: HashMap[String, ArrayBuffer[V]] = HashMap() @@ -129,7 +107,6 @@ case class StageRangeContainer[V <: SelectableInBound]() extends StageContainer[ localKeyword.filterInPlace((_, g) => g.nonEmpty) } } -// case class StageRangeContainer[V <: SelectableInBound[_, SelectionBoundScopeTrait]]() extends StageRangeContainerTrait[V] object StageRangeContainer { type RangeContainer[V <: HasRangePositions with SelectableInBound, U] = LspContainer[StageRangeContainer[V], (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean), V, (Option[String], Int), U] implicit def default[V <: SelectableInBound]: () => StageRangeContainer[V] = () => StageRangeContainer() @@ -192,73 +169,11 @@ case class StageSuggestableContainer[V <: lsp.SuggestableInBound]() extends Stag perScope.filterInPlace((_, g) => g.nonEmpty) } } -// case class StageRangeContainer[V <: SelectableInBound[_, SelectionBoundScopeTrait]]() extends StageRangeContainerTrait[V] object StageSuggestableContainer { type SuggestableContainer[V <: HasRangePositions with lsp.SuggestableInBound, U] = LspContainer[StageSuggestableContainer[V], (lsp.SuggestionScope, Option[lsp4j.Position], Char), V, Map[Option[lsp.SuggestionScope], Int], U] implicit def default[V <: lsp.SuggestableInBound]: () => StageSuggestableContainer[V] = () => StageSuggestableContainer() } -// case class StageRangeProjectContainer[V <: SelectableInBound[V, SelectionBoundTrait]](uriToStage: String => StageRangeContainer[SelectableInBound[V, SelectionBoundScopeTrait]])(implicit root: String) extends StageRangeContainerTrait[SelectableInBound[V, SelectionBoundScopeTrait]] { -// // No `scope` bound -// val globalKeyword: HashMap[String, ArrayBuffer[V]] = HashMap() -// val global: ArrayBuffer[V] = ArrayBuffer() - -// override def reset(): Unit = { -// super.reset() -// globalKeyword.clear() -// global.clear() -// } -// override def add(v: V): Unit = v.selectableInScope match { -// case Some(u) => { -// val uri = u.bound.scope.file.toUri().toString() -// if (uri == root) super.add(u) else uriToStage(uri).add(u) -// } -// case None => v.bound match { -// case bound: SelectionBoundKeywordTrait => -// globalKeyword.getOrElseUpdate(bound.keyword, ArrayBuffer()).addOne(v) -// case _ => global.addOne(v) -// } -// } -// override def get(k: (Option[lsp4j.Position], Option[(String, lsp4j.Range)])): Seq[V] = { -// val local = if (uri == root) super.get(uri, k) else uriToStage(uri).get(uri, k) -// global.toSeq ++ globalKeyword.get(k._1).toSeq.flatten ++ local.map(_.get) -// } -// override def all(): Iterator[V] = -// super.all().map(_.get) ++ global.iterator ++ globalKeyword.values.flatten -// override def filterInPlace(p: V => Boolean): Unit = { -// super.filterInPlace(v => p(v.get)) -// global.filterInPlace(p) -// globalKeyword.values.foreach(_.filterInPlace(p)) -// globalKeyword.filterInPlace((_, g) => g.nonEmpty) -// } -// } -// object StageRangeProjectContainer { -// type RangeProjectContainer[V <: HasRangePositions with SelectableInBound[V, SelectionBoundTrait], U] = LspContainer[StageRangeProjectContainer[V], (Option[lsp4j.Position], Option[(String, lsp4j.Range)]), V, U] - -// def default[V <: SelectableInBound[V, SelectionBoundTrait]](uriToStage: String => StageRangeContainer[SelectableInBound[V, SelectionBoundScopeTrait]])(implicit root: String): StageRangeProjectContainer[V] = StageRangeProjectContainer[V](uriToStage) -// } - -// case class RangeSelector[T <: SelectableInBound]( -// localKeyword: HashMap[String, ArrayBuffer[T]] = HashMap[String, ArrayBuffer[T]](), -// localPosition: ArrayBuffer[T] = ArrayBuffer[T](), -// globalKeyword: HashMap[String, ArrayBuffer[T]] = HashMap[String, ArrayBuffer[T]](), -// ) { -// def getGlobal(ident: String): Seq[T] = { -// globalKeyword.get(ident).toSeq.flatMap(_.toSeq) -// } -// def getLocalForPos(ident: String, pos: lsp4j.Position): Seq[T] = { -// // println("Checking for local pos: " + pos.toString() + " in " + localPosition.toString()) -// localKeyword.get(ident).toSeq.flatMap(_.filter(inLocalPos(pos)).toSeq) ++ -// localPosition.filter(inLocalPos(pos)).toSeq -// } -// def inLocalPos(pos: lsp4j.Position)(h: T): Boolean = { -// val range = Common.toRange(h.bound.scope.get) -// Common.comparePosition(range.getStart(), pos) <= 0 && -// Common.comparePosition(range.getEnd(), pos) >= 0 -// } -// // def setLocal -// } - case class LspContainer[+C <: StageContainer[K, V, I], K, V <: HasRangePositions, I, U] (translator: Translates[V, U, K], onUpdate: () => Unit = () => {}, expandOnBorder: Boolean = false)(implicit initial: () => C) { private val parseTypeck: C = initial() @@ -316,15 +231,12 @@ case class LspContainer[+C <: StageContainer[K, V, I], K, V <: HasRangePositions } for (buffer <- Seq(parseTypeck, verify)) buffer.filterInPlace(v => { - // println("Updating pos for " + v.toString) val positions = v.rangePositions var overlapped = false for (pos <- positions if !pos.modified && !overlapped) { pos.modified = true val pRange = Common.toRange(pos) val cmp = Common.compareRange(pRange, range) - // println("PRange: " + pRange.toString() + " Range: " + range.toString()) - // println("Cmp: " + cmp) cmp match { case -4 => case -3 | -2 => @@ -347,139 +259,7 @@ case class LspContainer[+C <: StageContainer[K, V, I], K, V <: HasRangePositions case _ => } } - // if (overlapped) println("overlapped: " + v.toString()) !overlapped }) } } - -// case class LspProjectContainer[C <: StageProjectContainer[K, V], K, V <: HasRangePositions, U, T <: Translates[V, U, K]] -// (containerInFile: String => LspContainer[C, K, V], onUpdate: () => Unit = () => {}) -// (implicit initial: (String => StageContainer[K, V]) => C, implicit val translator: T) extends LspContainerTrait[C, K, V] { -// override val parse: C = initial(containerInFile(_).parse) -// override val typeck: C = initial(containerInFile(_).typeck) -// override val verify: C = initial(containerInFile(_).verify) - -// def resetAll() = { -// resetParse(false) -// resetTypeck(false) -// resetVerify(false) -// onUpdate() -// } -// def resetParse(doUpdate: Boolean = true) = { -// parse.reset() -// if (doUpdate) onUpdate() -// } -// def resetTypeck(doUpdate: Boolean = true) = { -// typeck.reset() -// if (doUpdate) onUpdate() -// } -// def resetVerify(doUpdate: Boolean = true) = { -// verify.reset() -// if (doUpdate) onUpdate() -// } - -// // private def addToFile[N <: V with BelongsToFile](v: N, uriToStage: String => StageContainer[K, V]) = { -// // val uri = v.file.toUri().toString() -// // uriToStage(uri).add(v) -// // } - -// def receiveParse(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveParse(_, false)) -// if (doUpdate) onUpdate() -// } -// def receiveTypeck(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveTypeck(_, false)) -// if (doUpdate) onUpdate() -// } -// def receiveVerify(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveVerify(_, false)) -// if (doUpdate) onUpdate() -// } - -// def receiveParse(p: V, doUpdate: Boolean): Unit = { -// this.parse.add(p) -// if (doUpdate) onUpdate() -// } -// def receiveTypeck(t: V, doUpdate: Boolean): Unit = { -// this.typeck.add(t) -// if (doUpdate) onUpdate() -// } -// def receiveVerify(v: V, doUpdate: Boolean): Unit = { -// this.verify.add(v) -// if (doUpdate) onUpdate() -// } - -// def get(uri: String, k: K)(implicit log: Logger): Seq[U] = translator.translate(Seq(parse.get(uri, k), typeck.get(uri, k), verify.get(uri, k)).flatten)(k) - -// /** If a range position is aliased, we do not want to update it twice */ -// def resetModifiedFlag(): Unit = { -// parse.all().foreach(_.rangePositions.foreach(_.modified = false)) -// typeck.all().foreach(_.rangePositions.foreach(_.modified = false)) -// verify.all().foreach(_.rangePositions.foreach(_.modified = false)) -// } -// /** -// * Update the positions of semantic tokens after a change in the file -// * -// * @param range Replaced (deleted) range -// * @param text Newly inserted (added) text -// */ -// def updatePositions(range: lsp4j.Range, text: String): Unit = { -// val lines = text.split("\n", -1) -// val deltaLines = lines.length - 1 + range.getStart.getLine - range.getEnd.getLine -// val startCharacter = if (lines.length == 1) range.getStart.getCharacter else 0 -// val deltaChars = startCharacter + lines.last.length - range.getEnd.getCharacter -// val endLine = range.getEnd.getLine - -// // TODO: -// // If the change cannot ruin the meaning of a semantic token at the start, -// // adjust the range start to avoid overlaps with adjacent tokens -// // if (text.isEmpty || !text.head.isLetterOrDigit) { -// // range.getStart.setCharacter(range.getStart.getCharacter + 1) -// // } -// // If the change cannot ruin the meaning of a semantic token at the end, -// // adjust the range end to avoid overlaps with adjacent tokens -// // if (text.isEmpty || !text.last.isLetterOrDigit) { -// // range.getEnd.setCharacter(range.getEnd.getCharacter - 1) -// // } -// // Remove overlapping semantic tokens and update positions of those after change -// def shiftEnd(pos: RangePosition, end: lsp4j.Position): Unit = { -// if (end.getLine == endLine) pos.shiftEnd(deltaLines, deltaChars) -// else pos.shiftEnd(deltaLines, 0) -// } -// def shiftStart(pos: RangePosition, start: lsp4j.Position): Unit = { -// if (start.getLine == endLine) pos.shiftStart(deltaLines, deltaChars) -// else pos.shiftStart(deltaLines, 0) -// } - -// for (buffer <- Seq(parse, typeck, verify)) buffer.filterInPlace(v => { -// val positions = v.rangePositions -// var overlapped = false -// for (pos <- positions if !pos.modified && !overlapped) { -// pos.modified = true -// val start = Common.toPosition(pos.start) -// val end = Common.toPosition(pos._end) -// Common.containsPos(range, start) match { -// // `start` < `range.start` -// case neg if neg < 0 => Common.containsPos(range, end) match { -// // `end` < `range.start` -// case neg if neg < 0 => {} -// // `end` within `range` -// case 0 => overlapped = true -// // `end` > `range.end` -// case _ => shiftEnd(pos, end) -// } -// // `start` within `range` -// case 0 => overlapped = true -// // `start` > `range.end` -// case _ => { -// shiftStart(pos, start) -// shiftEnd(pos, end) -// } -// } -// } -// if (overlapped) println("overlapped: " + v.toString()) -// !overlapped -// }) -// } -// } diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/ContainersBackup.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/ContainersBackup.scala deleted file mode 100644 index 91edf7d..0000000 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/ContainersBackup.scala +++ /dev/null @@ -1,386 +0,0 @@ -// // This Source Code Form is subject to the terms of the Mozilla Public -// // License, v. 2.0. If a copy of the MPL was not distributed with this -// // file, You can obtain one at http://mozilla.org/MPL/2.0/. -// // -// // Copyright (c) 2023 ETH Zurich. - -// package viper.server.frontends.lsp.file.utility - -// import org.eclipse.lsp4j - -// import scala.collection.mutable.ArrayBuffer -// import viper.silver.ast.utility.lsp.{BelongsToFile, HasRangePositions, RangePosition, SelectableInBound} -// import viper.server.frontends.lsp.Common -// import ch.qos.logback.classic.Logger -// import scala.collection.mutable.HashMap -// import viper.silver.ast.utility.lsp.SelectionBoundTrait - -// trait StageContainerSimple[K, V] { -// def reset(): Unit -// def add(v: V): Unit -// def get(k: K): Seq[V] -// def all(): Iterator[V] -// def filterInPlace(p: V => Boolean): Unit -// } - -// trait StageContainer[K, V] { -// def reset(): Unit -// def add(v: V): Unit -// def get(uri: String, k: K): Seq[V] -// def all(): Iterator[V] -// def filterInPlace(p: V => Boolean): Unit -// } - -// case class ArrayStageContainer[V <: BelongsToFile](uriToStage: String => ArrayStageContainer[V]) extends StageContainer[Unit, V] { -// val array: ArrayBuffer[V] = ArrayBuffer() -// override def reset(): Unit = array.clear() -// override def add(v: V): Unit = { -// val uri = v.file.toUri().toString() -// uriToStage(uri).array.addOne(v) -// } -// override def get(uri: String, k: Unit): Seq[V] = uriToStage(uri).array.toSeq -// override def all(): Iterator[V] = array.iterator -// def filterInPlace(p: V => Boolean): Unit = array.filterInPlace(p) -// } -// object ArrayStageContainer { -// type ArrayContainer[V <: HasRangePositions with BelongsToFile, U, T <: Translates[V, U, Unit]] = LspContainer[ArrayStageContainer[V], Unit, V, U, T] - -// def default[V <: BelongsToFile](uriToStage: String => ArrayStageContainer[V]): ArrayStageContainer[V] = ArrayStageContainer[V](uriToStage) -// } - -// case class RangeSelectContainer[V <: SelectableInBound](uriToStage: String => RangeSelectContainer[V]) extends StageContainer[(String, lsp4j.Position, lsp4j.Range), V] { -// // type Key = (String, lsp4j.Position, lsp4j.Range) - -// // Has a `scope` bound -// val localKeyword: HashMap[String, ArrayBuffer[(lsp4j.Range, V)]] = HashMap() -// val local: ArrayBuffer[(lsp4j.Range, V)] = ArrayBuffer() -// // No `scope` bound -// val globalKeyword: HashMap[String, ArrayBuffer[V]] = HashMap() -// val global: ArrayBuffer[V] = ArrayBuffer() - -// override def reset(): Unit = { -// localKeyword.clear() -// local.clear() -// globalKeyword.clear() -// global.clear() -// } -// override def add(v: V): Unit = v.bound match { -// case SelectionBoundTrait(k, Some(scope)) => { -// val stage = uriToStage(scope.file.toUri().toString()) -// val range = Common.toRange(scope) -// k match { -// case Some(keyword) => stage.localKeyword.getOrElseUpdate(keyword, ArrayBuffer()).addOne((range, v)) -// case None => stage.local.addOne((range, v)) -// } -// } -// case SelectionBoundTrait(Some(keyword), None) => -// globalKeyword.getOrElseUpdate(keyword, ArrayBuffer()).addOne(v) -// case SelectionBoundTrait(None, None) => global.addOne(v) -// } -// override def get(uri: String, k: (String, lsp4j.Position, lsp4j.Range)): Seq[V] = { -// val (keyword, position, _) = k -// val stage = uriToStage(uri) -// val localAll = stage.local.iterator ++ stage.localKeyword.get(keyword).iterator.flatten -// val local = localAll.filter(h => Common.containsPos(h._1, position) == 0) -// global.toSeq ++ globalKeyword.get(keyword).toSeq.flatten ++ local.map(_._2).toSeq -// } -// override def all(): Iterator[V] = -// global.iterator ++ globalKeyword.values.flatten ++ -// local.iterator.map(_._2) ++ localKeyword.values.flatten.map(_._2) -// override def filterInPlace(p: V => Boolean): Unit = { -// global.filterInPlace(p) -// globalKeyword.values.foreach(_.filterInPlace(p)) -// globalKeyword.filterInPlace((_, g) => g.nonEmpty) -// local.filterInPlace(l => p(l._2)) -// localKeyword.values.foreach(_.filterInPlace(l => p(l._2))) -// localKeyword.filterInPlace((_, g) => g.nonEmpty) -// } -// } -// object RangeSelectContainer { -// type RangeContainer[V <: HasRangePositions with SelectableInBound, U, T <: Translates[V, U, (String, lsp4j.Position, lsp4j.Range)]] = LspContainer[RangeSelectContainer[V], (String, lsp4j.Position, lsp4j.Range), V, U, T] - -// def default[V <: SelectableInBound](uriToStage: String => RangeSelectContainer[V]): RangeSelectContainer[V] = RangeSelectContainer[V](uriToStage) -// } - -// // case class RangeSelector[T <: SelectableInBound]( -// // localKeyword: HashMap[String, ArrayBuffer[T]] = HashMap[String, ArrayBuffer[T]](), -// // localPosition: ArrayBuffer[T] = ArrayBuffer[T](), -// // globalKeyword: HashMap[String, ArrayBuffer[T]] = HashMap[String, ArrayBuffer[T]](), -// // ) { -// // def getGlobal(ident: String): Seq[T] = { -// // globalKeyword.get(ident).toSeq.flatMap(_.toSeq) -// // } -// // def getLocalForPos(ident: String, pos: lsp4j.Position): Seq[T] = { -// // // println("Checking for local pos: " + pos.toString() + " in " + localPosition.toString()) -// // localKeyword.get(ident).toSeq.flatMap(_.filter(inLocalPos(pos)).toSeq) ++ -// // localPosition.filter(inLocalPos(pos)).toSeq -// // } -// // def inLocalPos(pos: lsp4j.Position)(h: T): Boolean = { -// // val range = Common.toRange(h.bound.scope.get) -// // Common.comparePosition(range.getStart(), pos) <= 0 && -// // Common.comparePosition(range.getEnd(), pos) >= 0 -// // } -// // // def setLocal -// // } - -// case class LspSimpleContainer[C <: StageContainer[K, V], K, V <: HasRangePositions, U, T <: Translates[V, U, K]] -// (onUpdate: () => Unit = () => {}) -// (implicit initial: (String => C) => C, implicit val translator: T) { -// private val parse: C = initial(containerInFile(_).parse) -// private val typeck: C = initial(containerInFile(_).typeck) -// private val verify: C = initial(containerInFile(_).verify) - -// def resetAll() = { -// resetParse(false) -// resetTypeck(false) -// resetVerify(false) -// onUpdate() -// } -// def resetParse(doUpdate: Boolean = true) = { -// parse.reset() -// if (doUpdate) onUpdate() -// } -// def resetTypeck(doUpdate: Boolean = true) = { -// typeck.reset() -// if (doUpdate) onUpdate() -// } -// def resetVerify(doUpdate: Boolean = true) = { -// verify.reset() -// if (doUpdate) onUpdate() -// } - -// // private def addToFile[N <: V with BelongsToFile](v: N, uriToStage: String => StageContainer[K, V]) = { -// // val uri = v.file.toUri().toString() -// // uriToStage(uri).add(v) -// // } - -// def receiveParse(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveParse(_, false)) -// if (doUpdate) onUpdate() -// } -// def receiveTypeck(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveTypeck(_, false)) -// if (doUpdate) onUpdate() -// } -// def receiveVerify(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveVerify(_, false)) -// if (doUpdate) onUpdate() -// } - -// def receiveParse(p: V, doUpdate: Boolean): Unit = { -// this.parse.add(p) -// if (doUpdate) onUpdate() -// } -// def receiveTypeck(t: V, doUpdate: Boolean): Unit = { -// this.typeck.add(t) -// if (doUpdate) onUpdate() -// } -// def receiveVerify(v: V, doUpdate: Boolean): Unit = { -// this.verify.add(v) -// if (doUpdate) onUpdate() -// } - -// def get(uri: String, k: K)(implicit log: Logger): Seq[U] = translator.translate(Seq(parse.get(uri, k), typeck.get(uri, k), verify.get(uri, k)).flatten)(k) - -// /** If a range position is aliased, we do not want to update it twice */ -// def resetModifiedFlag(): Unit = { -// parse.all().foreach(_.rangePositions.foreach(_.modified = false)) -// typeck.all().foreach(_.rangePositions.foreach(_.modified = false)) -// verify.all().foreach(_.rangePositions.foreach(_.modified = false)) -// } -// /** -// * Update the positions of semantic tokens after a change in the file -// * -// * @param range Replaced (deleted) range -// * @param text Newly inserted (added) text -// */ -// def updatePositions(range: lsp4j.Range, text: String): Unit = { -// val lines = text.split("\n", -1) -// val deltaLines = lines.length - 1 + range.getStart.getLine - range.getEnd.getLine -// val startCharacter = if (lines.length == 1) range.getStart.getCharacter else 0 -// val deltaChars = startCharacter + lines.last.length - range.getEnd.getCharacter -// val endLine = range.getEnd.getLine - -// // TODO: -// // If the change cannot ruin the meaning of a semantic token at the start, -// // adjust the range start to avoid overlaps with adjacent tokens -// // if (text.isEmpty || !text.head.isLetterOrDigit) { -// // range.getStart.setCharacter(range.getStart.getCharacter + 1) -// // } -// // If the change cannot ruin the meaning of a semantic token at the end, -// // adjust the range end to avoid overlaps with adjacent tokens -// // if (text.isEmpty || !text.last.isLetterOrDigit) { -// // range.getEnd.setCharacter(range.getEnd.getCharacter - 1) -// // } -// // Remove overlapping semantic tokens and update positions of those after change -// def shiftEnd(pos: RangePosition, end: lsp4j.Position): Unit = { -// if (end.getLine == endLine) pos.shiftEnd(deltaLines, deltaChars) -// else pos.shiftEnd(deltaLines, 0) -// } -// def shiftStart(pos: RangePosition, start: lsp4j.Position): Unit = { -// if (start.getLine == endLine) pos.shiftStart(deltaLines, deltaChars) -// else pos.shiftStart(deltaLines, 0) -// } - -// for (buffer <- Seq(parse, typeck, verify)) buffer.filterInPlace(v => { -// val positions = v.rangePositions -// var overlapped = false -// for (pos <- positions if !pos.modified && !overlapped) { -// pos.modified = true -// val start = Common.toPosition(pos.start) -// val end = Common.toPosition(pos._end) -// Common.containsPos(range, start) match { -// // `start` < `range.start` -// case neg if neg < 0 => Common.containsPos(range, end) match { -// // `end` < `range.start` -// case neg if neg < 0 => {} -// // `end` within `range` -// case 0 => overlapped = true -// // `end` > `range.end` -// case _ => shiftEnd(pos, end) -// } -// // `start` within `range` -// case 0 => overlapped = true -// // `start` > `range.end` -// case _ => { -// shiftStart(pos, start) -// shiftEnd(pos, end) -// } -// } -// } -// if (overlapped) println("overlapped: " + v.toString()) -// !overlapped -// }) -// } -// } - -// case class LspContainer[C <: StageContainer[K, V], K, V <: HasRangePositions, U, T <: Translates[V, U, K]] -// (containerInFile: String => LspContainer[C, K, V, U, T], onUpdate: () => Unit = () => {}) -// (implicit initial: (String => C) => C, implicit val translator: T) { -// private val parse: C = initial(containerInFile(_).parse) -// private val typeck: C = initial(containerInFile(_).typeck) -// private val verify: C = initial(containerInFile(_).verify) - -// def resetAll() = { -// resetParse(false) -// resetTypeck(false) -// resetVerify(false) -// onUpdate() -// } -// def resetParse(doUpdate: Boolean = true) = { -// parse.reset() -// if (doUpdate) onUpdate() -// } -// def resetTypeck(doUpdate: Boolean = true) = { -// typeck.reset() -// if (doUpdate) onUpdate() -// } -// def resetVerify(doUpdate: Boolean = true) = { -// verify.reset() -// if (doUpdate) onUpdate() -// } - -// // private def addToFile[N <: V with BelongsToFile](v: N, uriToStage: String => StageContainer[K, V]) = { -// // val uri = v.file.toUri().toString() -// // uriToStage(uri).add(v) -// // } - -// def receiveParse(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveParse(_, false)) -// if (doUpdate) onUpdate() -// } -// def receiveTypeck(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveTypeck(_, false)) -// if (doUpdate) onUpdate() -// } -// def receiveVerify(ps: Seq[V], doUpdate: Boolean = true): Unit = { -// ps.foreach(receiveVerify(_, false)) -// if (doUpdate) onUpdate() -// } - -// def receiveParse(p: V, doUpdate: Boolean): Unit = { -// this.parse.add(p) -// if (doUpdate) onUpdate() -// } -// def receiveTypeck(t: V, doUpdate: Boolean): Unit = { -// this.typeck.add(t) -// if (doUpdate) onUpdate() -// } -// def receiveVerify(v: V, doUpdate: Boolean): Unit = { -// this.verify.add(v) -// if (doUpdate) onUpdate() -// } - -// def get(uri: String, k: K)(implicit log: Logger): Seq[U] = translator.translate(Seq(parse.get(uri, k), typeck.get(uri, k), verify.get(uri, k)).flatten)(k) - -// /** If a range position is aliased, we do not want to update it twice */ -// def resetModifiedFlag(): Unit = { -// parse.all().foreach(_.rangePositions.foreach(_.modified = false)) -// typeck.all().foreach(_.rangePositions.foreach(_.modified = false)) -// verify.all().foreach(_.rangePositions.foreach(_.modified = false)) -// } -// /** -// * Update the positions of semantic tokens after a change in the file -// * -// * @param range Replaced (deleted) range -// * @param text Newly inserted (added) text -// */ -// def updatePositions(range: lsp4j.Range, text: String): Unit = { -// val lines = text.split("\n", -1) -// val deltaLines = lines.length - 1 + range.getStart.getLine - range.getEnd.getLine -// val startCharacter = if (lines.length == 1) range.getStart.getCharacter else 0 -// val deltaChars = startCharacter + lines.last.length - range.getEnd.getCharacter -// val endLine = range.getEnd.getLine - -// // TODO: -// // If the change cannot ruin the meaning of a semantic token at the start, -// // adjust the range start to avoid overlaps with adjacent tokens -// // if (text.isEmpty || !text.head.isLetterOrDigit) { -// // range.getStart.setCharacter(range.getStart.getCharacter + 1) -// // } -// // If the change cannot ruin the meaning of a semantic token at the end, -// // adjust the range end to avoid overlaps with adjacent tokens -// // if (text.isEmpty || !text.last.isLetterOrDigit) { -// // range.getEnd.setCharacter(range.getEnd.getCharacter - 1) -// // } -// // Remove overlapping semantic tokens and update positions of those after change -// def shiftEnd(pos: RangePosition, end: lsp4j.Position): Unit = { -// if (end.getLine == endLine) pos.shiftEnd(deltaLines, deltaChars) -// else pos.shiftEnd(deltaLines, 0) -// } -// def shiftStart(pos: RangePosition, start: lsp4j.Position): Unit = { -// if (start.getLine == endLine) pos.shiftStart(deltaLines, deltaChars) -// else pos.shiftStart(deltaLines, 0) -// } - -// for (buffer <- Seq(parse, typeck, verify)) buffer.filterInPlace(v => { -// val positions = v.rangePositions -// var overlapped = false -// for (pos <- positions if !pos.modified && !overlapped) { -// pos.modified = true -// val start = Common.toPosition(pos.start) -// val end = Common.toPosition(pos._end) -// Common.containsPos(range, start) match { -// // `start` < `range.start` -// case neg if neg < 0 => Common.containsPos(range, end) match { -// // `end` < `range.start` -// case neg if neg < 0 => {} -// // `end` within `range` -// case 0 => overlapped = true -// // `end` > `range.end` -// case _ => shiftEnd(pos, end) -// } -// // `start` within `range` -// case 0 => overlapped = true -// // `start` > `range.end` -// case _ => { -// shiftStart(pos, start) -// shiftEnd(pos, end) -// } -// } -// } -// if (overlapped) println("overlapped: " + v.toString()) -// !overlapped -// }) -// } -// } diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala index 56752e3..0d08711 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala @@ -15,7 +15,6 @@ import ch.qos.logback.classic.Logger import scala.jdk.CollectionConverters._ import scala.collection.mutable.ArrayBuffer -import viper.silver.ast.utility.lsp.DocumentSymbol trait Translates[-T, +U, I] { def translate(t: T)(i: I): U