Merge pull request #568 from UniFormal/devel

Devel
UniFormal · May 4, 2022 · bed907f · bed907f
2 parents 5730190 + e23b73d
commit bed907f
Show file tree

Hide file tree

Showing 16 changed files with 184 additions and 57 deletions.
diff --git 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
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
@@ -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
@@ -5,7 +5,6 @@
     <link rel="stylesheet" href="/stex/htmlfragments/sidenotes.css"/>
     <link rel="stylesheet" href="/stex/htmlfragments/overlay.css"/>
     <script type="text/javascript" id="overlayjs" src="/stex/htmlfragments/overlay.js">&#8205;</script>
-    <!--<script type="text/javascript" id="MathJax-fix" src="/stex/htmlfragments/mathjax-fix.js">&#8205;</script>
+    <script type="text/javascript" id="MathJax-fix" src="/stex/htmlfragments/mathjax-fix.js">&#8205;</script>
     <script type="text/javascript" id="MathJax-script" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/mml-chtml.js">&#8205;</script>
-    -->
 </head>
diff --git 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
@@ -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 + "&amp;user=" + user.options[user.selectedIndex].value + "&amp;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 &amp;&amp; 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 + "&amp;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 &amp;&amp; xhr.status == 200) {
                     elem.innerHTML = xhr.responseText;
                     elem.style.display = 'flex';
                     MathJax.Hub.Queue(["Typeset",MathJax.Hub]);

diff --git 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/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-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 => 

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
@@ -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(<div style="font-size:small"/>)
-        def space = scala.xml.Text("&nbsp;")
         border.add(<b>Symbol </b>)
-        border.add(space)
-        border.add(<a href={"/?"+path} target="_blank">{XMLEscaping(c.path.toString)}</a>)
+        border.add("&nbsp;")
+        border.add(<a href={"/?"+path} target="_blank" style="pointer-events:all">{XMLEscaping(c.path.toString)}</a>)
         border.add(<br/>)
+        if (controller.extman.get(classOf[ServerExtension]).contains(FullsTeXGraph)) {
+          border.add(<a href={"/:vollki?path=" + c.parent.toString} target="_blank" style="pointer-events:all;color:blue">{"> Guided Tour"}</a>)
+          border.add(<br/>)
+        }
         border.add(
           <table>
             <tr><th>Macro</th><th>Presentation</th><th>Type</th><th></th></tr>

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
@@ -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(<div><a href={"/:" + server.pathPrefix + "/browser?archive=" + a.id + "&filepath="  + path} style="pointer-events:all;color:blue">{
+                  d.metadata.get(STeX.meta_doctitle).headOption.map(_.value match {
+                    case OMFOREIGN(node) => node
+                    case _ => <span>{d.path.toString}</span>
+                  }).getOrElse(<span>{d.path.toString}</span>)
+                }</a></div>,iref))
+            case _ =>
+          }
+        case _ =>
+      }
+    },
     {case thm: HTMLTheory =>
       sidebar(thm, <b style="font-size: larger">Theory: {thm.name.toString}</b> :: 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 + "&amp;language=" + getLanguage(t),
+          "/:" + server.pathPrefix + "/declaration?" + t.head.toString  + "&amp;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
@@ -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
@@ -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"
 }