Merge pull request #487 from UniFormal/master

Release 18

.dockerignore

@@ -0,0 +1,38 @@
+src/project/project
+src/project/build.properties
+
+# configuration files
+src/mmt-sbt-settings
+
+# mmtrc --created by installed
+deploy/mmtrc
+
+# compiled MMT Jars
+deploy/mmt.jar
+deploy/main/*.jar
+
+# Compiled dependened projects
+deploy/lfcatalog/lfcatalog.jar
+deploy/lib/tiscaf.jar
+
+# Documentation & Deploy
+apidoc
+scripts/travis/deploy_key
+
+# IntelliJ Failes
+**/.idea
+**/.idea_modules
+**/*.iml
+
+
+# Eclipse Files
+**/bin
+**/.cache-main
+**/.cache-tests
+**/.project
+**/.settings
+**/target
+**/.classpath
+
+# scala-bin compilation articfacts
+out/

.gitignore

@@ -29,7 +29,6 @@ scripts/travis/deploy_key
 .idea_modules
 *.iml
 
-
 # Eclipse Files
 bin
 .cache-main

.travis.yml

@@ -11,6 +11,7 @@ env:
   global:
   - ENCRYPTION_LABEL: "25a07036478c"
   - COMMIT_AUTHOR_EMAIL: "[email protected]"
+  - JAVA_OPTS: "-Xmx8192m"
 
 # use java, and install sbt on OS X
 language: java
@@ -31,16 +32,28 @@ notifications:
 git:
   depth: 1
 
+# cache the dependencies for sbt so that we do not need to re-download them all the time
+# adapted from https://www.scala-sbt.org/0.13/docs/Travis-CI-with-sbt.html
+cache:
+  directories:
+    - $HOME/.ivy2/cache
+    - $HOME/.sbt
+
+before_cache:
+  # Cleanup the cached directories to avoid unnecessary cache updates
+  - find $HOME/.ivy2/cache -name "ivydata-*.properties" -print -delete
+  - find $HOME/.sbt        -name "*.lock"               -print -delete
+
 # +===============================================================+
 # |Anything below this line has been generated automatically      |
 # |from src/travis.sbt.                                           |
 # +===============================================================+
 before_install:
   - 'if [[ "$TRAVIS_OS_NAME" = "osx" ]]; then brew update; brew install sbt; fi'
 before_script:
-  - 'if [ "$TRAVIS_BRANCH" == "devel" ]; then export TEST_USE_DEVEL=1; fi; echo $TEST_USE_DEVEL;'
+  - "export TEST_USE_BRANCH=$TRAVIS_BRANCH; echo TEST_USE_BRANCH=;"
 install:
-  - "cd src && (cat /dev/null | sbt ++2.12.3 update) && cd .."
+  - "cd src && (cat /dev/null | sbt ++2.12.8 update) && cd .."
 jobs:
   include:
     # check that 'sbt genTravisYML' has been run
@@ -50,69 +63,63 @@ jobs:
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk8
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 genTravisYML) && cd .."
+        - "cd src && (cat /dev/null | sbt ++2.12.8 genTravisYML) && cd .."
         - '(git diff --quiet --exit-code ".travis.yml")'
       stage: SelfCheck
     # Check that our tests run and the code compiles
     - dist: trusty
       env:
-        - "INFO='Check mmt.jar generation and integration tests'"
+        - "INFO='Check that unit tests run'"
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk8
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 deploy) && cd .."
-        - '[[ -f "deploy/mmt.jar" ]]'
-        - "java -cp deploy/mmt.jar info.kwarc.mmt.test.APITest"
-        - "java -cp deploy/mmt.jar info.kwarc.mmt.test.LFTest"
-        - "java -cp deploy/mmt.jar info.kwarc.mmt.odk.ODKTest"
-        - "java -cp deploy/mmt.jar info.kwarc.mmt.odk.MitMTest"
+        - "cd src && (cat /dev/null | sbt ++2.12.8 test) && cd .."
       stage: CompileAndCheck
     - dist: trusty
       env:
-        - "INFO='Check mmt.jar generation and integration tests'"
+        - "INFO='Check that unit tests run'"
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk11
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 deploy) && cd .."
-        - '[[ -f "deploy/mmt.jar" ]]'
-        - "java -cp deploy/mmt.jar info.kwarc.mmt.test.APITest"
-        - "java -cp deploy/mmt.jar info.kwarc.mmt.test.LFTest"
-        - "java -cp deploy/mmt.jar info.kwarc.mmt.odk.ODKTest"
-        - "java -cp deploy/mmt.jar info.kwarc.mmt.odk.MitMTest"
+        - "cd src && (cat /dev/null | sbt ++2.12.8 test) && cd .."
     - dist: trusty
       env:
-        - "INFO='Check that unit tests run'"
+        - "INFO='Check mmt.jar generation and integration tests'"
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk8
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 test) && cd .."
+        - "cd src && (cat /dev/null | sbt ++2.12.8 deploy) && cd .."
+        - '[[ -f "deploy/mmt.jar" ]]'
+        - "java -cp deploy/mmt.jar info.kwarc.mmt.test.TestRunner"
     - dist: trusty
       env:
-        - "INFO='Check that unit tests run'"
+        - "INFO='Check mmt.jar generation and integration tests'"
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk11
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 test) && cd .."
+        - "cd src && (cat /dev/null | sbt ++2.12.8 deploy) && cd .."
+        - '[[ -f "deploy/mmt.jar" ]]'
+        - "java -cp deploy/mmt.jar info.kwarc.mmt.test.TestRunner"
     # check that the 'apidoc' and 'deployLFCatalog' targets work
     - dist: trusty
       env:
         - "INFO='Check lfcatalog.jar generation using `sbt deployLFCatalog`'"
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk8
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 deployLFCatalog) && cd .."
+        - "cd src && (cat /dev/null | sbt ++2.12.8 deployLFCatalog) && cd .."
         - '[[ -f "deploy/lfcatalog/lfcatalog.jar" ]]'
       stage: DeployCheck
     - dist: trusty
@@ -121,29 +128,29 @@ jobs:
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk11
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 deployLFCatalog) && cd .."
+        - "cd src && (cat /dev/null | sbt ++2.12.8 deployLFCatalog) && cd .."
         - '[[ -f "deploy/lfcatalog/lfcatalog.jar" ]]'
     - dist: trusty
       env:
         - "INFO='Check that apidoc generation works'"
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk8
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 apidoc) && cd .."
+        - "cd src && (cat /dev/null | sbt ++2.12.8 apidoc) && cd .."
         - '[[ -d "apidoc" ]]'
     - dist: trusty
       env:
         - "INFO='Check that apidoc generation works'"
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk11
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
-        - "cd src && (cat /dev/null | sbt ++2.12.3 apidoc) && cd .."
+        - "cd src && (cat /dev/null | sbt ++2.12.8 apidoc) && cd .."
         - '[[ -d "apidoc" ]]'
     # deploy the api documentation
     - dist: trusty
@@ -152,7 +159,7 @@ jobs:
         - 'SBT_VERSION_CMD="^validate"'
       jdk: openjdk8
       language: scala
-      scala: "2.12.3"
+      scala: "2.12.8"
       script:
         - "bash scripts/travis/deploy_doc.sh"
       stage: deploy

Dockerfile

@@ -1,12 +1,12 @@
 # Start from the sbt builder image
-FROM kwarc/sbt-builder
+FROM mozilla/sbt:8u212_1.2.8
 
 # Add all of MMT
 ADD src/ /build/MMT/src
 ADD deploy/ /build/MMT/deploy
 
 WORKDIR /build/MMT/src
-RUN sbt deploy
+RUN sbt ++2.12.8 deploy
 
 # Runtime dependencies
 FROM openjdk:jre-alpine

src/build.sbt

@@ -145,9 +145,9 @@ lazy val src = (project in file(".")).
   exclusions(excludedProjects).
   aggregatesAndDepends(
     mmt, api,
-    lf, concepts, tptp, owl, mizar, frameit, mathscheme, pvs, metamath, tps, imps, isabelle, odk, specware, stex, mathhub, planetary, interviews, latex, openmath, oeis, repl, got, coq,
+    lf, concepts, tptp, owl, mizar, frameit, mathscheme, pvs, metamath, tps, imps, isabelle, odk, specware, stex, mathhub, planetary, interviews, latex, openmath, oeis, repl, got, coq, glf, gf,
     tiscaf, lfcatalog,
-    jedit, intellij
+    jedit, intellij, argsemcomp
   ).
   settings(
     unidocProjectFilter in(ScalaUnidoc, unidoc) := excludedProjects.toFilter,
@@ -160,7 +160,7 @@ lazy val src = (project in file(".")).
 // 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.
 lazy val mmt = (project in file("mmt")).
   exclusions(excludedProjects).
-  dependsOn(tptp, stex, pvs, specware, oeis, odk, jedit, latex, openmath, imps, isabelle, repl, concepts, interviews, mathhub, python, intellij, coq).
+  dependsOn(tptp, stex, pvs, specware, oeis, odk, jedit, latex, openmath, imps, isabelle, repl, concepts, interviews, mathhub, python, intellij, coq, glf, lsp, gf).
   settings(mmtProjectsSettings("mmt"): _*).
   settings(
     exportJars := false,
@@ -190,7 +190,7 @@ lazy val mmt = (project in file("mmt")).
 
 def apiJars(u: Utils) = Seq(
   "scala-compiler.jar",
-  "scala-reflect.jar",
+  "scala-library.jar",
   "scala-parser-combinators.jar",
   "scala-xml.jar",
   "xz.jar",
@@ -254,6 +254,17 @@ lazy val coq = (project in file("mmt-coq")).
   dependsOn(api, lf).
   settings(mmtProjectsSettings("mmt-coq"): _*)
 
+lazy val lsp = (project in file("mmt-lsp")).
+  dependsOn(api,lf).
+  settings(mmtProjectsSettings("mmt-lsp"): _*).
+  settings(unmanagedJars in Compile += baseDirectory.value / "lib" / "lsp4j.jar").
+  settings(unmanagedJars in Compile += baseDirectory.value / "lib" / "jsonrpc.jar").
+  settings(unmanagedJars in Compile += baseDirectory.value / "lib" / "gson.jar").
+  settings(unmanagedJars in Compile += baseDirectory.value / "lib" / "compat.jar").
+  // settings(unmanagedJars in Compile += baseDirectory.value / "lib" / "websocket-api.jar").
+  settings(unmanagedJars in Compile += baseDirectory.value / "lib" / "xtext.jar").
+  settings(unmanagedJars in Compile += baseDirectory.value / "lib" / "guava.jar")
+
 // using MMT as a part of LaTeX. Maintainer: Florian
 lazy val latex = (project in file("latex-mmt")).
   dependsOn(stex).
@@ -280,6 +291,16 @@ lazy val webEdit = (project in file("mmt-webEdit")).
   settings(mmtProjectsSettings("mmt-webEdit"): _*)
 */
 
+// Glf server. Maintainer: Frederik
+lazy val glf = (project in file("mmt-glf")).
+  dependsOn(api, lf, repl).
+  settings(mmtProjectsSettings("mmt-glf"): _*)
+
+// plugin for reading GF. Maintainer: Frederik
+lazy val gf = (project in file("mmt-gf")).
+  dependsOn(api, lf).
+  settings(mmtProjectsSettings("mmt-gf"): _*)
+
 // MMT in the interview server. Maintainer: Teresa
 lazy val interviews = (project in file("mmt-interviews")).
   dependsOn(api, lf).
@@ -413,8 +434,17 @@ lazy val oeis = (project in file("mmt-oeis")).
     unmanagedJars in Compile += utils.value.lib.toJava / "scala-parser-combinators.jar"
   )
 
+// plugin for computing argumentation semantics
+lazy val argsemcomp = (project in file("mmt-argsemcomp")).
+  dependsOn(api).
+  settings(mmtProjectsSettings("mmt-argsemcomp"): _*).
+  settings(
+    libraryDependencies ++= Seq("com.spotify" % "docker-client" % "latest.integration",
+    "org.slf4j" % "slf4j-simple" % "1.7.26", "net.sf.jargsemsat" % "jArgSemSAT" % "0.1.5")
+  )
+
 // =================================
-// DEPENDENT PROJECTS (projects that do not use mmt-api)
+// DEPENDENT PROJECTS (projects that are used by mmt-api)
 // =================================
 
 // this is a dependency of MMT that is copied into the MMT repository for convenience; it only has to be rebuilt when updated (which rarely happens)

src/intellij-mmt/src/info/kwarc/mmt/intellij/MMTPlugin.scala

@@ -34,14 +34,19 @@ class MMTPluginInterface(homestr: String, reportF: Any) {
 	}
 
 	private object Abbreviations {
-		lazy val pairstrings = MMTSystem.getResourceAsString("latex/unicode-latex-map").split("\n")
-		lazy val pairs: List[(String, String)] = pairstrings.collect { case s if s.nonEmpty =>
+		lazy val pairstrings = (MMTSystem.getResourceAsString("unicode/unicode-latex-map") + "\n" +
+			MMTSystem.getResourceAsString("unicode/unicode-ascii-map")).split("\n")
+		lazy val pairs: List[(String, String)] = pairstrings.collect { case s if s.nonEmpty && !s.trim.startsWith("//") =>
+			val ps = s.splitAt(s.lastIndexOf('|'))
+			(ps._1.trim,ps._2.trim.drop(1))
+			/*
 			val ls = s.split('|')
 			if (ls.length != 2) {
 				println(ls.mkString(", "))
 				???
 			}
 			( /*"""\""" + */ ls.head.trim /*.drop(1)*/ , ls.last.trim)
+			 */
 		}.filterNot(p => List("❚", "❙", "❘").contains(p._2)).toList
 	}
 

src/jEdit-mmt/src/info/kwarc/mmt/jedit/Asset.scala

@@ -15,7 +15,7 @@ case class MyPosition(offset : Int) extends javax.swing.text.Position {
 }
 
 /** node in the sidekick outline tree: common ancestor class
- * @param name the label of the asset
+ * @param label the label of the asset
  * @param region the source region of the asset
  */
 sealed abstract class JAsset(protected val label: String, val region: SourceRegion) extends enhanced.SourceAsset(label, region.start.line, MyPosition(region.start.offset))
@@ -44,9 +44,9 @@ class JElemAsset(val elem : StructuralElement, name: String, reg: SourceRegion)
 }
 
 /** node for objects
- * @param term the node in the MMT syntax tree
+ * @param obj the node in the MMT syntax tree
  * @param parent the component containing the term
- * @param subobjectPosition the position in that term
+ * @param reg the region of the term
  */
 class JObjAsset(mmtplugin: MMTPlugin, val obj: Obj, val pragmatic: Obj, val context: Context, val parent: CPath, name: String, reg: SourceRegion)
   extends JAsset(name, reg) with MMTObjAsset {