From 2eff253eeb734bd3abb55a3768c6921c4c94428b Mon Sep 17 00:00:00 2001 From: "Aleksei.Luchinin" Date: Fri, 5 Jul 2024 11:09:57 +0300 Subject: [PATCH 1/2] Fix graph problems --- .../kotlin/org/arend/graph/GraphSimulator.kt | 68 +++++++++++-------- .../clazz/ArendClassHierarchyBrowser.kt | 33 +++++---- .../editor/ArendModuleConfigurationView.kt | 4 +- src/main/resources/META-INF/plugin.xml | 2 + 4 files changed, 62 insertions(+), 45 deletions(-) diff --git a/src/main/kotlin/org/arend/graph/GraphSimulator.kt b/src/main/kotlin/org/arend/graph/GraphSimulator.kt index 6ff059b41..db636a70e 100644 --- a/src/main/kotlin/org/arend/graph/GraphSimulator.kt +++ b/src/main/kotlin/org/arend/graph/GraphSimulator.kt @@ -6,6 +6,7 @@ import com.intellij.notification.Notifications import com.intellij.openapi.project.Project import com.intellij.openapi.ui.DialogWrapper import com.intellij.openapi.ui.MessageType +import com.intellij.openapi.ui.Messages import com.intellij.openapi.updateSettings.impl.pluginsAdvertisement.notificationGroup import com.intellij.ui.components.JBPanel import guru.nidi.graphviz.engine.Format @@ -21,20 +22,23 @@ import java.awt.datatransfer.UnsupportedFlavorException import java.awt.event.ActionEvent import java.awt.event.ComponentAdapter import java.awt.event.ComponentEvent +import java.io.File +import java.io.IOException import javax.swing.* data class GraphNode(val id: String) data class GraphEdge(val from: String, val to: String) -class GraphSimulator( - private val project: Project?, - private val graphId: String, - private val edges: Set, - private val vertices: Set -) { +class GraphSimulator(val project: Project) { + private val fileChooser = JFileChooser() - fun displayOrthogonal() { + fun displayOrthogonal( + graphId: String, + graphName: String, + edges: Set, + vertices: Set + ) { try { var graph = graph(graphId).directed() @@ -47,19 +51,20 @@ class GraphSimulator( } val graphviz = Graphviz.fromGraph(graph) - val image = graphviz.render(Format.PNG).toImage() + val render = graphviz.render(format) + val image = render.toImage() val imageIcon = ImageIcon(image) val screenSize = Toolkit.getDefaultToolkit().screenSize - val screenWidth = screenSize.getWidth().toInt() - val screenHeight = screenSize.getHeight().toInt() + val screenWidth = screenSize.getWidth().toInt() - PADDING_SCREEN_WIDTH + val screenHeight = screenSize.getHeight().toInt() - PADDING_SCREEN_HEIGHT val baseImageIcon = if (imageIcon.iconWidth > screenWidth && imageIcon.iconHeight > screenHeight) { - ImageIcon(graphviz.width(screenWidth).height(screenHeight).render(Format.PNG).toImage()) + ImageIcon(graphviz.width(screenWidth).height(screenHeight).render(format).toImage()) } else if (imageIcon.iconWidth > screenWidth) { - ImageIcon(graphviz.width(screenWidth).height(imageIcon.iconHeight).render(Format.PNG).toImage()) + ImageIcon(graphviz.width(screenWidth).height(imageIcon.iconHeight).render(format).toImage()) } else if (imageIcon.iconWidth > screenWidth) { - ImageIcon(graphviz.width(imageIcon.iconWidth).height(screenHeight).render(Format.PNG).toImage()) + ImageIcon(graphviz.width(imageIcon.iconWidth).height(screenHeight).render(format).toImage()) } else { imageIcon } @@ -67,19 +72,27 @@ class GraphSimulator( 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) + val transferableImage = TransferableImage(image) Toolkit.getDefaultToolkit().systemClipboard.setContents(transferableImage, null) - buttonMap[this]?.isEnabled = false } } - private val copyFullImageAction = object : DialogWrapperAction("Copy Full Image") { + private val downloadImageAction = object : DialogWrapperAction("Download Image") { override fun doAction(e: ActionEvent?) { - val transferableImage = TransferableImage(image) - Toolkit.getDefaultToolkit().systemClipboard.setContents(transferableImage, null) + fileChooser.dialogTitle = "Specify a file to save" + fileChooser.selectedFile = File("${graphName.replace(".", "_")}.${format.toString().lowercase()}") + + val userSelection = fileChooser.showSaveDialog(null) + if (userSelection == JFileChooser.APPROVE_OPTION) { + val destinationFilePath = fileChooser.selectedFile.absolutePath + try { + render.toFile(File(destinationFilePath)).createNewFile() + } catch (exception: IOException) { + Messages.showErrorDialog("Failed to save a graph image", "Error") + } + } } } @@ -103,7 +116,6 @@ class GraphSimulator( panel.removeAll() panel.add(imageLabel) panel.revalidate() - buttonMap[copyImageAction]?.isEnabled = true } }) return panel @@ -112,26 +124,22 @@ class GraphSimulator( 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) + ImageIcon(graphviz.width(baseImageIcon.iconWidth).height(height).render(format).toImage()) } height <= baseImageIcon.iconHeight -> { - graphImage =graphviz.width(width).height(baseImageIcon.iconHeight).render(Format.PNG).toImage() - ImageIcon(graphImage) + ImageIcon(graphviz.width(width).height(baseImageIcon.iconHeight).render(format).toImage()) } else -> { - graphImage = graphviz.width(width).height(height).render(Format.PNG).toImage() - ImageIcon(graphImage) + ImageIcon(graphviz.width(width).height(height).render(format).toImage()) } } } override fun createActions(): Array { - return arrayOf(copyImageAction, copyFullImageAction) + return arrayOf(copyImageAction, downloadImageAction) } } dialogWrapper.pack() @@ -146,6 +154,10 @@ class GraphSimulator( } companion object { + val format: Format = Format.SVG + const val PADDING_SCREEN_HEIGHT = 150 + const val PADDING_SCREEN_WIDTH = 100 + class TransferableImage(private val image: Image) : Transferable { override fun getTransferDataFlavors(): Array { return arrayOf(DataFlavor.imageFlavor) diff --git a/src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt b/src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt index b82e9b2ea..39d4fc6e2 100644 --- a/src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt +++ b/src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt @@ -23,11 +23,11 @@ import org.arend.graph.GraphSimulator import org.arend.hierarchy.ArendHierarchyNodeDescriptor import org.arend.psi.ext.ArendDefClass import org.arend.psi.ext.fullName +import org.arend.search.ClassDescendantsSearch import org.arend.settings.ArendProjectSettings import java.util.* import javax.swing.* import javax.swing.tree.DefaultMutableTreeNode -import javax.swing.tree.TreeNode import javax.swing.tree.TreePath class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHierarchyBrowserBase(project, method) { @@ -169,18 +169,21 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie } inner class ArendHierarchyGraphAction : AnAction("Visualize as Orthogonal Diagram", "A hierarchical class graph", ArendIcons.ORTHOGONAL_GRAPH) { - private val usedNodes = mutableSetOf() + private val usedNodes = mutableSetOf() private val edges = mutableSetOf() - private fun findEdges(currentNode: DefaultMutableTreeNode, isSuperTypes: Boolean) { + private fun findEdges(currentNode: ArendDefClass, isSuperTypes: Boolean) { usedNodes.add(currentNode) - val from = ((currentNode.userObject as ArendHierarchyNodeDescriptor).psiElement as ArendDefClass).fullName + val from = currentNode.fullName - val children = TreeUtil.listChildren(currentNode) + val children = if (isSuperTypes) { + currentNode.superClassReferences + } else { + myProject.service().search(currentNode) + }.mapNotNull { it as? ArendDefClass? } for (child in children) { - val to = (((child as DefaultMutableTreeNode).userObject as ArendHierarchyNodeDescriptor).psiElement as? ArendDefClass?)?.fullName - ?: continue + val to = child.refLongName.toString() if (isSuperTypes) { edges.add(GraphEdge(to, from)) } else { @@ -198,20 +201,20 @@ class ArendClassHierarchyBrowser(project: Project, method: PsiElement) : TypeHie edges.clear() val tree = getJTree(currentViewType) ?: return - val root = tree.model.root as DefaultMutableTreeNode + val root = ((tree.model.root as DefaultMutableTreeNode).userObject as ArendHierarchyNodeDescriptor).psiElement as ArendDefClass findEdges(root, myProject.service().data.hierarchyViewType == getSupertypesHierarchyType()) - val simulator = GraphSimulator( - e.project, + myProject.service().displayOrthogonal( this.toString(), + if (currentViewType == getSubtypesHierarchyType()) { + "Subtypes_${root.fullName}" + } else { + "Supertypes_${root.fullName}" + }, edges, - usedNodes.map { - GraphNode( - (((it as DefaultMutableTreeNode).userObject as ArendHierarchyNodeDescriptor).psiElement as? ArendDefClass?)?.fullName!! - ) }.toSet() + usedNodes.map { GraphNode(it.fullName) }.toSet() ) - simulator.displayOrthogonal() } } } diff --git a/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt b/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt index 64e140cb7..184c1cc09 100644 --- a/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt +++ b/src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt @@ -4,6 +4,7 @@ import com.intellij.notification.Notifications import com.intellij.openapi.actionSystem.AnAction import com.intellij.openapi.actionSystem.AnActionEvent import com.intellij.openapi.application.ApplicationManager +import com.intellij.openapi.components.service import com.intellij.openapi.fileChooser.FileChooserDescriptorFactory import com.intellij.openapi.module.Module import com.intellij.openapi.module.ModuleServiceManager @@ -241,8 +242,7 @@ class ArendModuleConfigurationView( } } - val simulator = GraphSimulator(e.project, this.toString(), edges, usedNodes.map { GraphNode(it.name) }.toSet()) - simulator.displayOrthogonal() + module.project.service().displayOrthogonal(this.toString(), "${e.project?.name}_modules", edges, usedNodes.map { GraphNode(it.name) }.toSet()) } }) } diff --git a/src/main/resources/META-INF/plugin.xml b/src/main/resources/META-INF/plugin.xml index 09fe91ea2..bdc677cf6 100644 --- a/src/main/resources/META-INF/plugin.xml +++ b/src/main/resources/META-INF/plugin.xml @@ -393,6 +393,8 @@ + + From 8e10adf136afb27e1008f9a947724d61962437b6 Mon Sep 17 00:00:00 2001 From: "Aleksei.Luchinin" Date: Fri, 5 Jul 2024 11:13:08 +0300 Subject: [PATCH 2/2] Fix html generation html for Arend libraries --- .../org/arend/documentation/ArendDocumentationLibHtmlUtil.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/kotlin/org/arend/documentation/ArendDocumentationLibHtmlUtil.kt b/src/main/kotlin/org/arend/documentation/ArendDocumentationLibHtmlUtil.kt index f206efca0..4ec05f410 100644 --- a/src/main/kotlin/org/arend/documentation/ArendDocumentationLibHtmlUtil.kt +++ b/src/main/kotlin/org/arend/documentation/ArendDocumentationLibHtmlUtil.kt @@ -80,7 +80,7 @@ internal fun generateHtmlForArendLib( val indexFile = File(pathToArendLibInArendSite+ File.separator + "index.md") indexFile.readLines().find { REGEX_AREND_LIB_VERSION.find(it)?.groupValues?.getOrNull(1) == version } - ?: indexFile.appendText("\n * [$version]($version/$AREND_DIR_HTML/Base.html)") + ?: indexFile.appendText("\n * [$version]($version/${AREND_DIR_HTML}Base.html)") val psiManager = PsiManager.getInstance(psiProject)