From 10a36f6cfe76c7a10907c678ecdbc2d693fc647d Mon Sep 17 00:00:00 2001 From: Jazzpirate Date: Thu, 2 Nov 2023 11:11:37 +0100 Subject: [PATCH] annotations in sTeX problems --- .../stex/Extensions/DocumentExtension.scala | 81 ++++++++++++++++++- .../src/info/kwarc/mmt/stex/lsp/Server.scala | 43 +--------- 2 files changed, 82 insertions(+), 42 deletions(-) diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/DocumentExtension.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/DocumentExtension.scala index f4fa1d9711..ee613889f2 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/DocumentExtension.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/DocumentExtension.scala @@ -17,6 +17,8 @@ import info.kwarc.mmt.stex.xhtml.HTMLParser.ParsingState import info.kwarc.mmt.stex.{ErrorReturn, SHTML, STeXServer} import info.kwarc.mmt.stex.xhtml.{HTMLNode, HTMLNodeWrapper, HTMLParser, HTMLRule, SHTMLFrame, SHTMLNode, SHTMLRule, SHTMLState} +import java.net.URLEncoder +import java.nio.charset.Charset import scala.collection.mutable import scala.util.Try //import info.kwarc.mmt.stex.xhtml.{HTMLArg, HTMLComp, HTMLLanguageComponent, HTMLNode, HTMLParser, HasHead, NotationComponent} @@ -637,8 +639,6 @@ trait SHTMLDocumentServer { this : STeXServer => if (!inline) bindings.add(StatementStep) val styles = plain.attributes.getOrElse((HTMLParser.ns_shtml, "styles"), "").split(',').map(_.trim).toList.filterNot(_.isEmpty) plain.classes :::= ("shtml-" + s) :: styles.reverse.map(st => "shtml-" + s + "-" + st) - //val old = plain.attributes.getOrElse((plain.namespace, "style"), "") - //plain.attributes((plain.namespace, "style")) = "counter-set: shtml-statement " + bindings.statement.toString + ";" + old } case class STitle(orig: HTMLNode) extends SHTMLNode(orig) { override def onAdd = { @@ -748,6 +748,21 @@ trait SHTMLDocumentServer { this : STeXServer => def copy = SecTitle(orig.copy) } + case class ProblemTitle(orig: HTMLNode) extends SHTMLNode(orig) { + override def onAdd = { + super.onAdd + this.plain.attributes((this.namespace, "data-problem-title")) = "true" + val n = if (this.plain.parent.exists(_.plain.classes.contains("paragraph"))) { + this.plain.parent.get + } else this + if (n.label == "span") { + n.plain._label = "div" + } + if (n.isEmpty) n.plain.classes ::= "empty" + } + + def copy = ProblemTitle(orig.copy) + } case class SectionLevel(lvl: Int, orig: HTMLNode) extends SHTMLNode(orig) { def copy = SectionLevel(lvl, orig.copy) @@ -805,10 +820,52 @@ trait SHTMLDocumentServer { this : STeXServer => } case class Problem(orig: HTMLNode) extends SHTMLNode(orig) { def copy = Problem(orig.copy) + var objectives: List[(String,String)] = Nil + var preconditions: List[(String, String)] = Nil override def onAdd: Unit = { super.onAdd plain.attributes((this.namespace, "data-problem")) = "true" + plain.attributes((this.namespace,"data-problem-objectives")) = objectives.distinct.map(p => s"${p._1}:${URLEncoder.encode(p._2,Charset.defaultCharset())}").mkString(",") + plain.attributes((this.namespace, "data-problem-preconditions")) = preconditions.distinct.map(p => s"${p._1}:${URLEncoder.encode(p._2,Charset.defaultCharset())}").mkString(",") + } + } + + case class Objective(orig: HTMLNode) extends SHTMLNode(orig) { + def copy = Objective(orig.copy) + + override def onAdd: Unit = { + super.onAdd + this.findAncestor { + case p: Problem => p + }.foreach { p => + val sym = plain.attributes.get((HTMLParser.ns_shtml, "objectivesymbol")) + val dim = plain.attributes.get((HTMLParser.ns_shtml, "objectivedimension")) + (sym,dim) match { + case (Some(sym),Some(dim)) => + p.objectives ::= (dim,sym) + case _ => + } + } + } + } + + case class Precondition(orig: HTMLNode) extends SHTMLNode(orig) { + def copy = Precondition(orig.copy) + + override def onAdd: Unit = { + super.onAdd + this.findAncestor { + case p: Problem => p + }.foreach { p => + val sym = plain.attributes.get((HTMLParser.ns_shtml, "preconditionsymbol")) + val dim = plain.attributes.get((HTMLParser.ns_shtml, "preconditiondimension")) + (sym, dim) match { + case (Some(sym), Some(dim)) => + p.preconditions ::= (dim, sym) + case _ => + } + } } } @@ -960,6 +1017,9 @@ trait SHTMLDocumentServer { this : STeXServer => simple("statementtitle",n => STitle(n)) simple("section",n => Section(n)) simple("sectiontitle",n => SecTitle(n)) + simple("problemtitle", n => ProblemTitle(n)) + simple("objectivesymbol", n => Objective(n)) + simple("preconditionsymbol", n => Precondition(n)) simple("skipsection",n => SkipSection(n)) simple("currentsectionlevel",node => new SHTMLNode(node) { override def copy = node.copy @@ -988,7 +1048,24 @@ trait SHTMLDocumentServer { this : STeXServer => simple("term",node => new SHTMLNode(node) { override def onAdd: Unit = { val lang = getLanguage(this) + + val problem = this.findAncestor { + case p: Problem => p + }/*.foreach { p => + val sym = plain.attributes.get((HTMLParser.ns_shtml, "objectivesymbol")) + val dim = plain.attributes.get((HTMLParser.ns_shtml, "objectivedimension")) + (sym, dim) match { + case (Some(sym), Some(dim)) => + p.objectives ::= (dim, sym) + case _ => + } + }*/ + overlay(this) { s => + problem match { + case Some(p) => p.preconditions ::= ("remember",s) + case _ => + } ("/:" + pathPrefix + "/fragment?" + s + "&language=" + lang, "/:" + pathPrefix + "/declaration?" + s + "&language=" + lang ) diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/lsp/Server.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/lsp/Server.scala index 17dd89520d..d050637311 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/lsp/Server.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/lsp/Server.scala @@ -245,55 +245,18 @@ class STeXLSPServer(style:RunStyle) extends LSPServer(classOf[STeXClient]) with msg.file = msg.file.replace(".xhtml",".tex") val files = controller.backend.getArchive(msg.archive) match { case Some(a) if msg.file.isEmpty => - //val target = controller.extman.getOrAddExtension(classOf[FullsTeX], "fullstex").get val src = a / source - src.descendants.filter(f => f.getExtension.contains("tex") && !a.ignore(src.relativize(f).toFilePath))//.map(src.relativize) - //val eh = STeXLSPErrorHandler(_ => {}, update) - /* files.foreach{f => - update(0, "Building " + a.id + ": " + f) - log("Building " + a.id + ": " + f) - val d = documents.synchronized(documents.getOrElseUpdate(f.toURI.toString,newDocument(f.toURI.toString))) - d.buildFull() - } - a.readRelational(Nil,controller,"rel") - ((),"Done") */ + src.descendants.filter(f => f.getExtension.contains("tex") && !a.ignore(src.relativize(f).toFilePath)) case Some(a) if File(a / source / msg.file).isDirectory => - //val target = controller.extman.getOrAddExtension(classOf[FullsTeX], "fullstex").get val src = (a / source) / msg.file - src.descendants.filter(f => f.getExtension.contains("tex") && !a.ignore((a/source).relativize(f).toFilePath))//.map(f => src.relativize(f)) - //val eh = STeXLSPErrorHandler(_ => {}, update) - /* files.foreach { f => - update(0, "Building " + a.id + ": " + f) - log("Building " + a.id + ": " + f) - val d = documents.synchronized(documents.getOrElseUpdate(f.toURI.toString, newDocument(f.toURI.toString))) - d.buildFull() - } - a.readRelational(Nil, controller, "rel") - ((), "Done") */ + src.descendants.filter(f => f.getExtension.contains("tex") && !a.ignore((a/source).relativize(f).toFilePath)) case Some(a) => - //val target = controller.extman.getOrAddExtension(classOf[FullsTeX], "fullstex").get - //val eh = STeXLSPErrorHandler(_ => {}, update) List((a / source) / msg.file) - //val relfile = File(msg.file).toFilePath - /* update(0,"Building " + a.id + ": " + f) - log("Building " + a.id + ": " + f) - val d = documents.synchronized(documents.getOrElseUpdate(f.toURI.toString, newDocument(f.toURI.toString))) - d.buildFull() - ((), "Done") */ case _ => val archs = controller.backend.getArchives.filter(_.id.startsWith(msg.archive + "/")) - //val target = controller.extman.getOrAddExtension(classOf[FullsTeX], "fullstex").get - //val eh = STeXLSPErrorHandler(_ => {}, update) archs.flatMap {a => val src = a / source - src.descendants.filter(f => f.getExtension.contains("tex") && !a.ignore(src.relativize(f).toFilePath))//.map(src.relativize) - /*files.foreach {f => - update(0, "Building " + a.id + ": " + f) - log("Building " + a.id + ": " + f) - val d = documents.synchronized(documents.getOrElseUpdate(f.toURI.toString, newDocument(f.toURI.toString))) - d.buildFull() - } - a.readRelational(Nil, controller, "rel") */ + src.descendants.filter(f => f.getExtension.contains("tex") && !a.ignore(src.relativize(f).toFilePath)) } return ((),"Archive not found") }