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 fb0878c92..446a48acd 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 @@ -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 index c8d67dc2b..dee7b0e8f 100644 --- 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)