Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,19 @@ | ||
| <component name="ProjectRunConfigurationManager"> | ||
| <configuration default="false" name="GoalTest" type="JUnit" factoryName="JUnit" nameIsGenerated="true"> | ||
| <module name="lean4ij.test" /> | ||
| <extension name="coverage"> | ||
| <pattern> | ||
| <option name="PATTERN" value="lean4ij.infoview.*" /> | ||
| <option name="ENABLED" value="true" /> | ||
| </pattern> | ||
| </extension> | ||
| <option name="PACKAGE_NAME" value="lean4ij.infoview" /> | ||
| <option name="MAIN_CLASS_NAME" value="lean4ij.infoview.GoalTest" /> | ||
| <option name="METHOD_NAME" value="" /> | ||
| <option name="TEST_OBJECT" value="class" /> | ||
| <option name="VM_PARAMETERS" value="--add-exports=java.base/jdk.internal.vm=ALL-UNNAMED --add-exports=java.base/sun.util.calendar=ALL-UNNAMED --add-exports=java.desktop/sun.awt=ALL-UNNAMED --add-exports=jdk.scripting.nashorn/jdk.nashorn.internal.ir=ALL-UNNAMED --add-opens=java.base/java.lang=ALL-UNNAMED --add-opens=java.base/java.lang.module=ALL-UNNAMED --add-opens=java.base/java.lang.reflect=ALL-UNNAMED --add-opens=java.base/java.math=ALL-UNNAMED --add-opens=java.base/java.nio=ALL-UNNAMED --add-opens=java.base/java.text=ALL-UNNAMED --add-opens=java.base/java.time=ALL-UNNAMED --add-opens=java.base/java.util=ALL-UNNAMED --add-opens=java.base/jdk.internal.jimage=ALL-UNNAMED --add-opens=java.base/jdk.internal.jimage.decompressor=ALL-UNNAMED --add-opens=java.base/jdk.internal.jrtfs=ALL-UNNAMED --add-opens=java.base/jdk.internal.loader=ALL-UNNAMED --add-opens=java.base/jdk.internal.math=ALL-UNNAMED --add-opens=java.base/jdk.internal.module=ALL-UNNAMED --add-opens=java.base/jdk.internal.perf=ALL-UNNAMED --add-opens=java.base/jdk.internal.platform.cgroupv1=ALL-UNNAMED --add-opens=java.base/jdk.internal.ref=ALL-UNNAMED --add-opens=java.base/jdk.internal.reflect=ALL-UNNAMED --add-opens=java.base/jdk.internal.util.jar=ALL-UNNAMED --add-opens=java.base/jdk.internal.vm=ALL-UNNAMED --add-opens=java.base/sun.nio.ch=ALL-UNNAMED --add-opens=java.desktop/com.apple.eawt=ALL-UNNAMED --add-opens=java.desktop/com.apple.eawt.event=ALL-UNNAMED --add-opens=java.desktop/com.apple.laf=ALL-UNNAMED --add-opens=java.desktop/java.awt=ALL-UNNAMED --add-opens=java.desktop/java.awt.dnd.peer=ALL-UNNAMED --add-opens=java.desktop/java.awt.event=ALL-UNNAMED --add-opens=java.desktop/java.awt.image=ALL-UNNAMED --add-opens=java.desktop/java.awt.peer=ALL-UNNAMED --add-opens=java.desktop/javax.swing=ALL-UNNAMED --add-opens=java.desktop/javax.swing.plaf.basic=ALL-UNNAMED --add-opens=java.desktop/javax.swing.text.html=ALL-UNNAMED --add-opens=java.desktop/sun.awt=ALL-UNNAMED --add-opens=java.desktop/sun.awt.image=ALL-UNNAMED --add-opens=java.desktop/sun.awt.windows=ALL-UNNAMED --add-opens=java.desktop/sun.font=ALL-UNNAMED --add-opens=java.desktop/sun.java2d=ALL-UNNAMED --add-opens=java.desktop/sun.lwawt=ALL-UNNAMED --add-opens=java.desktop/sun.lwawt.macosx=ALL-UNNAMED --add-opens=java.desktop/sun.swing=ALL-UNNAMED --add-opens=java.logging/sun.util.logging.internal=ALL-UNNAMED --add-opens=java.xml/javax.xml.catalog=ALL-UNNAMED --add-opens=java.xml/jdk.xml.internal=ALL-UNNAMED --add-opens=jdk.attach/sun.tools.attach=ALL-UNNAMED --add-opens=jdk.internal.jvmstat/sun.jvmstat.monitor=ALL-UNNAMED --add-opens=jdk.jdi/com.sun.tools.jdi=ALL-UNNAMED --add-opens=jdk.management/com.sun.management.internal=ALL-UNNAMED --add-opens=jdk.management.jfr/jdk.management.jfr=ALL-UNNAMED --add-opens=jdk.zipfs/jdk.nio.zipfs=ALL-UNNAMED -Didea.force.use.core.classloader=true -Djava.system.class.loader=com.intellij.util.lang.PathClassLoader -ea" /> | ||
| <method v="2"> | ||
| <option name="Make" enabled="true" /> | ||
| </method> | ||
| </configuration> | ||
| </component> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,129 @@ | ||
| package lean4ij.infoview.dsl | ||
|
|
||
| import com.intellij.openapi.editor.Editor | ||
| import com.intellij.openapi.editor.FoldRegion | ||
| import com.intellij.openapi.editor.colors.EditorColorsManager | ||
| import com.intellij.openapi.editor.colors.TextAttributesKey | ||
| import com.intellij.openapi.editor.markup.HighlighterLayer | ||
| import com.intellij.openapi.editor.markup.HighlighterTargetArea | ||
| import lean4ij.infoview.Lean4TextAttributesKeys | ||
|
|
||
| fun info(init: InfoObjectBuilder.()->Unit) : InfoObjectModel { | ||
| val infoObjectBuilder = InfoObjectBuilder().apply { | ||
| init() | ||
| } | ||
| return infoObjectBuilder.build() | ||
| } | ||
|
|
||
| // fun fold(init: InfoObjectBuilder.()->Unit) { | ||
| // val infoObjectBuilder = InfoObjectBuilder().apply { | ||
| // init() | ||
| // } | ||
| // return infoObjectBuilder.build().apply { | ||
| // fold = Pair("", true) | ||
| // } | ||
| // } | ||
|
|
||
| class InfoObjectBuilder { | ||
|
|
||
| private val data: MutableList<InfoObjectModel> = mutableListOf() | ||
|
|
||
| fun build(): InfoObjectModel { | ||
| return InfoObjectModel(children = data) | ||
| } | ||
|
|
||
| fun info(model: InfoObjectModel) { | ||
| data.add(model) | ||
| } | ||
|
|
||
| fun fold(init: InfoObjectBuilder.() -> Unit) { | ||
| val model = InfoObjectBuilder().run { | ||
| init() | ||
| build() | ||
| } | ||
| model.fold = Pair("", true) | ||
| data.add(model) | ||
| } | ||
|
|
||
| fun h1(text: String) { | ||
| // TODO add attr for h1? | ||
| data.add(InfoObjectModel(text)) | ||
| } | ||
|
|
||
| fun h2(text: String) { | ||
| data.add(InfoObjectModel(text, attr = Lean4TextAttributesKeys.SwingInfoviewCasePos.key)) | ||
| } | ||
|
|
||
| fun p(text: String, attr: MutableList<TextAttributesKey> = mutableListOf()) { | ||
| data.add(InfoObjectModel(text, attr=attr)) | ||
| } | ||
|
|
||
| operator fun String.unaryPlus() { | ||
| data.add(InfoObjectModel(this)) | ||
| } | ||
|
|
||
| } | ||
|
|
||
|
|
||
| class InfoObjectModel( | ||
| val text: String = "", | ||
| val attr: MutableList<TextAttributesKey> = mutableListOf(), | ||
| val children: MutableList<InfoObjectModel>? = mutableListOf(), | ||
| // TODO make a class for this | ||
| var fold: Pair<String, Boolean>? = null | ||
| ) { | ||
| constructor(text: String, attr: TextAttributesKey) : this(text, attr = mutableListOf(attr)) | ||
| fun insert(infoviewObject: InfoObjectModel) { | ||
| children?.add(infoviewObject) | ||
| } | ||
|
|
||
| fun output(renderBuffer: InfoviewRenderBuffer) { | ||
|
Check notice on line 80 in src/main/kotlin/lean4ij/infoview/dsl/dsl.kt
|
||
| // TODO here using some dsl the start/end could be moved to InfoviewRenderBuffer, but | ||
| // currently we do it this way | ||
| val start = renderBuffer.length() | ||
| renderBuffer.output(text) | ||
| if (children != null) { | ||
| for (elem in children) { | ||
| elem.output(renderBuffer) | ||
| } | ||
| } | ||
| val end = renderBuffer.length() | ||
| for (key in attr) { | ||
| renderBuffer.attr(start, end, key) | ||
| } | ||
| if (fold != null) { | ||
| renderBuffer.fold(start, end, fold!!.first, fold!!.second) | ||
| } | ||
| } | ||
| } | ||
|
|
||
|
|
||
| class InfoviewRenderBuffer(private val sb: StringBuilder, private val editor: Editor) { | ||
|
|
||
| fun length() = sb.length | ||
|
|
||
| fun output(text: String) { | ||
| sb.append(text) | ||
| } | ||
|
|
||
| fun attr(start: Int, end: Int, attr: TextAttributesKey) { | ||
| EditorColorsManager.getInstance().globalScheme.getAttributes(attr)?.let { | ||
| editor.markupModel.addRangeHighlighter(start, end, HighlighterLayer.SYNTAX, it, HighlighterTargetArea.EXACT_RANGE) | ||
| } | ||
| } | ||
|
|
||
| fun fold(start: Int, end: Int, placeholderText: String, expanded: Boolean) { | ||
| val foldRegion = editor.foldingModel.addFoldRegion(start, end, placeholderText) | ||
| foldRegion?.isExpanded = expanded | ||
| } | ||
|
|
||
| /** | ||
| * This is mainly for some logic in handling all messages. Once it's expanded, it will keep expanded even | ||
| * default to collapse. | ||
| */ | ||
| fun fold(start: Int, end: Int, placeholderText: String, expanded: Boolean, consumer: (FoldRegion)->Unit) { | ||
| val foldRegion = editor.foldingModel.addFoldRegion(start, end, placeholderText) | ||
| foldRegion?.isExpanded = expanded | ||
| } | ||
|
|
||
| } | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.