mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-12 20:23:52 +00:00
parent
5cabe75933
commit
916f73927d
@ -101,13 +101,20 @@ window.MathJax = {
|
|||||||
html.render();
|
html.render();
|
||||||
const hostTag = root.host.tagName.toLowerCase();
|
const hostTag = root.host.tagName.toLowerCase();
|
||||||
if (hostTag !== "tc-proof-tree") {
|
if (hostTag !== "tc-proof-tree") {
|
||||||
if (callback != null) {
|
if (callback) {
|
||||||
callback(html);
|
callback(html);
|
||||||
}
|
}
|
||||||
return html;
|
return html;
|
||||||
}
|
}
|
||||||
|
// setup style container for styles applied on hover
|
||||||
|
let hoverStyles = root.querySelector("#typicalc-hover-styles");
|
||||||
|
if (!hoverStyles) {
|
||||||
|
hoverStyles = document.createElement('style');
|
||||||
|
hoverStyles.id = "typicalc-hover-styles";
|
||||||
|
root.querySelector("mjx-head").appendChild(hoverStyles);
|
||||||
|
}
|
||||||
// set the size of the rendered SVG to the size of the container element
|
// set the size of the rendered SVG to the size of the container element
|
||||||
if (root.querySelector("#style-fixes") === null) {
|
if (!root.querySelector("#style-fixes")) {
|
||||||
const style = document.createElement('style');
|
const style = document.createElement('style');
|
||||||
style.innerHTML = "\
|
style.innerHTML = "\
|
||||||
mjx-doc, mjx-body, mjx-container, #tc-content, svg {\
|
mjx-doc, mjx-body, mjx-container, #tc-content, svg {\
|
||||||
@ -115,16 +122,49 @@ window.MathJax = {
|
|||||||
}\
|
}\
|
||||||
mjx-container {\
|
mjx-container {\
|
||||||
margin: 0 !important;\
|
margin: 0 !important;\
|
||||||
|
}\
|
||||||
|
.typicalc-type {\
|
||||||
|
stroke: transparent; stroke-width: 600px; pointer-events: all;\
|
||||||
}";
|
}";
|
||||||
if (hostTag === "tc-proof-tree") {
|
|
||||||
style.innerHTML += "svg { width: 100%; }";
|
style.innerHTML += "svg { width: 100%; }";
|
||||||
}
|
|
||||||
style.id = "style-fixes";
|
style.id = "style-fixes";
|
||||||
root.querySelector("mjx-head").appendChild(style);
|
root.querySelector("mjx-head").appendChild(style);
|
||||||
}
|
}
|
||||||
if (callback != null) {
|
if (callback) {
|
||||||
callback(html);
|
callback(html);
|
||||||
}
|
}
|
||||||
|
// listen for hover events on types
|
||||||
|
// the class "typicalc-type" is set in LatexCreatorType
|
||||||
|
root.querySelector("#step0").addEventListener("mouseover", e => {
|
||||||
|
let typeTarget = e.target;
|
||||||
|
let counter = 0;
|
||||||
|
while (!typeTarget.classList.contains("typicalc-type")) {
|
||||||
|
typeTarget = typeTarget.parentElement;
|
||||||
|
counter++;
|
||||||
|
if (counter > 3) {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
const typeClass = typeTarget.classList[1];
|
||||||
|
hoverStyles.innerHTML = "." + typeClass + " { color: red; }";
|
||||||
|
});
|
||||||
|
root.querySelector("#step0").addEventListener("mouseout", e => {
|
||||||
|
let typeTarget = e.target;
|
||||||
|
let counter = 0;
|
||||||
|
while (!typeTarget.classList.contains("typicalc-type")) {
|
||||||
|
typeTarget = typeTarget.parentElement;
|
||||||
|
counter++;
|
||||||
|
if (counter > 3) {
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (!typeTarget.classList.contains("typicalc-type")) {
|
||||||
|
console.log(typeTarget);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
console.log(typeTarget.classList[1]);
|
||||||
|
hoverStyles.innerHTML = "";
|
||||||
|
});
|
||||||
return html;
|
return html;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -15,6 +15,7 @@ import static edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.La
|
|||||||
* @see Type
|
* @see Type
|
||||||
*/
|
*/
|
||||||
public class LatexCreatorType implements TypeVisitor {
|
public class LatexCreatorType implements TypeVisitor {
|
||||||
|
private final Type type;
|
||||||
private static final int MAX_LENGTH = 100000; // 100 KB
|
private static final int MAX_LENGTH = 100000; // 100 KB
|
||||||
|
|
||||||
private final StringBuilder latex = new StringBuilder();
|
private final StringBuilder latex = new StringBuilder();
|
||||||
@ -26,6 +27,7 @@ public class LatexCreatorType implements TypeVisitor {
|
|||||||
* @param type the type
|
* @param type the type
|
||||||
*/
|
*/
|
||||||
protected LatexCreatorType(Type type) {
|
protected LatexCreatorType(Type type) {
|
||||||
|
this.type = type;
|
||||||
type.accept(this);
|
type.accept(this);
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -33,7 +35,8 @@ public class LatexCreatorType implements TypeVisitor {
|
|||||||
* @return the generated LaTeX code
|
* @return the generated LaTeX code
|
||||||
*/
|
*/
|
||||||
protected String getLatex() {
|
protected String getLatex() {
|
||||||
return latex.toString();
|
// this class is used in frontend/src/mathjax-setup.js
|
||||||
|
return "\\class{typicalc-type typicalc-type-" + type.hashCode() + "}{" + latex + "}";
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
|
Loading…
Reference in New Issue
Block a user