Skip to content

Commit

Permalink
Merge pull request #529 from alex999990009/alex99999/fixes-2
Browse files Browse the repository at this point in the history 
Fixes with graph visualization and html generation
  • Loading branch information
@sxhya
sxhya authored Jul 5, 2024
2 parents 31dad75 + 8e10adf commit 44a2023
Show file tree
Hide file tree
Showing 5 changed files with 63 additions and 46 deletions.
2 changes: 1 addition & 1 deletion src/main/kotlin/org/arend/documentation/ArendDocumentationLibHtmlUtil.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
68 changes: 40 additions & 28 deletions src/main/kotlin/org/arend/graph/GraphSimulator.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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<GraphEdge>,
private val vertices: Set<GraphNode>
) {
class GraphSimulator(val project: Project) {
private val fileChooser = JFileChooser()

fun displayOrthogonal() {
fun displayOrthogonal(
graphId: String,
graphName: String,
edges: Set<GraphEdge>,
vertices: Set<GraphNode>
) {
try {
var graph = graph(graphId).directed()

Expand All @@ -47,39 +51,48 @@ 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
}

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")
}
}
}
}

Expand All @@ -103,7 +116,6 @@ class GraphSimulator(
panel.removeAll()
panel.add(imageLabel)
panel.revalidate()
buttonMap[copyImageAction]?.isEnabled = true
}
})
return panel
Expand All @@ -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<Action> {
return arrayOf(copyImageAction, copyFullImageAction)
return arrayOf(copyImageAction, downloadImageAction)
}
}
dialogWrapper.pack()
Expand All @@ -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<DataFlavor> {
return arrayOf(DataFlavor.imageFlavor)
Expand Down
33 changes: 18 additions & 15 deletions src/main/kotlin/org/arend/hierarchy/clazz/ArendClassHierarchyBrowser.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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<TreeNode>()
private val usedNodes = mutableSetOf<ArendDefClass>()
private val edges = mutableSetOf<GraphEdge>()

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<ClassDescendantsSearch>().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 {
Expand All @@ -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<ArendProjectSettings>().data.hierarchyViewType == getSupertypesHierarchyType())

val simulator = GraphSimulator(
e.project,
myProject.service<GraphSimulator>().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()
}
}
}
4 changes: 2 additions & 2 deletions src/main/kotlin/org/arend/module/editor/ArendModuleConfigurationView.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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<GraphSimulator>().displayOrthogonal(this.toString(), "${e.project?.name}_modules", edges, usedNodes.map { GraphNode(it.name) }.toSet())
}
})
}
Expand Down
2 changes: 2 additions & 0 deletions src/main/resources/META-INF/plugin.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -393,6 +393,8 @@

<projectService serviceImplementation="org.arend.toolWindow.errors.tree.ArendErrorTreeCellRendererService"/>

<projectService serviceImplementation="org.arend.graph.GraphSimulator"/>

<applicationService serviceImplementation="org.arend.typechecking.TypecheckingTaskQueue"/>

<!-- Task Execution Listener -->
Expand Down

0 comments on commit 44a2023

Please sign in to comment.