Skip to content

Commit

Permalink
tabbed multiple definitions in on-click for sTeX + bug fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@Jazzpirate
Jazzpirate committed Sep 24, 2023
1 parent 9a67c1d commit 85c6360
Show file tree
Hide file tree
Showing 8 changed files with 245 additions and 185 deletions.
4 changes: 2 additions & 2 deletions src/mmt-api/resources/mmt-web/stex/mmt-viewer/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@
<meta charset="utf-8" />
<title>sTeX Viewer</title>
<meta name="viewport" content="width=device-width, initial-scale=1" />
<link rel="icon" type="image/x-icon" href="favicon.ico" />
<link rel="icon" type="image/x-icon" href="/stex/mmt-viewer/favicon.ico" />
<link rel="stylesheet" href="/stex/mmt-viewer/styles.17b9ee704abcc86c.css"><link rel="stylesheet" href="/stex/mmt-viewer/main.420346012a7e8d87.css">
<link rel="stylesheet" href="CONTENT_CSS_PLACEHOLDER">
<link rel="stylesheet" href="/stex/fonts.css">
Expand All @@ -39,6 +39,6 @@

<body>
<div id="root"></div>
<script src="/stex/mmt-viewer/runtime.ef661e1f8606875b.js" type="module"></script><script src="/stex/mmt-viewer/styles.97c1288dfae7ac4e.js" type="module"></script><script src="/stex/mmt-viewer/main.a7de4abe6131954b.js" type="module"></script></body>
<script src="/stex/mmt-viewer/runtime.ef661e1f8606875b.js" type="module"></script><script src="/stex/mmt-viewer/styles.97c1288dfae7ac4e.js" type="module"></script><script src="/stex/mmt-viewer/main.f7e3ca12f00f4bfe.js" type="module"></script></body>

</html>
154 changes: 0 additions & 154 deletions src/mmt-api/resources/mmt-web/stex/mmt-viewer/main.a7de4abe6131954b.js
View file

This file was deleted.

154 changes: 154 additions & 0 deletions src/mmt-api/resources/mmt-web/stex/mmt-viewer/main.f7e3ca12f00f4bfe.js
View file

Large diffs are not rendered by default.

6 changes: 5 additions & 1 deletion src/mmt-api/resources/mmt-web/stex/mmt-viewer/styles.17b9ee704abcc86c.css
View file

Large diffs are not rendered by default.

67 changes: 54 additions & 13 deletions src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/DocumentExtension.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import info.kwarc.mmt.api.archives.{Archive, RedirectableDimension}
import info.kwarc.mmt.api.documents.{DRef, Document}
import info.kwarc.mmt.api.frontend.Controller
import info.kwarc.mmt.api.objects.{OMA, OMFOREIGN, OMID, OMMOD, OMS, Term}
import info.kwarc.mmt.api.ontology.ULO
import info.kwarc.mmt.api.opaque.OpaqueXML
import info.kwarc.mmt.api.parser.SourceRef
import info.kwarc.mmt.api.symbols.Constant
Expand All @@ -25,17 +26,38 @@ import scala.xml.parsing.XhtmlParser
import scala.xml.{Elem, Node}

trait SHTMLDocumentServer { this : STeXServer =>

def parseLanguage(s: String) = {
var ds = s
if (ds.endsWith(".omdoc")) ds = ds.dropRight(6)
if (ds.endsWith(".xhtml")) ds = ds.dropRight(6)
if (ds.endsWith(".tex")) ds = ds.dropRight(4)
ds.split('.').lastOption
}
protected case class DocParams(q: WebQuery) {
lazy val path = q.pairs.find(p => p._2.isEmpty && p._1.contains('?') && !p._1.endsWith("="))
.map(p => Path.parse(p._1))
lazy val language = q("language")
lazy val language = q("language").orElse(context_filepath.flatMap(parseLanguage))
lazy val archive = q("archive").flatMap{id => getArchive(id)}
lazy val filepath = q("filepath")
lazy val bindings = {
val bnds = q("bindings").map(LateBinding.fromNum)
log("Bindings: " + q("bindings") + " --> " + bnds.map(_.toString).getOrElse("None"))
bnds
}
private lazy val ctx = q("contextUrl").flatMap{s =>
(s.indexOf("archive="),s.indexOf("filepath=")) match {
case (-1,_)|(_,-1) => None
case (i,j) => Some((s.drop(i),s.drop(j)))
}
}
lazy val context_archive = q("contextArchive").flatMap(getArchive)
lazy val context_filepath = q("contextFilepath")
lazy val context_doc = (context_archive,context_filepath) match {
case (Some(a),Some(fp)) =>
Some(DPath(a.narrationBase / fp.replace(".tex",".omdoc").replace(".xhtml",".omdoc")))
case _ => None
}
}
private case class ErrorResponse(message:String) extends Throwable
protected def documentRequest(request: ServerRequest) : ServerResponse = try {
Expand Down Expand Up @@ -404,20 +426,20 @@ trait SHTMLDocumentServer { this : STeXServer =>
val (_, body) = this.emptydoc
body.add(doDeclHeader(c))
Try(getAllFragments).toOption match {
case Some(htm :: Nil) =>
case Some((htm,_) :: Nil) =>
body.add(<hr/>)
body.add(htm)
case Some(ls) =>
val id = ls.hashCode().toHexString;
body.add(<hr/>)
val nhtml = body.add("<ul class=\"shtml-declaration-tabs\"/>")
val nls = ls.zipWithIndex.map{case (node,i) =>
val nls = ls.zipWithIndex.map{case ((node,label),i) =>
val li = nhtml.add("<li class=\"shtml-declaration-tab\"/>")
if (i == 0)
li.add(s"<input type=\'radio\' name=\'tabs\' id=\'$id\' checked=\'checked\'/><label for=\'$id\'>1</label>")
li.add(s"<input type=\'radio\' name=\'tabs\' id=\'$id\' checked=\'checked\'/><label for=\'$id\'>$label</label>")
else {
val nid = id + i.toString
li.add(s"<input type=\'radio\' name=\'tabs\' id=\'$nid\'/><label for=\'$nid\'>${i+1}</label>")
li.add(s"<input type=\'radio\' name=\'tabs\' id=\'$nid\'/><label for=\'$nid\'>$label</label>")
}
val inner = li.add("<div class=\"shtml-declaration-tab-content\"/>")
inner.add(node)
Expand Down Expand Up @@ -490,7 +512,7 @@ trait SHTMLDocumentServer { this : STeXServer =>
case Some(elem) =>
elem match {
case c: Constant =>
getAllFragmentsDefault(c).map(f => present(f)(dp.bindings))
getAllFragmentsDefault(c).map(f => (present(f._1)(dp.bindings),f._2))
case _ =>
throw ErrorResponse("No symbol with path " + path + " found")
}
Expand Down Expand Up @@ -522,8 +544,8 @@ trait SHTMLDocumentServer { this : STeXServer =>
}
}

def getAllFragmentsDefault(c : Constant)(implicit dp:DocParams) : List[String] = {
SHTMLContentManagement.getSymdocs(c.path, dp.language.getOrElse("en"))(controller) match { // TODO language
def getAllFragmentsDefault(c : Constant)(implicit dp:DocParams) : List[(String,String)] = {
SHTMLContentManagement.getSymdocs(c.path, dp.language.getOrElse("en"),dp.context_doc)(controller) match { // TODO language
case Nil =>
val res = "Symbol <b>" + c.name + "</b> in module " + (SourceRef.get(c) match {
case Some(sr) =>
Expand All @@ -536,15 +558,32 @@ trait SHTMLDocumentServer { this : STeXServer =>
}
case _ => c.parent.name.toString
})
List("<div>" + res + "</div>")
case a => a.map(_.toString())
List(("<div>" + res + "</div>",""))
case a =>
sort(a).zipWithIndex.map{
case ((gn,n),i) =>
val language = gn.module.name.toString
controller.backend.resolveLogical(gn.module.doc.uri) match {
case None => (n.toString(),language)
case Some((a,_)) =>
(n.toString(),s"${a.id} ($language)")
}
}
}
}

def sort(defs:List[(GlobalName,Node)])(implicit dp:DocParams): List[(GlobalName,Node)] = {
dp.language match {
case None => defs
case Some(lang) =>
val ls = defs.filter(_._1.module.name.toString == lang)
if (ls.isEmpty) defs else (ls ::: defs).distinct
}
}

def getFragmentDefault(c : Constant)(implicit dp:DocParams) : String = {
SHTMLContentManagement.getSymdocs(c.path,dp.language.getOrElse("en"))(controller) match { // TODO language
case a :: _ => a.toString()
case _ =>
SHTMLContentManagement.getSymdocs(c.path,dp.language.getOrElse("en"),dp.context_doc)(controller) match { // TODO language TODO sort by relevance
case Nil =>
val res = "Symbol <b>" + c.name + "</b> in module " + (SourceRef.get(c) match {
case Some(sr) =>
controller.backend.resolveLogical(sr.container) match {
Expand All @@ -557,6 +596,8 @@ trait SHTMLDocumentServer { this : STeXServer =>
case _ => c.parent.name.toString
})
"<div>" + res + "</div>"
case ls =>
sort(ls).head._2.toString()
}
}

Expand Down
31 changes: 23 additions & 8 deletions src/mmt-stex/src/info/kwarc/mmt/stex/Extensions/SHTMLContentManagement.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -235,23 +235,38 @@ object SHTMLContentManagement {
//parent.metadata.add(MetaDatum(meta_symdoc, OMA(OMS(meta_symdoc), StringLiterals(language) :: OMFOREIGN(node) :: fors.map(OMS(_)))))
}

def getSymdocs(sym: ContentPath, language: String)(implicit controller:Controller): List[Node] = {
def getSymdocs(sym: ContentPath, language: String,context:Option[DPath])(implicit controller:Controller): List[(GlobalName,Node)] = {
import info.kwarc.mmt.api.ontology.SPARQL._
val paths = controller.depstore.query(
SELECT("x") WHERE (T(sym,ULO.docref,V("x")) UNION T(V("x"),ULO.defines,sym))
).getPaths

val paths = context match {
case Some(docpath) =>
val first = controller.depstore.query(
SELECT("x") WHERE (
T(docpath,ULO.specifies | ULO.contains,V("x")) AND (
T(sym, ULO.docref, V("x")) UNION T(V("x"), ULO.defines, sym)
))
).getPaths
val second = controller.depstore.query(
SELECT("x") WHERE (T(sym, ULO.docref, V("x")) UNION T(V("x"), ULO.defines, sym))
).getPaths
(first ::: second).distinct
case None => controller.depstore.query(
SELECT("x") WHERE (T(sym, ULO.docref, V("x")) UNION T(V("x"), ULO.defines, sym))
).getPaths
}

val constants = paths.flatMap(controller.getO).collect {
case c : Constant if c.df.isDefined =>
/*val deps = controller.depstore.query(
SELECT("y") WHERE
T(c.path,(ULO.crossrefs | ULO.declares)+,V("y"))
)
deps.getPaths.foreach(println)*/
c.df.get
}
constants.collect {
case OMA(OMS(_),OMFOREIGN(node) :: _) => node
(c.path,c.df.get)
}.distinct
constants.collect {
case (p,OMA(OMS(_),OMFOREIGN(node) :: _)) => (p,node)
}
}

def addExample(path:GlobalName,fors:List[GlobalName],node:Node,controller:Controller,rel:ULOStatement => Unit) = {
Expand Down
2 changes: 1 addition & 1 deletion src/mmt-stex/src/info/kwarc/mmt/stex/lsp/Server.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -872,7 +872,7 @@ object Main {
controller.handleLine(s"server on ${port} ${ip}")
while (controller.server.isEmpty) {
port += 1
controller.handleLine("server on ${port} ${ip}")
controller.handleLine(s"server on ${port} ${ip}")
}
val end = new STeXLSP
controller.extman.get(classOf[BuildManager]).foreach(controller.extman.removeExtension)
Expand Down
12 changes: 6 additions & 6 deletions src/mmt-stex/src/info/kwarc/mmt/stex/vollki/GraphExtensions.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,8 @@ class VollKi(server:STeXServer) extends ServerExtension("vollki") {
case Some("frag") =>
path match {
case Some(gn : GlobalName) =>
SHTMLContentManagement.getSymdocs(gn, language)(controller).headOption match {
case Some(ht) => ServerResponse(present(ht.toString())(None).toString.trim, "text/html")
SHTMLContentManagement.getSymdocs(gn, language,None)(controller).headOption match {
case Some((_,ht)) => ServerResponse(present(ht.toString())(None).toString.trim, "text/html")
case _ => ServerResponse("Document not found: " + path.getOrElse("(None)"), "text/plain")
}
case _ => ServerResponse("Document not found: " + path.getOrElse("(None)"), "text/plain")
Expand All @@ -62,10 +62,10 @@ class VollKi(server:STeXServer) extends ServerExtension("vollki") {
case Some("deps") =>
path match {
case Some(p:GlobalName) =>
SHTMLContentManagement.getSymdocs(p, language)(controller).headOption match {
SHTMLContentManagement.getSymdocs(p, language,None)(controller).headOption match {
case None =>
ServerResponse.JsonResponse(JSONArray())
case Some(doc) =>
case Some((_,doc)) =>
val html = HTMLParser(doc.toString())(new ParsingState(controller, Nil))
var syms: List[GlobalName] = Nil
html.iterate { n =>
Expand Down Expand Up @@ -112,8 +112,8 @@ class VollKi(server:STeXServer) extends ServerExtension("vollki") {
}
class Deps(val symbol:GlobalName) {
var dependencies : Set[Deps] = Set.empty
lazy val doc = SHTMLContentManagement.getSymdocs(symbol,language)(controller).headOption
lazy val html = doc.map{d =>
lazy val doc = SHTMLContentManagement.getSymdocs(symbol,language,None)(controller).headOption
lazy val html = doc.map{case (_,d) =>
HTMLParser(d.toString())(new ParsingState(controller, Nil))
}
def transitive: Set[GlobalName] = {
Expand Down

0 comments on commit 85c6360

Please sign in to comment.