From 1fc88e5b45b181c3de3930181d1726fcf9e0a413 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dennis=20M=C3=BCller?= Date: Wed, 4 May 2022 11:33:02 +0200 Subject: [PATCH 1/4] sTeX, mostly --- .../kwarc/mmt/intellij/checking/Checker.scala | 6 +- .../mmt-web/stex/htmlfragments/header.xml | 3 +- .../mmt-web/stex/htmlfragments/highlights.css | 2 +- .../resources/mmt-web/vollki/guidedtours.html | 8 +-- .../info/kwarc/mmt/api/archives/Archive.scala | 6 +- .../stex/Extensions/FragmentExtension.scala | 12 ++-- .../mmt/stex/Extensions/OMDocExtension.scala | 27 ++++++- .../info/kwarc/mmt/stex/rules/Sequences.scala | 10 +++ .../src/info/kwarc/mmt/stex/sTeX.scala | 2 + .../mmt/stex/vollki/GraphExtensions.scala | 72 ++++++++++++------- .../src/info/kwarc/mmt/stex/xhtml/XHTML.scala | 27 ++++--- .../kwarc/mmt/stex/xhtml/XHTMLOMDoc.scala | 28 ++++++-- 12 files changed, 149 insertions(+), 54 deletions(-) diff --git a/src/intellij-mmt/src/info/kwarc/mmt/intellij/checking/Checker.scala b/src/intellij-mmt/src/info/kwarc/mmt/intellij/checking/Checker.scala index c1b45d4086..1a1451895b 100644 --- a/src/intellij-mmt/src/info/kwarc/mmt/intellij/checking/Checker.scala +++ b/src/intellij-mmt/src/info/kwarc/mmt/intellij/checking/Checker.scala @@ -70,7 +70,7 @@ class Checker(controller: Controller,ev : ErrorViewer) { e match { case s: SourceError => - (s.ref.region, s.mainMessage, s.extraMessages, s.level == Level.Warning) + (s.ref.region, s.mainMessage, s.extraMessages, s.level == Level.Warning || e.excuse.isDefined) case e: Invalid => var mainMessage = e.shortMsg var extraMessages: List[String] = e.extraMessage.split("\n").toList @@ -106,9 +106,9 @@ class Checker(controller: Controller,ev : ErrorViewer) { mainMessage = "error with unknown location: " + mainMessage SourceRef(utils.FileURI(file), SourceRegion(SourcePosition(0, 0, 0), SourcePosition(0, 0, 0))) } - (ref.region, mainMessage, extraMessages.filter(_.trim != ""),e.level == Level.Warning) + (ref.region, mainMessage, extraMessages.filter(_.trim != ""),e.level == Level.Warning || e.excuse.isDefined) case e: Error => - (SourceRegion.none, "error with unknown location: " + e.getMessage, e.extraMessage.split("\n").toList,e.level==Level.Warning) + (SourceRegion.none, "error with unknown location: " + e.getMessage, e.extraMessage.split("\n").toList,e.level==Level.Warning || e.excuse.isDefined) } } } diff --git a/src/mmt-api/resources/mmt-web/stex/htmlfragments/header.xml b/src/mmt-api/resources/mmt-web/stex/htmlfragments/header.xml index 8016541b67..39637a35b4 100644 --- a/src/mmt-api/resources/mmt-web/stex/htmlfragments/header.xml +++ b/src/mmt-api/resources/mmt-web/stex/htmlfragments/header.xml @@ -5,7 +5,6 @@ - \ No newline at end of file diff --git a/src/mmt-api/resources/mmt-web/stex/htmlfragments/highlights.css b/src/mmt-api/resources/mmt-web/stex/htmlfragments/highlights.css index 3db186e112..20e3b1db48 100644 --- a/src/mmt-api/resources/mmt-web/stex/htmlfragments/highlights.css +++ b/src/mmt-api/resources/mmt-web/stex/htmlfragments/highlights.css @@ -1,5 +1,5 @@ .definiendum { - color: #00FF00; + color: #00BB00; font-weight: bold; } .varcomp { diff --git a/src/mmt-api/resources/mmt-web/vollki/guidedtours.html b/src/mmt-api/resources/mmt-web/vollki/guidedtours.html index 484620c05f..106010a44e 100644 --- a/src/mmt-api/resources/mmt-web/vollki/guidedtours.html +++ b/src/mmt-api/resources/mmt-web/vollki/guidedtours.html @@ -21,10 +21,10 @@ var edoc = document.getElementById("entrydoc"); var user = document.getElementById("usermodel"); var lang = document.getElementById("language"); - xhr.open("GET","/:vollki/tour?path=" + edoc.options[edoc.selectedIndex].text + "&user=" + user.options[user.selectedIndex].text + "&lang=" + lang.options[lang.selectedIndex].value, true); + xhr.open("GET","/:vollki/tour?path=" + edoc.options[edoc.selectedIndex].value + "&user=" + user.options[user.selectedIndex].value + "&lang=" + lang.options[lang.selectedIndex].value, true); xhr.setRequestHeader('Content-type', 'text/html'); xhr.onreadystatechange = function(e) { - if(xhr.readyState == 4 && xhr.status == 200) { + if(xhr.readyState == 4 && xhr.status == 200) { con.innerHTML = xhr.responseText; MathJax.Hub.Queue(["Typeset",MathJax.Hub]); } @@ -40,10 +40,10 @@ var lang = document.getElementById("language"); var elem = document.getElementById(id + '-collapse'); var xhr = new XMLHttpRequest(); - xhr.open("GET","/:vollki/frag?path=" + id + "&lang=" + lang.options[lang.selectedIndex].value, true); + xhr.open("GET","/:vollki/frag?path=" + id + "&lang=" + lang.options[lang.selectedIndex].value, true); xhr.setRequestHeader('Content-type', 'text/html'); xhr.onreadystatechange = function(e) { - if(xhr.readyState == 4 && xhr.status == 200) { + if(xhr.readyState == 4 && xhr.status == 200) { elem.innerHTML = xhr.responseText; elem.style.display = 'flex'; MathJax.Hub.Queue(["Typeset",MathJax.Hub]); diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/archives/Archive.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/archives/Archive.scala index e390c02364..db85fc3a6a 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/archives/Archive.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/archives/Archive.scala @@ -117,6 +117,10 @@ class Archive(val root: File, val properties: mutable.Map[String, String], val r val TraverseMode(filter, filterDir, parallel) = mode def recurse(n: String): List[A] = traverse(dim, in / n, mode, sendLog)(onFile, onDir).toList + + lazy val reg = properties.get("ignore").map(_.replace(".","\\.").replace("*",".*").r) + // if (reg.exists(_.matches("/" + inPath.toString)) + def regfilter(f : File) : Boolean = !reg.exists(_.matches("/" + (this / source).relativize(f).toString)) val inFile = this / dim / in val inFileName = inFile.getName if (inFile.isDirectory) { @@ -128,7 +132,7 @@ class Archive(val root: File, val properties: mutable.Map[String, String], val r if (sendLog) log("leaving " + inFile) Some(result) } else None - } else if (filter(inFileName) && filterDir(inFile.up.getName)) { + } else if (filter(inFileName) && regfilter(inFile) && filterDir(inFile.up.getName)) { if (!forClean && !inFile.existsCompressed) { throw ArchiveError(id, "file does not exist: " + inFile) } else diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/FragmentExtension.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/FragmentExtension.scala index fc6c16f189..9bd456c4bc 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/FragmentExtension.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/FragmentExtension.scala @@ -7,7 +7,8 @@ import info.kwarc.mmt.api.ontology.{Binary, CustomBinary, RelationalElement, Rel import info.kwarc.mmt.api.parser.SourceRef import info.kwarc.mmt.api.symbols.{Constant, DerivedDeclaration} import info.kwarc.mmt.api.utils.{MMTSystem, XMLEscaping} -import info.kwarc.mmt.api.web.{ServerRequest, ServerResponse} +import info.kwarc.mmt.api.web.{ServerExtension, ServerRequest, ServerResponse} +import info.kwarc.mmt.stex.vollki.FullsTeXGraph import info.kwarc.mmt.stex.xhtml.HTMLParser.ParsingState import info.kwarc.mmt.stex.xhtml.{HTMLParser, OMDocHTML} //import info.kwarc.mmt.stex.xhtml.{HTMLConstant, HTMLParser, HTMLRule, HTMLTheory, HasLanguage, OMDocHTML} @@ -67,11 +68,14 @@ object FragmentExtension extends STeXExtension { body.attributes((HTMLParser.ns_html,"style")) = "background-color:white" stripMargins(doc) val border = body.add(
) - def space = scala.xml.Text(" ") border.add(Symbol ) - border.add(space) - border.add({XMLEscaping(c.path.toString)}) + border.add(" ") + border.add({XMLEscaping(c.path.toString)}) border.add(
) + if (controller.extman.get(classOf[ServerExtension]).contains(FullsTeXGraph)) { + border.add({"> Guided Tour"}) + border.add(
) + } border.add( diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/OMDocExtension.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/OMDocExtension.scala index 0a740df3da..e9c2b836e7 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/OMDocExtension.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/OMDocExtension.scala @@ -1,12 +1,14 @@ package info.kwarc.mmt.stex.Extensions +import info.kwarc.mmt.api.documents.Document import info.kwarc.mmt.api.modules.Theory +import info.kwarc.mmt.api.objects.OMFOREIGN import info.kwarc.mmt.api.ontology.{Binary, CustomBinary, RelationalElement, RelationalExtractor, Unary} import info.kwarc.mmt.api.symbols.Constant import info.kwarc.mmt.api.{NamespaceMap, Path, StructuralElement} import info.kwarc.mmt.stex.STeX import info.kwarc.mmt.stex.rules.MathStructureFeature -import info.kwarc.mmt.stex.xhtml.{CustomHTMLNode, HTMLAliasComponent, HTMLArg, HTMLArgMarker, HTMLArityComponent, HTMLAssoctypeComponent, HTMLBindTypeComponent, HTMLComp, HTMLComplexAssignment, HTMLConclusionComponent, HTMLCopyModule, HTMLDefComponent, HTMLDefiniendum, HTMLDomainComponent, HTMLDonotcopy, HTMLFrame, HTMLFromComponent, HTMLImport, HTMLIncludeproblem, HTMLInputref, HTMLLanguageComponent, HTMLMMTRule, HTMLMacroNameComponent, HTMLMetatheoryComponent, HTMLNotation, HTMLNotationComponent, HTMLNotationFragment, HTMLNotationPrec, HTMLOMA, HTMLOMBIND, HTMLOMID, HTMLOMV, HTMLParser, HTMLProblem, HTMLRealization, HTMLReorderComponent, HTMLRule, HTMLSAssertion, HTMLSDefinition, HTMLSExample, HTMLSParagraph, HTMLSProof, HTMLSProofsketch, HTMLSProofstep, HTMLSignatureComponent, HTMLSimpleAssignment, HTMLSpfcase, HTMLSpfeq, HTMLStatementNameComponent, HTMLStructuralFeature, HTMLStructureFeature, HTMLSubproof, HTMLSymbol, HTMLTheory, HTMLTheoryHeader, HTMLToComponent, HTMLTopLevelTerm, HTMLTypeComponent, HTMLTypeStringComponent, HTMLUseModule, HTMLVarComp, HTMLVarDecl, HTMLVarSeqDecl, HTMLVarStructDecl, HasHead, MathMLNode, OMDocHTML, SemanticState, SimpleHTMLRule} +import info.kwarc.mmt.stex.xhtml.{CustomHTMLNode, HTMLAliasComponent, HTMLArg, HTMLArgMarker, HTMLArityComponent, HTMLAssoctypeComponent, HTMLBindTypeComponent, HTMLComp, HTMLComplexAssignment, HTMLConclusionComponent, HTMLCopyModule, HTMLDefComponent, HTMLDefiniendum, HTMLDoctitle, HTMLDomainComponent, HTMLDonotcopy, HTMLFrame, HTMLFromComponent, HTMLImport, HTMLIncludeproblem, HTMLInputref, HTMLLanguageComponent, HTMLMMTRule, HTMLMacroNameComponent, HTMLMetatheoryComponent, HTMLNotation, HTMLNotationComponent, HTMLNotationFragment, HTMLNotationPrec, HTMLOMA, HTMLOMBIND, HTMLOMID, HTMLOMV, HTMLParser, HTMLProblem, HTMLRealization, HTMLReorderComponent, HTMLRule, HTMLSAssertion, HTMLSDefinition, HTMLSExample, HTMLSParagraph, HTMLSProof, HTMLSProofsketch, HTMLSProofstep, HTMLSignatureComponent, HTMLSimpleAssignment, HTMLSpfcase, HTMLSpfeq, HTMLStatementNameComponent, HTMLStructuralFeature, HTMLStructureFeature, HTMLSubproof, HTMLSymbol, HTMLTheory, HTMLTheoryHeader, HTMLToComponent, HTMLTopLevelTerm, HTMLTypeComponent, HTMLTypeStringComponent, HTMLUseModule, HTMLVarComp, HTMLVarDecl, HTMLVarSeqDecl, HTMLVarStructDecl, HasHead, MathMLNode, OMDocHTML, SemanticState, SimpleHTMLRule} object OMDocExtension extends DocumentExtension { @@ -86,6 +88,7 @@ object OMDocExtension extends DocumentExtension { SimpleHTMLRule("macroname",HTMLMacroNameComponent), SimpleHTMLRule("assoctype",HTMLAssoctypeComponent), SimpleHTMLRule("reorderargs",HTMLReorderComponent), + SimpleHTMLRule("doctitle",HTMLDoctitle), SimpleHTMLRule("import",HTMLImport), SimpleHTMLRule("usemodule",HTMLUseModule), SimpleHTMLRule("copymodule",HTMLCopyModule(_,false)), @@ -144,6 +147,24 @@ object OMDocExtension extends DocumentExtension { import DocumentExtension._ override lazy val documentRules = List( + {case iref : HTMLInputref => + val dp = Path.parseD(iref.resource + ".omdoc",NamespaceMap.empty) + controller.getO(dp) match { + case Some(d:Document) => + controller.backend.resolveLogical(d.path.uri) match { + case Some((a,ls)) => + val path = ls.init.mkString("/") + "/" + ls.last.dropRight(5) + "xhtml" + iref.parent.foreach(_.addAfter(
{ + d.metadata.get(STeX.meta_doctitle).headOption.map(_.value match { + case OMFOREIGN(node) => node + case _ => {d.path.toString} + }).getOrElse({d.path.toString}) + }
,iref)) + case _ => + } + case _ => + } + }, {case thm: HTMLTheory => sidebar(thm, Theory: {thm.name.toString} :: Nil) }, @@ -159,8 +180,8 @@ object OMDocExtension extends DocumentExtension { if (t.resource.startsWith("var://") || t.resource.startsWith("varseq://")) { // TODO } else { - overlay(t, "/:" + server.pathPrefix + "/fragment?" + t.head.toString + "&language=" + getLanguage(t), - "/:" + server.pathPrefix + "/declaration?" + t.head.toString + "&language=" + getLanguage(t)) + overlay(t, "/:" + server.pathPrefix + "/fragment?" + t.head.toString + "&language=" + getLanguage(t), + "/:" + server.pathPrefix + "/declaration?" + t.head.toString + "&language=" + getLanguage(t)) } }, ) diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/rules/Sequences.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/rules/Sequences.scala index d1404ce54f..d0ab166eaf 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/rules/Sequences.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/rules/Sequences.scala @@ -10,6 +10,13 @@ import info.kwarc.mmt.stex.{SCtx, SOMB, STeX, STerm} trait SeqRule { val seqexprpath : GlobalName val seqtppath : GlobalName + object SeqLike { + def apply(tm : Term) = tm match { + case STeX.flatseq(_) => true + case OMV(_) if tm.metadata.get(STeX.flatseq.sym).nonEmpty => true + case _ => false + } + } object Seqtype { def unapply(tp : Term) = tp match { case OMA(OMS(`seqtppath`),List(t)) => @@ -47,6 +54,9 @@ case class SeqInfTypeRule(seqtppath : GlobalName,seqexprpath : GlobalName) exten solver.check(Typing(stack, tm, tpA)) } (tp, Some(true)) + case Some(Seqexpr(tps)) => + // TODO ? + (tp,Some(true)) case _ => solver.inferType(h) match { case None => (None, None) diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/sTeX.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/sTeX.scala index 1808d77ec4..2e08c325ed 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/sTeX.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/sTeX.scala @@ -232,4 +232,6 @@ object STeX { val meta_quantification = mmtmeta_path ? "quantification" val meta_qforall = mmtmeta_path ? "universal" val meta_qexists = mmtmeta_path ? "existential" + + val meta_doctitle = mmtmeta_path ? "doctitle" } \ No newline at end of file diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/vollki/GraphExtensions.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/vollki/GraphExtensions.scala index 828807dd2c..224908e34e 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/vollki/GraphExtensions.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/vollki/GraphExtensions.scala @@ -4,16 +4,18 @@ import info.kwarc.mmt.api.{DPath, MPath, NamespaceMap, Path, StructuralElement} import info.kwarc.mmt.api.documents.{DRef, Document, MRef} import info.kwarc.mmt.api.frontend.{Controller, Extension} import info.kwarc.mmt.api.modules.{Theory, View} +import info.kwarc.mmt.api.objects.OMFOREIGN import info.kwarc.mmt.api.ontology.{Declares, IsDocument, IsTheory} import info.kwarc.mmt.api.symbols.DerivedDeclaration import info.kwarc.mmt.api.utils.{File, JSON, JSONArray, JSONObject, MMTSystem} import info.kwarc.mmt.api.web.{GraphSolverExtension, JGraphBuilder, JGraphEdge, JGraphExporter, JGraphNode, JGraphSelector, ServerExtension, ServerRequest, ServerResponse, StandardBuilder} import info.kwarc.mmt.stex.Extensions.DocumentExtension import info.kwarc.mmt.stex.xhtml.HTMLParser -import info.kwarc.mmt.stex.xhtml.HTMLParser.HTMLNode +import info.kwarc.mmt.stex.xhtml.HTMLParser.{HTMLNode, empty} import info.kwarc.mmt.stex.{STeX, STeXServer} import scala.collection.{Set, mutable} +import scala.xml.{Elem, Node, XML} class STeXGraphPopulator extends Extension { override def start(args: List[String]): Unit = { @@ -54,9 +56,9 @@ object FullsTeXGraph extends ServerExtension("vollki") { }) allobjects.foreach{ n => if (path.contains(n)) - entrydoc.add() + entrydoc.add() else - entrydoc.add() + entrydoc.add() } ServerResponse(doc.toString,"application/xhtml+xml") case Some("frag") => @@ -92,7 +94,7 @@ object FullsTeXGraph extends ServerExtension("vollki") { nodes.foreach { node => body.add() @@ -139,23 +141,37 @@ object FullsTeXGraph extends ServerExtension("vollki") { trait sTeXNode { val id : String def selectTopo : List[sTeXNode] - lazy val topologicalSort : List[sTeXNode] = { + def topologicalSort : List[sTeXNode] = { (selectTopo.flatMap(_.topologicalSort) ::: List(this)).distinct } - def getDocument(language : String) : Option[Document] + private def getDocumentDefinitely(language : String) = getDocument(language) match { + case Some(d) => Some(d) + case _ => getDocument("en") match { + case Some(d) => Some(d) + case _ => getDocument("") + } + } + def getTitle(language: String) : Node = getDocumentDefinitely(language).flatMap( + _.metadata.get(STeX.meta_doctitle).headOption.map(_.value match { + case OMFOREIGN(node) => node + case _ => {id} + }) + ).getOrElse({id}) + val parents = mutable.HashSet.empty[sTeXNode] + val keys = mutable.HashSet.empty[Path] + protected[FullsTeXGraph] val _documents = mutable.HashMap.empty[String,DPath] + def getDocument(language : String) : Option[Document] = _documents.get(language).flatMap(controller.getAsO(classOf[Document],_)) } class sTeXDocument(val id : String) extends sTeXNode { private[FullsTeXGraph] var _children : List[sTeXNode] = Nil def children = _children private[FullsTeXGraph] var _languages : List[String] = Nil def languages = _languages - private[FullsTeXGraph] val _documents = mutable.HashMap.empty[String,Document] - def getDocument(language : String) : Option[Document] = _documents.get(language) override def selectTopo: List[sTeXNode] = _children.reverse } - class sTeXTheory(val sig: Theory) extends sTeXNode { - val path : MPath = sig.path + class sTeXTheory(val sig: MPath) extends sTeXNode { + val path : MPath = sig val id = path.toString private[FullsTeXGraph] var _includes : List[sTeXTheory] = Nil def includes = _includes @@ -164,8 +180,6 @@ object FullsTeXGraph extends ServerExtension("vollki") { private[FullsTeXGraph] var _languages : List[String] = Nil def languages = _languages def getLanguageModule(language : String) : Option[Theory] = controller.getAsO(classOf[Theory],path.toDPath ? language) - private[FullsTeXGraph] val _documents = mutable.HashMap.empty[String,Document] - def getDocument(language : String) : Option[Document] = _documents.get(language) override def selectTopo: List[sTeXNode] = _includes.reverse } @@ -188,14 +202,16 @@ object FullsTeXGraph extends ServerExtension("vollki") { val node = new sTeXDocument(id) allobjects ::= node objects(Path.parse(id)) = node + node.keys.add(Path.parse(id)) if (lang == "") { - node._documents("") = d + node._documents("") = d.path objects(d.path) = node + node.keys.add(d.path) d.getDeclarations.foreach { case mr : MRef => - getO(mr.target).foreach(node._children ::= _) + getO(mr.target).foreach{c => node._children ::= c; c.parents.add(node)} case dr : DRef => - getO(dr.target).foreach(node._children ::= _) + getO(dr.target).foreach{c => node._children ::= c; c.parents.add(node)} case _ => } } else { @@ -203,13 +219,14 @@ object FullsTeXGraph extends ServerExtension("vollki") { controller.getO(Path.parseD(id + "." + l + ".omdoc",NamespaceMap.empty)) match { case Some(d : Document) => objects(d.path) = node - node._documents(l) = d + node.keys.add(d.path) + node._documents(l) = d.path node._languages ::= l d.getDeclarations.foreach { case mr : MRef => - getO(mr.target).foreach(node._children ::= _) + getO(mr.target).foreach{c => node._children ::= c; c.parents.add(node)} case dr : DRef => - getO(dr.target).foreach(node._children ::= _) + getO(dr.target).foreach{c => node._children ::= c; c.parents.add(node)} case _ => } case _ => @@ -229,19 +246,23 @@ object FullsTeXGraph extends ServerExtension("vollki") { val ls = pathstr.split('.') (ls.init.mkString("."),ls.last) } else (pathstr,"") - val node = new sTeXTheory(th) + val node = new sTeXTheory(th.path) allobjects ::= node objects(Path.parse(id)) = node objects(th.path) = node + node.keys.add(Path.parse(id)) + node.keys.add(th.path) if (lang == "") { - node._documents("") = d + node._documents("") = d.path objects(d.path) = node + node.keys.add(d.path) } else { all_languages.foreach {l => controller.getO(Path.parseD(id + "." + l + ".omdoc",NamespaceMap.empty)) match { case Some(d : Document) => objects(d.path) = node - node._documents(l) = d + node.keys.add(d.path) + node._documents(l) = d.path node._languages ::= l case _ => } @@ -257,6 +278,7 @@ object FullsTeXGraph extends ServerExtension("vollki") { case Some(t: Theory) => node._languages ::= s objects(t.path) = node + node.keys.add(t.path) t.getAllIncludesWithoutMeta.flatMap(i => getO(i.from)).filter(_ != node).foreach { case ch : sTeXTheory => node._uses ::= ch } @@ -266,6 +288,7 @@ object FullsTeXGraph extends ServerExtension("vollki") { node._uses = node._uses.distinct th.getAllIncludesWithoutMeta.flatMap(i => getO(i.from)).foreach{ case ch : sTeXTheory => node._includes ::= ch + ch.parents.add(node) } } @@ -319,9 +342,10 @@ object FullsTeXGraph extends ServerExtension("vollki") { case Some(d: Document) => checkDoc(d) match { case Some(_) => doThDoc(th, d) case _ => - val st = new sTeXTheory(th) + val st = new sTeXTheory(th.path) allobjects ::= st objects(p) = st + st.keys.add(p) getO(d.path).foreach { case doc: sTeXDocument => doc._documents.foreach { case (k, v) => st._documents(k) = v } @@ -333,7 +357,7 @@ object FullsTeXGraph extends ServerExtension("vollki") { None } case _ => - ??? + None } case List(_) if all_languages.contains(th.name.toString) => getO(th.path.parent.toMPath) @@ -380,7 +404,7 @@ object STeXGraph extends JGraphExporter("stexgraph") { override val id: String = th.id override val style: String = "theory" override val label: Option[String] = Some(th.sig.name.toString) - override val uri: Option[String] = Some(th.sig.path.toString) + override val uri: Option[String] = Some(th.sig.toString) } case doc : FullsTeXGraph.sTeXDocument => doc.children.foreach{n => diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/xhtml/XHTML.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/xhtml/XHTML.scala index b54c1b6291..b42fee71dc 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/xhtml/XHTML.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/xhtml/XHTML.scala @@ -203,7 +203,7 @@ object HTMLParser { elem } - private[HTMLParser] def present(n : HTMLNode,indent : Int = 0) : String = { + private[HTMLParser] def present(n : HTMLNode,indent : Int = 0,forcenamespace : Boolean = false) : String = { {if (_top.contains(n)) header else ""} + { if (n.startswithWS) "\n" + {if (indent>0) (0 until indent).map(_ => " ").mkString else ""} else "" @@ -212,7 +212,7 @@ object HTMLParser { t.toString() + {if(t.endswithWS) "\n" else ""} case _ => "<" + n.label + { - if (!n._parent.exists(_.namespace == n.namespace)) " xmlns=\"" + n.namespace + "\"" else "" + if (!n._parent.exists(_.namespace == n.namespace) || forcenamespace) " xmlns=\"" + n.namespace + "\"" else "" } + { if (_top.contains(n)) namespaces.toList.map { case (p,v) => " xmlns:" + p + "=\"" + v + "\"" @@ -223,7 +223,7 @@ object HTMLParser { else if (namespaces.values.toList.contains(ns)) " " + namespaces.toList.collectFirst{case p if p._2 == ns => p._1}.get + ":" else " " + ns + ":" - } + key + "=\"" + XMLEscaping(value) + "\"" + } + key + "=\"" + value.replace("\"","\'") + "\"" }.mkString + { if (n._sourceref.isDefined && !n._parent.exists(_._sourceref == n._sourceref)) " " + "stex:sourceref=\"" + n._sourceref.get.toString + "\"" else "" } + { @@ -240,7 +240,7 @@ object HTMLParser { } } - class HTMLNode(var state : ParsingState, val namespace : String, val label : String) { + class HTMLNode(var state : ParsingState, val namespace : String, var label : String) { override def toString: String = state.present(this) val attributes = mutable.Map.empty[(String, String), String] @@ -255,6 +255,14 @@ object HTMLParser { ret } + def plaincopy: HTMLNode = { + val ret = new HTMLNode(state, namespace, label) + ret.classes = classes + attributes.foreach(e => ret.attributes(e._1) = e._2) + children.foreach(c => ret.add(c.plaincopy)) + ret + } + def parent = _parent private[HTMLParser] var _children: List[HTMLNode] = Nil @@ -414,7 +422,7 @@ object HTMLParser { } def node = try { - XML.loadString(this.toString.trim) + XML.loadString(state.present(this,forcenamespace=true).trim) } catch { case o => println(o.toString) @@ -424,12 +432,15 @@ object HTMLParser { } class HTMLText(state : ParsingState, val text : String) extends HTMLNode(state,"","") { - override def toString() = text.replaceAll("&","&").replaceAll("<","<").replaceAll(">",">").replaceAll("\"",""") + override def toString() = text//.replaceAll("&","&").replaceAll("<","<").replaceAll(">",">").replaceAll("\"",""") override def isEmpty = toString() == "" || toString() == empty.toString override def copy : HTMLText = { new HTMLText(state,text) } + override def plaincopy : HTMLText = { + new HTMLText(state,text) + } } object HTMLNode { @@ -536,10 +547,10 @@ object HTMLParser { case c => var txt = c + in.takeWhileSafe(_ != '<') val endWS = txt.lastOption.exists(_.isWhitespace) - txt = if (txt.trim == empty.toString) empty.toString else Try(XMLEscaping.unapply(txt.trim)).toOption.getOrElse({ + txt = if (txt.trim == empty.toString) empty.toString else txt.trim/*Try(XMLEscaping.unapply(txt.trim)).toOption.getOrElse({ print("") txt.trim - }) + })*/ if (txt.nonEmpty) { val n = new HTMLText(state, txt) n.startswithWS = startWS diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/xhtml/XHTMLOMDoc.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/xhtml/XHTMLOMDoc.scala index c8c991f643..918849340c 100644 --- a/src/mmt-stex/src/info/kwarc/mmt/stex/xhtml/XHTMLOMDoc.scala +++ b/src/mmt-stex/src/info/kwarc/mmt/stex/xhtml/XHTMLOMDoc.scala @@ -6,7 +6,7 @@ import info.kwarc.mmt.api.metadata.MetaDatum import info.kwarc.mmt.api.modules.{AbstractTheory, Theory} import info.kwarc.mmt.api.notations.NotationContainer import info.kwarc.mmt.api.{AddError, ComplexStep, ContentPath, DPath, GeneratedDRef, GlobalName, LocalName, MPath, NamespaceMap, Path, Rule, RuleSet, StructuralElement} -import info.kwarc.mmt.api.objects.{Context, OMA, OMAorAny, OMBIND, OMBINDC, OMID, OMIDENT, OMMOD, OMS, OMV, Obj, Term, VarDecl} +import info.kwarc.mmt.api.objects.{Context, OMA, OMAorAny, OMBIND, OMBINDC, OMFOREIGN, OMID, OMIDENT, OMMOD, OMS, OMV, Obj, Term, VarDecl} import info.kwarc.mmt.api.parser.SourceRef import info.kwarc.mmt.api.symbols.{Constant, DerivedDeclaration, Include, NestedModule, PlainInclude, RuleConstant, Structure, TermContainer} import info.kwarc.mmt.stex.Extensions.NotationExtractor @@ -376,8 +376,12 @@ case class HTMLDefComponent(orig:HTMLParser.HTMLNode) extends OMDocHTML(orig) { hd.df = findTerm true case hd : HasDefinientia => - val gn = Path.parseS(resource) - findTerm.foreach(hd.dfs(gn) = _) + resource.split(',').foreach {r => + if (r.nonEmpty) { + val gn = Path.parseS(r) + findTerm.foreach(hd.dfs(gn) = _) + } + } true } } @@ -881,7 +885,7 @@ case class HTMLArg(orig : HTMLParser.HTMLNode) extends OMDocHTML(orig) { } } -case class HTMLTopLevelTerm(orig : OMDocHTML) extends OMDocHTML(orig) with HTMLConstant { +final case class HTMLTopLevelTerm(orig : OMDocHTML) extends OMDocHTML(orig) with HTMLConstant { assert(sstate.forall(!_.in_term)) sstate.foreach(_.in_term = true) @@ -1000,6 +1004,22 @@ case class HTMLSParagraph(orig : HTMLParser.HTMLNode) extends OMDocHTML(orig) wi if (typestrings.contains("symdoc")) addSymbolDoc(fors) } } + +case class HTMLDoctitle(orig : HTMLParser.HTMLNode) extends OMDocHTML(orig) { + override def onAdd = { + super.onAdd + collectAncestor { + case d : HTMLDocument => d + }.foreach { d => + val nnode = this.plaincopy + nnode.label = "span" + nnode.classes = Nil + nnode.attributes.clear() + d.doc.metadata.update(STeX.meta_doctitle,OMFOREIGN(nnode.node)) + } + } +} + case class HTMLSAssertion(orig : HTMLParser.HTMLNode) extends OMDocHTML(orig) with HTMLStatement { var conc : Option[Term] = None override def onAdd = {sstate.foreach{ state => if (name.nonEmpty) { collectAncestor { From 2892eaecc3e7de62d322c80f772fbc5acb4c4b5b Mon Sep 17 00:00:00 2001 From: Florian Rabe Date: Wed, 4 May 2022 13:50:34 +0200 Subject: [PATCH 2/4] no message --- .../src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala b/src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala index 67f22baa1e..381f81c8d8 100644 --- a/src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala +++ b/src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala @@ -327,7 +327,7 @@ object TheoryExp { * @param all if false, stop after the first meta-theory, true by default */ def metas(thy: Term, all: Boolean = true)(implicit lib: Lookup): List[MPath] = thy match { - case OMMOD(p) => + case OMPMOD(p,_) => val t = lib.getAs(classOf[AbstractTheory],p) t.meta match { case None => From fb9bbc5a4079b82b068d50059bc9c6dc84416562 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dennis=20M=C3=BCller?= Date: Wed, 4 May 2022 15:27:29 +0200 Subject: [PATCH 3/4] tests --- .github/workflows/CI.yml | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/.github/workflows/CI.yml b/.github/workflows/CI.yml index 3d0d8e93b8..593b86a942 100644 --- a/.github/workflows/CI.yml +++ b/.github/workflows/CI.yml @@ -79,3 +79,35 @@ jobs: run: | java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }} java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl + + - name: Test '${{ env.MMT_ARCHIVE }}' + if: always() && steps.setup.outcome == 'success' + env: + MMT_ARCHIVE: 'MMT/LFX' + run: | + java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }} + java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl + + - name: Test '${{ env.MMT_ARCHIVE }}' + if: always() && steps.setup.outcome == 'success' + env: + MMT_ARCHIVE: 'Test/General' + run: | + java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }} + java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl + + - name: Test '${{ env.MMT_ARCHIVE }}' + if: always() && steps.setup.outcome == 'success' + env: + MMT_ARCHIVE: 'MitM/Foundation' + run: | + java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }} + java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl + + - name: Test '${{ env.MMT_ARCHIVE }}' + if: always() && steps.setup.outcome == 'success' + env: + MMT_ARCHIVE: 'MitM/Core' + run: | + java -jar ./deploy/mmt.jar lmh install ${{ env.MMT_ARCHIVE }}@${{ env.MMT_ARCHIVE_VERSION }} + java -jar ./deploy/mmt.jar :file ${{ env.MMT_ARCHIVE_ROOT }}/${{ env.MMT_ARCHIVE }}/build.msl From e23b73d980caa593f001f9431dcb7219cbfcdb27 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Dennis=20M=C3=BCller?= Date: Wed, 4 May 2022 20:43:31 +0200 Subject: [PATCH 4/4] bump up version number --- src/mmt-api/resources/versioning/system.txt | 2 +- src/project/build.properties | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mmt-api/resources/versioning/system.txt b/src/mmt-api/resources/versioning/system.txt index fb5b513039..1d975bef24 100644 --- a/src/mmt-api/resources/versioning/system.txt +++ b/src/mmt-api/resources/versioning/system.txt @@ -1 +1 @@ -21.0.0 +22.0.0 diff --git a/src/project/build.properties b/src/project/build.properties index 0837f7a132..c8fcab543a 100644 --- a/src/project/build.properties +++ b/src/project/build.properties @@ -1 +1 @@ -sbt.version=1.3.13 +sbt.version=1.6.2
MacroPresentationType
- {"> " + node.id} + {"> "}{node.getTitle(language)}