search

JetBrains / Arend

The Arend Proof Assistant
https://arend-lang.github.io/
Apache License 2.0
694 stars 33 forks source link

StringIndexOutOfBoundsException #245

Closed ice1000 closed 4 years ago

ice1000 commented 4 years ago 
java.lang.StringIndexOutOfBoundsException: String index out of range: -1
    at java.base/java.lang.StringLatin1.charAt(StringLatin1.java:47)
    at java.base/java.lang.String.charAt(String.java:693)
    at org.arend.naming.renamer.Renamer.getPrefix(Renamer.java:155)
    at org.arend.naming.renamer.Renamer.generateFreshName(Renamer.java:122)
    at org.arend.naming.renamer.ReferableRenamer.generateFreshName(ReferableRenamer.java:29)
    at org.arend.naming.renamer.Renamer.generateFreshNames(Renamer.java:105)
    at org.arend.term.prettyprint.ToAbstractVisitor.convert(ToAbstractVisitor.java:71)
    at org.arend.core.expr.Expression.prettyPrint(Expression.java:85)
    at org.arend.ext.prettyprinting.doc.TermDoc.getString(TermDoc.java:26)
    at org.arend.ext.prettyprinting.doc.CachingDoc.getText(CachingDoc.java:17)
    at org.arend.ext.prettyprinting.doc.CachingDoc.isSingleLine(CachingDoc.java:48)
    at org.arend.ext.prettyprinting.doc.HangDoc.linearize(HangDoc.java:93)
    at org.arend.ext.prettyprinting.doc.HangDoc.linearize(HangDoc.java:102)
    at org.arend.ext.prettyprinting.doc.VListDoc.linearize(VListDoc.java:85)
    at org.arend.ext.prettyprinting.doc.HangDoc.linearize(HangDoc.java:86)
    at org.arend.ext.prettyprinting.doc.VListDoc.linearize(VListDoc.java:85)
    at org.arend.ext.prettyprinting.doc.Doc.linearize(Doc.java:23)
    at org.arend.ext.prettyprinting.doc.LineDocVisitor.visitDoc(LineDocVisitor.java:7)
    at org.arend.ext.prettyprinting.doc.LineDocVisitor.visitVList(LineDocVisitor.java:15)
    at org.arend.ext.prettyprinting.doc.LineDocVisitor.visitVList(LineDocVisitor.java:5)
    at org.arend.ext.prettyprinting.doc.VListDoc.accept(VListDoc.java:23)
    at org.arend.ext.prettyprinting.doc.DocStringBuilder.build(DocStringBuilder.java:14)
    at org.arend.highlight.BasePass.createAnnotation(BasePass.kt:87)
    at org.arend.highlight.BasePass.reportToEditor(BasePass.kt:120)
    at org.arend.highlight.TypecheckerPass.collectInformationWithProgress(TypecheckerPass.kt:24)
    at com.intellij.codeInsight.daemon.impl.ProgressableTextEditorHighlightingPass.doCollectInformation(ProgressableTextEditorHighlightingPass.java:84)
    at com.intellij.codeHighlighting.TextEditorHighlightingPass.collectInformation(TextEditorHighlightingPass.java:52)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$null$1(PassExecutorService.java:434)
    at com.intellij.openapi.application.impl.ApplicationImpl.tryRunReadAction(ApplicationImpl.java:1106)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$doRun$2(PassExecutorService.java:427)
    at com.intellij.openapi.progress.impl.CoreProgressManager.registerIndicatorAndRun(CoreProgressManager.java:625)
    at com.intellij.openapi.progress.impl.CoreProgressManager.executeProcessUnderProgress(CoreProgressManager.java:570)
    at com.intellij.openapi.progress.impl.ProgressManagerImpl.executeProcessUnderProgress(ProgressManagerImpl.java:61)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.doRun(PassExecutorService.java:426)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.lambda$run$0(PassExecutorService.java:402)
    at com.intellij.openapi.application.impl.ReadMostlyRWLock.executeByImpatientReader(ReadMostlyRWLock.java:168)
    at com.intellij.openapi.application.impl.ApplicationImpl.executeByImpatientReader(ApplicationImpl.java:168)
    at com.intellij.codeInsight.daemon.impl.PassExecutorService$ScheduledPass.run(PassExecutorService.java:400)
    at com.intellij.concurrency.JobLauncherImpl$VoidForkJoinTask$1.exec(JobLauncherImpl.java:171)
    at java.base/java.util.concurrent.ForkJoinTask.doExec(ForkJoinTask.java:290)
    at java.base/java.util.concurrent.ForkJoinPool$WorkQueue.topLevelExec(ForkJoinPool.java:1020)
    at java.base/java.util.concurrent.ForkJoinPool.scan(ForkJoinPool.java:1656)
    at java.base/java.util.concurrent.ForkJoinPool.runWorker(ForkJoinPool.java:1594)
    at java.base/java.util.concurrent.ForkJoinWorkerThread.run(ForkJoinWorkerThread.java:177)

image