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

Added latex formulas to quick documentation #443

Merged
merged 1 commit into from
Jan 18, 2024
Merged

Added latex formulas to quick documentation #443

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
1 change: 1 addition & 0 deletions build.gradle.kts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@ dependencies {
implementation("org.arend:base")
implementation(kotlin("reflect"))
implementation(kotlin("stdlib-jdk8"))
implementation("org.scilab.forge:jlatexmath:1.0.7")
}

java {
Expand Down
60 changes: 58 additions & 2 deletions src/main/grammars/ArendDocLexer.flex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,9 +38,13 @@ import static org.arend.psi.ArendElementTypes.*;
%state CODE1
%state CODE2
%state CODE3
%state NEWLINE_LATEX_CODE
%state INLINE_LATEX_CODE
%state CLOSE_CODE1
%state CLOSE_CODE2
%state CLOSE_CODE3
%state CLOSE_NEWLINE_LATEX_CODE
%state CLOSE_INLINE_LATEX_CODE
%state REFERENCE
%state REFERENCE_TEXT

Expand Down Expand Up @@ -94,6 +98,16 @@ NEW_LINE_HYPHEN = "\n" [ \t]* "-"
yybegin(CODE3);
return DOC_CODE_BLOCK_BORDER;
}
"$$" {
textStart = getTokenStart();
yybegin(NEWLINE_LATEX_CODE);
return DOC_NEWLINE_LATEX_CODE;
}
"$" {
textStart = getTokenStart();
yybegin(INLINE_LATEX_CODE);
return DOC_INLINE_LATEX_CODE;
}
"-}" {
if (zzMarkedPos == zzBuffer.length()) {
yybegin(YYINITIAL);
Expand All @@ -120,7 +134,7 @@ NEW_LINE_HYPHEN = "\n" [ \t]* "-"
}

<TEXT> {
("{" | "[" | "`" | {NEW_LINE}) {
("{" | "[" | "`" | "$$" | "$" | {NEW_LINE}) {
zzMarkedPos = zzStartRead;
zzStartRead = textStart;
yybegin(CONTENTS);
Expand Down Expand Up @@ -196,7 +210,39 @@ NEW_LINE_HYPHEN = "\n" [ \t]* "-"
[^] {}
}

<TEXT,CODE1,CODE2,CODE3,REFERENCE_TEXT> {
<NEWLINE_LATEX_CODE> {
"$$" {
zzMarkedPos -= 2;
zzStartRead = textStart;
yybegin(CLOSE_NEWLINE_LATEX_CODE);
return DOC_LATEX_CODE;
}
"\n" {
zzMarkedPos--;
zzStartRead = textStart;
yybegin(CONTENTS);
return DOC_LATEX_CODE;
}
[^] {}
}

<INLINE_LATEX_CODE> {
"$" {
zzMarkedPos--;
zzStartRead = textStart;
yybegin(CLOSE_INLINE_LATEX_CODE);
return DOC_LATEX_CODE;
}
"\n" {
zzMarkedPos--;
zzStartRead = textStart;
yybegin(CONTENTS);
return DOC_LATEX_CODE;
}
[^] {}
}

<TEXT,CODE1,CODE2,CODE3,NEWLINE_LATEX_CODE,INLINE_LATEX_CODE,REFERENCE_TEXT> {
"-}" {
if (zzMarkedPos == zzBuffer.length()) {
zzMarkedPos -= 2;
Expand Down Expand Up @@ -244,4 +290,14 @@ NEW_LINE_HYPHEN = "\n" [ \t]* "-"
}
}

<CLOSE_NEWLINE_LATEX_CODE>"$$" {
yybegin(CONTENTS);
return DOC_NEWLINE_LATEX_CODE;
}

<CLOSE_INLINE_LATEX_CODE>"$" {
yybegin(CONTENTS);
return DOC_INLINE_LATEX_CODE;
}

[^] { return BAD_CHARACTER; }
4 changes: 4 additions & 0 deletions src/main/java/org/arend/parser/ParserMixin.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,10 @@ public class ParserMixin {
public static final ArendTokenType DOC_LBRACKET = new ArendTokenType("[");
public static final ArendTokenType DOC_RBRACKET = new ArendTokenType("]");
public static final ArendTokenType DOC_CODE_BLOCK_BORDER = new ArendTokenType("```");
public static final ArendTokenType DOC_NEWLINE_LATEX_CODE = new ArendTokenType("$$");
public static final ArendTokenType DOC_INLINE_LATEX_CODE = new ArendTokenType("$");
public static final ArendTokenType DOC_LATEX_CODE = new ArendTokenType("DOC_LATEX_CODE");

public static final ArendCompositeElementType DOC_CODE_BLOCK = new ArendCompositeElementType("DOC_CODE_BLOCK");
public static final ArendCompositeElementType DOC_REFERENCE = new ArendCompositeElementType("DOC_REFERENCE");
public static final ArendCompositeElementType DOC_REFERENCE_TEXT = new ArendCompositeElementType("DOC_REFERENCE_TEXT");
Expand Down
13 changes: 13 additions & 0 deletions src/main/kotlin/org/arend/documentation/ArendDocumentationProvider.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,12 @@ import org.arend.psi.doc.ArendDocCodeBlock
import org.arend.psi.doc.ArendDocComment
import org.arend.psi.doc.ArendDocReference
import org.arend.psi.ext.*
import org.arend.psi.prevElement
import org.arend.term.abs.Abstract
import org.jsoup.Jsoup
import org.jsoup.nodes.Document
import org.jsoup.nodes.Element
import java.io.File
import java.net.UnknownHostException


Expand Down Expand Up @@ -209,13 +211,18 @@ class ArendDocumentationProvider : AbstractDocumentationProvider() {
}

private fun generateDoc(element: PsiElement, originalElement: PsiElement?, withDocComments: Boolean): String? {
File("latex-images").deleteRecursively()

val ref = element as? PsiReferable ?: (element as? ArendDocComment)?.owner
?: return if (element.isArendKeyword()) generateDocForKeywords(element) else null
return buildString { wrapTag("html") {
wrapTag("head") {
wrapTag("style") {
append(".normal_text { white_space: nowrap; }.code { white_space: pre; }")
}
wrapTag("style") {
append(".center {text-align: center;}")
}
}

wrapTag("body") {
Expand Down Expand Up @@ -247,6 +254,12 @@ class ArendDocumentationProvider : AbstractDocumentationProvider() {
elementType == DOC_TEXT -> html(docElement.text)
elementType == WHITE_SPACE -> append(" ")
elementType == DOC_CODE -> append("<code>${docElement.text.htmlEscape()}</code>")
elementType == DOC_LATEX_CODE -> append(getHtmlLatexCode("image${counterLatexImages++}",
docElement.text.htmlEscape(),
docElement.prevElement.elementType == DOC_NEWLINE_LATEX_CODE,
element.project,
docElement.textOffset)
)
elementType == DOC_PARAGRAPH_SEP -> {
append("<br>")
if (!full) {
Expand Down
94 changes: 92 additions & 2 deletions src/main/kotlin/org/arend/documentation/ArendDocumentationUtil.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,21 @@ package org.arend.documentation
import com.intellij.codeInsight.daemon.impl.DaemonProgressIndicator
import com.intellij.codeInsight.daemon.impl.DefaultHighlightInfoProcessor
import com.intellij.lang.documentation.DocumentationSettings
import com.intellij.notification.NotificationAction
import com.intellij.notification.NotificationType
import com.intellij.notification.SingletonNotificationManager
import com.intellij.openapi.application.PathManager
import com.intellij.openapi.diagnostic.Logger
import com.intellij.openapi.editor.colors.EditorColors
import com.intellij.openapi.editor.colors.EditorColorsManager
import com.intellij.openapi.editor.colors.EditorColorsScheme
import com.intellij.openapi.editor.richcopy.HtmlSyntaxInfoUtil
import com.intellij.openapi.fileEditor.FileEditorManager
import com.intellij.openapi.fileEditor.OpenFileDescriptor
import com.intellij.openapi.module.ModuleManager
import com.intellij.openapi.project.Project
import com.intellij.openapi.project.ProjectManager
import com.intellij.openapi.updateSettings.impl.pluginsAdvertisement.notificationGroup
import com.intellij.openapi.util.TextRange
import com.intellij.openapi.vfs.LocalFileSystem
import com.intellij.openapi.vfs.VfsUtilCore.visitChildrenRecursively
Expand All @@ -24,6 +30,8 @@ import com.intellij.psi.PsiManager
import com.intellij.psi.PsiRecursiveElementVisitor
import com.intellij.psi.util.elementType
import com.intellij.testFramework.LightVirtualFile
import com.intellij.util.ui.ImageUtil
import com.intellij.util.ui.JBUI
import com.intellij.xml.util.XmlStringUtil
import org.apache.commons.lang.StringEscapeUtils
import org.arend.ArendLanguage
Expand All @@ -33,12 +41,23 @@ import org.arend.highlight.ArendHighlightingPass
import org.arend.highlight.ArendSyntaxHighlighter
import org.arend.module.config.ArendModuleConfigService
import org.arend.psi.ArendFile
import org.arend.psi.ext.*
import org.arend.psi.ext.ArendReferenceElement
import org.arend.psi.ext.PsiLocatedReferable
import org.arend.util.ArendBundle
import org.arend.util.FileUtils.EXTENSION
import org.arend.util.register
import org.jsoup.nodes.Element
import org.scilab.forge.jlatexmath.ParseException
import org.scilab.forge.jlatexmath.TeXConstants
import org.scilab.forge.jlatexmath.TeXFormula
import org.scilab.forge.jlatexmath.TeXIcon
import java.awt.image.BufferedImage
import java.io.File
import javax.imageio.ImageIO
import javax.swing.JLabel
import javax.swing.UIManager
import kotlin.math.roundToInt
import kotlin.system.exitProcess

private val LOG: Logger = Logger.getInstance("#org.arend.documentation")
Expand All @@ -64,6 +83,8 @@ internal val REGEX_CODE = "<code class=\"language-plaintext highlighter-rouge\">
internal val REGEX_HREF = "<a href=\"([^\"]+)\">([^\"]+)</a>".toRegex()
internal val REGEX_AREND_LIB_VERSION = "\\* \\[(.+)]".toRegex()

const val HTML_IMAGE_LATEX_SHIFT = 0.15

internal fun String.htmlEscape(): String = XmlStringUtil.escapeString(this, true)

internal fun String.wrapTag(tag: String) = "<$tag>$this</$tag>"
Expand All @@ -80,7 +101,7 @@ internal inline fun StringBuilder.wrapTag(tag: String, crossinline body: () -> U
wrap("<$tag>", "</$tag>", body)
}

fun StringBuilder.appendNewLineHtml() = append("<br>")
fun StringBuilder.appendNewLineHtml(): StringBuilder = append("<br>")

internal fun StringBuilder.processElement(project: Project, element: Element, chapter: String?, folder: String?) {
if (element.className() == HIGHLIGHTER_CLASS) {
Expand All @@ -98,6 +119,75 @@ internal fun StringBuilder.processElement(project: Project, element: Element, ch
appendNewLineHtml()
}

internal var counterLatexImages = 0

internal fun getHtmlLatexCode(title: String, latexCode: String, isNewLine: Boolean, project: Project, offset: Int): String {
try {
val font = UIManager.getDefaults().getFont("Label.font").size.toFloat()

val formula = TeXFormula(latexCode)
val icon: TeXIcon = formula.TeXIconBuilder()
.setStyle(TeXConstants.STYLE_DISPLAY)
.setSize(font)
.build()
.apply {
insets.run {
top -= (font * HTML_IMAGE_LATEX_SHIFT).roundToInt()
bottom -= (font * HTML_IMAGE_LATEX_SHIFT).roundToInt()
left -= (font * HTML_IMAGE_LATEX_SHIFT).roundToInt()
right -= (font * HTML_IMAGE_LATEX_SHIFT).roundToInt()
}
}
val image = ImageUtil.createImage(icon.iconWidth, icon.iconHeight, BufferedImage.TYPE_INT_ARGB)

val graphics = image.createGraphics()
graphics.color = EditorColorsManager.getInstance().globalScheme.getColor(EditorColors.DOCUMENTATION_COLOR)
graphics.fillRect(0, 0, icon.iconWidth, icon.iconHeight)

val label = JLabel()
label.setForeground(JBUI.CurrentTheme.RunWidget.FOREGROUND)

icon.paintIcon(label, graphics, 0, 0)

val latexImagesDir = File("latex-images").apply {
mkdir()
}

val file = File(latexImagesDir.path + File.separator + title + ".png")
ImageIO.write(image, "png", file.getAbsoluteFile())

return buildString {
if (isNewLine) {
append("<div class=\"center\">")
}
append("<img ${if (!isNewLine) "style=\"transform: translate(0px,${icon.iconDepth}px);\"" else ""} src=\"file:///${file.absolutePath}\" title=$title width=\"${icon.iconWidth}\" height=\"${icon.iconHeight}\">")
if (isNewLine) {
append("</div>")
}
}
} catch (e: Exception) {
if (e is ParseException) {
val notificationManager = SingletonNotificationManager(notificationGroup.displayId, NotificationType.WARNING)

val notificationAction = NotificationAction.createSimpleExpiring(ArendBundle.message("arend.click.to.set.cursor.latex")) {
val fileEditorManager = FileEditorManager.getInstance(project)
val editor = fileEditorManager.selectedTextEditor ?: return@createSimpleExpiring
val caretModel = editor.caretModel
caretModel.moveToOffset(offset)
}

e.message?.let {
notificationManager.notify("LaTeX parsing warning", it, project) { notification ->
notification.setSuggestionType(true).addAction(notificationAction)
}
}
} else {
LOG.error(e)
}
}
return ""
}

private fun isAside(tag: String) = tag == "aside"

internal fun changeTags(line: String, chapter: String?, folder: String?, isAside: Boolean): String {
Expand Down Expand Up @@ -211,7 +301,7 @@ fun generateHtmlForArendLib(
}
arendBaseFile.delete()
} catch (e : Exception) {
e.printStackTrace()
LOG.warn(e)
} finally {
projectManager.closeAndDispose(psiProject)
}
Expand Down
3 changes: 2 additions & 1 deletion src/main/kotlin/org/arend/parser/ArendDocParser.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,8 @@ class ArendDocParser : PsiParser, LightPsiParser {

while (!builder.eof()) {
when (val token = builder.tokenType) {
DOC_INLINE_CODE_BORDER, DOC_CODE, DOC_PARAGRAPH_SEP -> builder.advanceLexer()
DOC_INLINE_CODE_BORDER, DOC_CODE, DOC_PARAGRAPH_SEP,
DOC_INLINE_LATEX_CODE, DOC_NEWLINE_LATEX_CODE, DOC_LATEX_CODE -> builder.advanceLexer()
DOC_LBRACKET -> parseReferenceText(builder)
LBRACE -> parseReference(builder, builder.mark())
DOC_CODE_BLOCK_BORDER -> parseCodeBlock(builder)
Expand Down
2 changes: 1 addition & 1 deletion src/main/kotlin/org/arend/psi/ArendTokenType.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -147,4 +147,4 @@ val AREND_GOALS: TokenSet = TokenSet.create(TGOAL, UNDERSCORE, APPLY_HOLE)

val AREND_DOC_TOKENS: TokenSet = TokenSet.create(DOC_SINGLE_LINE_START, DOC_START, DOC_END, DOC_INLINE_CODE_BORDER,
DOC_TEXT, DOC_CODE, DOC_CODE_LINE, DOC_PARAGRAPH_SEP, DOC_LBRACKET, DOC_RBRACKET, DOC_CODE_BLOCK_BORDER, DOC_CODE_BLOCK,
DOC_REFERENCE, DOC_REFERENCE_TEXT)
DOC_REFERENCE, DOC_REFERENCE_TEXT, DOC_INLINE_LATEX_CODE, DOC_NEWLINE_LATEX_CODE, DOC_LATEX_CODE)
3 changes: 2 additions & 1 deletion src/main/resources/messages/ArendBundle.properties
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -168,4 +168,5 @@ arend.disableGroupSource=MarkSourceRootGroup
arend.disableActionUnmark=UnmarkRoot

arend.click.to.see.diff.link=<Click to see difference>
arend.click.to.see.diff.link.title=Type comparison
arend.click.to.see.diff.link.title=Type comparison
arend.click.to.set.cursor.latex=Set the cursor to the incorrect latex formula
Loading