Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master'
Browse files Browse the repository at this point in the history
  • Loading branch information
@valis
valis committed Jun 17, 2024
2 parents 5ec3f20 + 5353fa0 commit 8825bd4
Show file tree
Hide file tree
Showing 34 changed files with 646 additions and 420 deletions.
2 changes: 1 addition & 1 deletion src/main/kotlin/org/arend/actions/ArendActions.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ package org.arend.actions
import com.intellij.openapi.actionSystem.DefaultActionGroup
import org.arend.ArendIcons.AREND

class ArendActions : DefaultActionGroup("Arend Actions", "Show Arend Actions", AREND) {
class ArendActions : DefaultActionGroup("Arend", "Show Arend Actions", AREND) {
init {
templatePresentation.isPopupGroup = true
}
Expand Down
44 changes: 22 additions & 22 deletions src/main/kotlin/org/arend/actions/ArendGotoNextErrorAction.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,34 +45,34 @@ fun selectErrorFromEditor(project: Project, editor: Editor, file: ArendFile?, al
return
}

var arendFile = file
if (arendFile == null) {
ApplicationManager.getApplication().run {
executeOnPooledThread {
ApplicationManager.getApplication().run {
executeOnPooledThread {
var arendFile = file
if (arendFile == null) {
runReadAction {
arendFile = PsiDocumentManager.getInstance(project).getPsiFile(document) as? ArendFile
}
if (arendFile == null) {
return@executeOnPooledThread
}
if (arendFile == null) {
return@executeOnPooledThread
}
runInEdt {
val arendErrors = project.service<ErrorService>().getErrors(arendFile!!)
if (arendErrors.isEmpty()) {
return@runInEdt
}
runInEdt {
val arendErrors = project.service<ErrorService>().getErrors(arendFile!!)
if (arendErrors.isEmpty()) {
return@runInEdt
}

val service = project.service<ArendProjectSettings>()
for (arendError in arendErrors) {
if (always || arendError.error.satisfies(service.autoScrollFromSource)) {
val textRange = BasePass.getImprovedTextRange(arendError.error) ?: continue
if (textRange.containsOffset(offset)) {
val messagesService = project.service<ArendMessagesService>()
messagesService.view?.tree?.select(arendError.error)
if (activate) {
messagesService.activate(project, false)
}
break
val service = project.service<ArendProjectSettings>()
for (arendError in arendErrors) {
if (always || arendError.error.satisfies(service.autoScrollFromSource)) {
val textRange = BasePass.getImprovedTextRange(arendError.error) ?: continue
if (textRange.containsOffset(offset)) {
val messagesService = project.service<ArendMessagesService>()
messagesService.view?.tree?.select(arendError.error)
if (activate) {
messagesService.activate(project, false)
}
break
}
}
}
Expand Down
7 changes: 2 additions & 5 deletions src/main/kotlin/org/arend/actions/SearchArendFilesContributor.kt
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,6 @@
package org.arend.actions

import com.intellij.ide.actions.searcheverywhere.AbstractGotoSEContributor
import com.intellij.ide.actions.searcheverywhere.FileSearchEverywhereContributor
import com.intellij.ide.actions.searcheverywhere.SearchEverywhereContributor
import com.intellij.ide.actions.searcheverywhere.SearchEverywhereContributorFactory
import com.intellij.ide.actions.searcheverywhere.*
import com.intellij.ide.util.gotoByName.FileTypeRef
import com.intellij.ide.util.gotoByName.FilteringGotoByModel
import com.intellij.ide.util.gotoByName.GotoFileModel
Expand Down Expand Up @@ -44,6 +41,6 @@ class SearchArendFilesContributor(val event: AnActionEvent) : AbstractGotoSECont

class ArendSECFactory : SearchEverywhereContributorFactory<Any> {
override fun createContributor(initEvent: AnActionEvent): SearchEverywhereContributor<Any> {
return SearchArendFilesContributor(initEvent)
return PSIPresentationBgRendererWrapper(SearchArendFilesContributor(initEvent))
}
}
95 changes: 81 additions & 14 deletions src/main/kotlin/org/arend/graph/GraphSimulator.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,12 +6,19 @@ import com.intellij.openapi.project.Project
import com.intellij.openapi.ui.DialogWrapper
import com.intellij.openapi.ui.MessageType
import com.intellij.openapi.updateSettings.impl.pluginsAdvertisement.notificationGroup
import com.intellij.ui.util.minimumHeight
import com.intellij.ui.util.minimumWidth
import guru.nidi.graphviz.engine.Format
import guru.nidi.graphviz.engine.Graphviz
import guru.nidi.graphviz.model.Factory.graph
import guru.nidi.graphviz.model.Factory.node
import java.awt.Color
import java.awt.Image
import java.awt.Toolkit
import java.awt.datatransfer.DataFlavor
import java.awt.datatransfer.Transferable
import java.awt.datatransfer.UnsupportedFlavorException
import java.awt.event.ActionEvent
import java.awt.event.ComponentAdapter
import java.awt.event.ComponentEvent
import javax.swing.*
Expand Down Expand Up @@ -40,18 +47,42 @@ class GraphSimulator(
}

val graphviz = Graphviz.fromGraph(graph)
val baseImageIcon = ImageIcon(
graphviz.render(Format.PNG).toImage()
)
val image = graphviz.render(Format.PNG).toImage()
val imageIcon = ImageIcon(image)

val screenSize = Toolkit.getDefaultToolkit().screenSize
val screenWidth = screenSize.getWidth().toInt()
val screenHeight = screenSize.getHeight().toInt()

var imageIcon = getImageIcon(baseImageIcon, graphviz, screenWidth, screenHeight)
var imageLabel = JLabel(imageIcon)
val baseImageIcon = if (imageIcon.iconWidth > screenWidth && imageIcon.iconHeight > screenHeight) {
ImageIcon(graphviz.width(screenWidth).height(screenHeight).render(Format.PNG).toImage())
} else if (imageIcon.iconWidth > screenWidth) {
ImageIcon(graphviz.width(screenWidth).height(imageIcon.iconHeight).render(Format.PNG).toImage())
} else if (imageIcon.iconWidth > screenWidth) {
ImageIcon(graphviz.width(imageIcon.iconWidth).height(screenHeight).render(Format.PNG).toImage())
} else {
imageIcon
}

var imageLabel = JLabel(baseImageIcon)

val dialogWrapper = object : DialogWrapper(project, true) {
private var graphImage = image
private val copyImageAction = object : DialogWrapperAction("Copy Image") {
override fun doAction(e: ActionEvent?) {
val transferableImage = TransferableImage(graphImage)
Toolkit.getDefaultToolkit().systemClipboard.setContents(transferableImage, null)
buttonMap[this]?.isEnabled = false
}
}

private val copyFullImageAction = object : DialogWrapperAction("Copy Full Image") {
override fun doAction(e: ActionEvent?) {
val transferableImage = TransferableImage(image)
Toolkit.getDefaultToolkit().systemClipboard.setContents(transferableImage, null)
}
}

init {
init()
}
Expand All @@ -62,18 +93,46 @@ class GraphSimulator(
panel.background = Color.WHITE
panel.addComponentListener(object : ComponentAdapter() {
override fun componentResized(e: ComponentEvent) {
imageIcon = getImageIcon(baseImageIcon, graphviz, e.component.width, e.component.height)
val component = panel.components.getOrNull(0) ?: return
panel.minimumWidth = baseImageIcon.iconWidth + size.width - e.component.width
panel.minimumHeight = baseImageIcon.iconHeight + size.height - e.component.height

val imageIcon = getImageIcon(baseImageIcon, graphviz, e.component.width - component.bounds.x * 2, e.component.height - component.bounds.y * 2)
imageLabel = JLabel(imageIcon)

panel.removeAll()
panel.add(imageLabel)
panel.revalidate()
buttonMap[copyImageAction]?.isEnabled = true
}
})
return panel
}

override fun createActions(): Array<Action> = emptyArray()
private fun getImageIcon(baseImageIcon: ImageIcon, graphviz: Graphviz, width: Int, height: Int): ImageIcon {
return when {
width <= baseImageIcon.iconWidth && height <= baseImageIcon.iconHeight -> {
graphImage = image
baseImageIcon
}
width <= baseImageIcon.iconWidth -> {
graphImage = graphviz.width(baseImageIcon.iconWidth).height(height).render(Format.PNG).toImage()
ImageIcon(graphImage)
}
height <= baseImageIcon.iconHeight -> {
graphImage =graphviz.width(width).height(baseImageIcon.iconHeight).render(Format.PNG).toImage()
ImageIcon(graphImage)
}
else -> {
graphImage = graphviz.width(width).height(height).render(Format.PNG).toImage()
ImageIcon(graphImage)
}
}
}

override fun createActions(): Array<Action> {
return arrayOf(copyImageAction, copyFullImageAction)
}
}
dialogWrapper.pack()
dialogWrapper.show()
Expand All @@ -84,14 +143,22 @@ class GraphSimulator(
}
}

private fun getImageIcon(baseImageIcon: ImageIcon, graphviz: Graphviz, width: Int, height: Int): ImageIcon {
return when {
width <= baseImageIcon.iconWidth || height <= baseImageIcon.iconHeight -> {
ImageIcon(
graphviz.width(width).height(height).render(Format.PNG).toImage()
)
companion object {
class TransferableImage(private val image: Image) : Transferable {
override fun getTransferDataFlavors(): Array<DataFlavor> {
return arrayOf(DataFlavor.imageFlavor)
}

override fun isDataFlavorSupported(flavor: DataFlavor): Boolean {
return flavor.equals(DataFlavor.imageFlavor)
}

override fun getTransferData(flavor: DataFlavor): Any {
if (flavor.equals(DataFlavor.imageFlavor)) {
return image
}
throw UnsupportedFlavorException(flavor)
}
else -> baseImageIcon
}
}
}
14 changes: 9 additions & 5 deletions src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -167,11 +167,11 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie
}
}

inner class ArendHierarchyGraphAction : AnAction(ArendIcons.ORTHOGONAL_GRAPH) {
inner class ArendHierarchyGraphAction : AnAction("Visualize as Orthogonal Diagram", "A hierarchical class graph", ArendIcons.ORTHOGONAL_GRAPH) {
private val usedNodes = mutableSetOf<TreeNode>()
private val edges = mutableSetOf<GraphEdge>()

private fun findEdges(currentNode: DefaultMutableTreeNode) {
private fun findEdges(currentNode: DefaultMutableTreeNode, isSuperTypes: Boolean) {
usedNodes.add(currentNode)

val from = ((currentNode.userObject as ArendHierarchyNodeDescriptor).psiElement as ArendDefClass).fullName
Expand All @@ -180,10 +180,14 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie
for (child in children) {
val to = (((child as DefaultMutableTreeNode).userObject as ArendHierarchyNodeDescriptor).psiElement as? ArendDefClass?)?.fullName
?: continue
edges.add(GraphEdge(from, to))
if (isSuperTypes) {
edges.add(GraphEdge(to, from))
} else {
edges.add(GraphEdge(from, to))
}

if (!usedNodes.contains(child)) {
findEdges(child)
findEdges(child, isSuperTypes)
}
}
}
Expand All @@ -195,7 +199,7 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie
val tree = getJTree(currentViewType) ?: return
val root = tree.model.root as DefaultMutableTreeNode

findEdges(root)
findEdges(root, myProject.service<ArendProjectSettings>().data.hierarchyViewType == getSupertypesHierarchyType())

val simulator = GraphSimulator(
e.project,
Expand Down
65 changes: 0 additions & 65 deletions src/main/kotlin/org/arend/highlight/RedundantParameterNamePass.kt
View file

This file was deleted.

27 changes: 0 additions & 27 deletions src/main/kotlin/org/arend/highlight/RedundantParameterNamePassFactory.kt
View file

This file was deleted.

Loading

0 comments on commit 8825bd4

Please sign in to comment.