sTeX fix for out-of-memory-problem; URIs for definienda

UniFormal · Dec 11, 2023 · 795778c · 795778c
1 parent 3ef072c
commit 795778c
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 2 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
@@ -395,6 +395,11 @@ trait SHTMLDocumentServer { this : STeXServer =>
         e.plain.classes ::= "varcomp" // TODO
       } else if (hasAttribute(e,"definiendum")) {
         e.plain.classes ::= "definiendum" // TODO
+        elem.plain.attributes.get((HTMLParser.ns_mmt,"definiendum")) match {
+          case Some(str) =>
+            e.plain.attributes((elem.namespace, "data-definiendum-uri")) = str
+          case _ =>
+        }
       }
     }
   }

diff --git a/src/mmt-stex/src/info/kwarc/mmt/stex/LaTeXBuildTarget.scala b/src/mmt-stex/src/info/kwarc/mmt/stex/LaTeXBuildTarget.scala
@@ -544,11 +544,17 @@ class FullsTeX extends Importer with XHTMLParser {
         ilog("    -      bibtex " + bt.inPath)
         Process(Seq("bibtex",pdffile.stripExtension.getName),pdffile.up).lazyLines_!
       }
+      val usesms = {
+        val sms = bt.inFile.setExtension("sms")
+        if (sms.exists() && sms.toJava.length() < 2097152) {
+          Seq(("STEX_USESMS","true"))
+        } else Seq()
+      }
       ilog("    -    pdflatex " + bt.inPath + " (second run)")
-      buildSingle(bt,("STEX_USESMS","true"))
+      buildSingle(bt,usesms:_*)
       bt.outFile.delete()
       ilog("    -    pdflatex " + bt.inPath + " (final run)")
-      buildSingle(bt,("STEX_USESMS","true"))
+      buildSingle(bt,usesms:_*)
       bt.outFile.delete()
       ilog("    -       omdoc " + bt.inPath)
       val (errored,texerrored,_) = buildFileActually(bt.archive,bt.inFile, outFile, state, bt.errorCont)