| Macro | Presentation | Type | |
|---|
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(,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(
|
- {"> " + node.id}
+ {"> "}{node.getTitle(language)}
|
)
@@ -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 {
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