Merge remote-tracking branch 'origin/devel' into frameit-multiplayer

.gitignore

@@ -37,6 +37,7 @@ target
 out/
 
 .DS_Store
+*~
 
 # Artifact of https://github.com/coursier/coursier when working with IntelliJ
 src/null

src/build.sbt

@@ -176,7 +176,18 @@ lazy val src = (project in file(".")).
     // add the test folder to the test sources
     // but don't actually run any of them
     Test / scalaSource := baseDirectory.value / "test",
-    test := {}
+    test := {},
+
+    // This silences a dependency semver version conflict from the frameit project.
+    // It is necessary to have this silencing mechanism both in the frameit project
+    // and here in the super project (I guess because the version conflict somehow
+    // bubbles up?)
+    libraryDependencySchemes ++= Seq(
+      // see https://github.com/circe/circe-iteratee/issues/261
+      "io.circe" %% "circe-jawn" % VersionScheme.Always,
+      // see https://github.com/sbt/sbt/issues/7140#issuecomment-1464119328
+      "io.circe" % "circe-jawn_2.13" % VersionScheme.Always
+    )
   )
 
 // This is the main project. 'mmt/deploy' compiles all relevants subprojects, builds a self-contained jar file, and puts into the deploy folder, from where it can be run.
@@ -443,6 +454,9 @@ lazy val frameit = (project in file("frameit-mmt"))
       //  https://github.com/circe/circe-generic-extras/issues/279)
     ),
 
+    // This silences a dependency semver version conflict.
+    // It is necessary to have this silencing mechanism both here and in the super project src
+    // (I guess because the version conflict somehow bubbles up?)
     libraryDependencySchemes ++= Seq(
       // see https://github.com/circe/circe-iteratee/issues/261
       "io.circe" %% "circe-jawn" % VersionScheme.Always,
@@ -464,7 +478,6 @@ lazy val frameit = (project in file("frameit-mmt"))
     Compile / mainClass  := Some("info.kwarc.mmt.frameit.communication.server.Server"),
     assembly / mainClass := Some("info.kwarc.mmt.frameit.communication.server.Server")
   )
-
 
 // plugin for mathscheme-related functionality. Obsolete
 lazy val mathscheme = (project in file("mmt-mathscheme")).

src/frameit-mmt/src/info/kwarc/mmt/frameit/business/datastructures/Fact.scala

@@ -72,14 +72,14 @@ sealed case class Fact(
   private def _toSimple(implicit ctrl: Controller): SFact = {
     val simplify: Term => Term = {
       val ctx = Context(ref.uri.module) ++ additionalContext
-      val simplificationRules: RuleSet = {
+      val simplificationRules: RuleSet = Fact.ruleCache.computeIfAbsent(ctx, _ => {
         val rules = RuleSet.collectRules(ctrl, ctx)
         rules.add(new LabelVerbalizationRule()(ctrl.globalLookup))
 
         rules
-      }
+      })
 
-      val simplicationUnit = SimplificationUnit(ctx, expandVarDefs = true, expandConDefs = true, fullRecursion = true)
+      val simplicationUnit = SimplificationUnit(ctx, expandVarDefs = true, expandConDefs = true, fullRecursion = false)
 
       ctrl.simplifier(_, simplicationUnit, simplificationRules)
     }
@@ -101,9 +101,16 @@ sealed case class Fact(
 
 object Fact {
   /**
-    * A cache to speed up [[Fact.toSimple]].
+    * A cache to speed up [[Fact.toSimple]] when one and the same fact is simplified over again.
     */
   private val sfactCache: ConcurrentHashMap[Fact, SFact] = new ConcurrentHashMap
+  /**
+    * A cache to speed up [[Fact.toSimple]] when facts are simplified in one and the same context (most likely the
+    * problem or solution theory).
+    * The cache stores [[RuleSet RuleSets]] because redundantly calling [[RuleSet.collectRules]] every time as part of
+    * [[Fact.toSimple]] is slow.
+    */
+  private val ruleCache: ConcurrentHashMap[Context, RuleSet] = new ConcurrentHashMap
 
   def fromConstant(c: Constant)(implicit ctrl: Controller): Fact = Fact(
     FactReference(c.path),

src/mmt-api/resources/mmt-web/stex/mmt-viewer/3rdpartylicenses.txt

@@ -473,16 +473,6 @@ IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
 CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 
 
-@stex-react/api
-
-@stex-react/comments
-
-@stex-react/markdown
-
-@stex-react/mathjax
-
-@stex-react/react-utils
-
 @stex-react/source
 GNU AGPL
 GNU AFFERO GENERAL PUBLIC LICENSE
@@ -1148,10 +1138,6 @@ For more information on this, and how to apply and follow the GNU AGPL, see
 <http://www.gnu.org/licenses/>.
 
 
-@stex-react/stex-react-renderer
-
-@stex-react/utils
-
 axios
 MIT
 # Copyright (c) 2014-present Matt Zabriskie & Collaborators

src/mmt-api/resources/mmt-web/stex/mmt-viewer/index.html

@@ -8,12 +8,14 @@
       window.BASE_URL = 'BASE_URL_PLACEHOLDER';
       // If 'SHOW_FILE_BROWSER' is set to 'TRUE', then the filebrowser is displayed and all other values are ignored.
       window.SHOW_FILE_BROWSER = 'SHOW_FILE_BROWSER_PLACEHOLDER';
+      // If USE_EMBEDDED is true, it uses the html it renders the content in 'embedding' element of this doc. 'CONTENT_URL' is ignored.
+      window.USE_EMBEDDED = 'FALSE';
       // Eg. /:sTeX/document?archive=MiKoMH/GenCS&filepath=dmath/mod/addition-function.en.xhtml
       // NOTE: CONTENT_URL must be empty if tours are to be displayed.
       window.CONTENT_URL = 'CONTENT_URL_PLACEHOLDER';
       // Eg. http://mathhub.info/smglom/sets/mod?subsupset
       window.TOUR_ID = 'TOUR_ID_PLACEHOLDER';
-      // Eg. en
+      // Eg. en or de
       window.LANGUAGE = 'LANGUAGE_PLACEHOLDER';
       // Eg. If 'NO_FRILLS' is set to 'TRUE', the sidepanel etc will not be shown
       window.NO_FRILLS = 'NO_FRILLS_PLACEHOLDER';
@@ -24,13 +26,19 @@
   <title>sTeX Viewer</title>
   <meta name="viewport" content="width=device-width, initial-scale=1" />
   <link rel="icon" type="image/x-icon" href="/stex/mmt-viewer/favicon.ico" />
-<link rel="stylesheet" href="/stex/mmt-viewer/styles.e4e14622fc5599b3.css"><link rel="stylesheet" href="/stex/mmt-viewer/main.420346012a7e8d87.css">
+<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">
 </head>
 
+<div style="display: none;">
+    <div id="embedding">
+        <!--Embedded Code-->
+    </div>
+</div>
+
 <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.1ed01a91b22a2975.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>

src/mmt-api/resources/versioning/system.txt

@@ -1 +1 @@
-25.0.0
+26.0.0

src/mmt-api/src/main/info/kwarc/mmt/api/archives/Index.scala

@@ -173,7 +173,7 @@ abstract class Importer extends TraversingBuildTarget with GeneralImporter {imp
   def importDocument(bt: BuildTask, index: Document => Unit,rel:ULOStatement => Unit): BuildResult
 
   def buildFile(bf: BuildTask): BuildResult = {
-    val sourcefile = bf.archive.root.relativize(bf.inFile).toString.split('/').foldLeft(bf.archive.narrationBase)((p, s) => p / s)
+    val sourcefile = bf.archive.root.relativize(bf.inFile).toFilePath.foldLeft(bf.archive.narrationBase)((p, s) => p / s)
     val graph = controller.depstore.newGraph(sourcefile)
     import info.kwarc.mmt.api.ontology.RDFImplicits._
     graph.add(ULO.file(sourcefile))

src/mmt-api/src/main/info/kwarc/mmt/api/ontology/ULO.scala

@@ -11,7 +11,7 @@ import org.eclipse.rdf4j.model.vocabulary.{DC, OWL, RDF, RDFS, XSD}
 import org.eclipse.rdf4j.query.TupleQueryResult
 import org.eclipse.rdf4j.repository.RepositoryResult
 import org.eclipse.rdf4j.repository.sail.SailRepositoryConnection
-import org.eclipse.rdf4j.rio.Rio
+import org.eclipse.rdf4j.rio.{RDFParseException, Rio}
 import org.eclipse.rdf4j.sparqlbuilder.core.SparqlBuilder
 import org.eclipse.rdf4j.sparqlbuilder.core.query.Queries
 import org.eclipse.rdf4j.sparqlbuilder.graphpattern.GraphPatterns
@@ -53,8 +53,19 @@ object RDFImplicits {
     .replace("%5E","^"))//URLDecoder.decode(i.getLocalName,"UTF-8"))
   implicit def asResource(e: ULOTrait): Resource = e.toIri
   def isPath(i:Value) = i.isIRI && i.asInstanceOf[IRI].getLocalName.isEmpty//.getNamespace == path_namespace
-
-  implicit def URIToIRI(uri:URI): IRI = iri(uri.toString)
+  implicit def URIToIRI(uri:URI): IRI = iri(uri.toString
+    .replace("[", "%5B")
+    .replace("]", "%5D")
+    .replace(" ", "%20")
+    .replace(">", "%3E")
+    .replace("<", "%3C")
+    .replace("|", "%7C")
+    .replace("\\", "%5C")
+    .replace("{", "%7B")
+    .replace("}", "%7D")
+    .replace("#", "%23")
+    .replace("^", "%5E")
+  )
 }
 import RDFImplicits._
 
@@ -645,7 +656,9 @@ class RDFStore(protected val report : frontend.Report) extends RDFRelStoreLike {
     val conn = repo.getConnection
     if ((a / relational).exists) a.traverse(relational, in, Archive.traverseIf(fileFormat._1)) { case info.kwarc.mmt.api.archives.Current(inFile, _) =>
       val iri = relpath(a, inFile)
-      conn.add(inFile.toJava, fileFormat._2, iri)
+      try{conn.add(inFile.toJava, fileFormat._2, iri)} catch {
+        case _:RDFParseException =>
+      }
     }
     conn.close()
   }
@@ -988,10 +1001,16 @@ object SPARQL {
   private case class PathO(p:Path) extends Subject {
     override def toObjString: String = "<" + pathToIri(p).toString + ">"
   }
-  case class V(s:String) extends Subject {
+  private case class IriO(i:IRI) extends Object {
+    override def toObjString: String = "<" + i.toString + ">"
+  }
+  case class V(s:String) extends Subject with Predicate {
     def toObjString = s"?$s"
+    def predString: String = s"?$s"
   }
   implicit def pathtosubject(p:Path): Subject = PathO(p)
+
+  implicit def classtoobject(p: ULOClass): Object = IriO(p.toIri)
   private case class SelectWhere(vars:List[String],where:SparqlQuery) extends SparqlQuery {
     def queryString: String = s"SELECT ${vars.map("?" + _).mkString(" ")} WHERE { ${where.queryString} }"
   }

src/mmt-lsp/src/info/kwarc/mmt/lsp/Server.scala

@@ -146,7 +146,7 @@ class UnitError(val cp: CPath, h: History) {
 class ClientWrapper[+A <: LSPClient](val client : A,server:LSPServer[A]) {
   private def normalizeUri(s : String) : String = s.take(5) + s.drop(5).replace(":","%3A")
   def log(s : String) = client.logMessage(new MessageParams(MessageType.Info,s))
-  def logError(s : String) = client.logMessage(new MessageParams(MessageType.Error,s))
+  def logError(s : String) = client.showMessage(new MessageParams(MessageType.Error,s))//client.logMessage(new MessageParams(MessageType.Error,s))
   def resetErrors(uri:String) = this.synchronized {
     diags.get(uri).foreach(_.clear)
     val params = new PublishDiagnosticsParams()

src/mmt-lsp/src/info/kwarc/mmt/lsp/TextDocument.scala

@@ -12,7 +12,7 @@ import scala.collection.{immutable, mutable}
 trait TextDocumentServer[ClientType <: LSPClient,DocumentType <: LSPDocument[ClientType,LSPServer[ClientType]]] { self : LSPServer[ClientType] =>
 
   def newDocument(uri : String) : DocumentType
-  protected val documents = mutable.Map.empty[String,DocumentType]
+  val documents = mutable.Map.empty[String,DocumentType]
 
   override def didOpen(params: DidOpenTextDocumentParams): Unit = {
     val document = params.getTextDocument