Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fixes with graph visualization and html generation #529

Merged
merged 2 commits into from
Jul 5, 2024
Merged

Fixes with graph visualization and html generation #529

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2eff253
Fix graph problems
alex999990009 Jul 5, 2024
8e10adf
Fix html generation html for Arend libraries
alex999990009 Jul 5, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/main/kotlin/org/arend/documentation/ArendDocumentationLibHtmlUtil.kt
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading