Merge pull request #323 from UniFormal/devel

Prepare for Release 10.1

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

@@ -86,7 +86,7 @@ class BooleanOption(val key: String, val label: String) extends MMTOption[Boolea
 object MMTOptions {
   val startup = new StringOption("startup", "custom startup msl file")
   val config = new StringOption("config", "custom configuration file")
-  val archives = new StringOption("archives", "custom folder that contains archives")
+  val archives = new StringOption("archives", "local folder that contains archives (mathhub root)")
   val lowAsciiDelims = new BooleanOption("lowAsciiDelims", "use ASCII 28-31 as delimiters")
   val semantichighlighting = new BooleanOption("SemanticHighlighting","Semantic highlighting (does not work yet)")
   /** the list of all options */

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

@@ -60,7 +60,14 @@ class MMTPlugin extends EBPlugin with Logger {
       errorlist.ErrorSource.registerErrorSource(errorSource)
       val archives = MMTOptions.archives.get orElse
         controller.getMathHub.map(_.local.toString) getOrElse "mars"
-      controller.addArchive(home resolve archives)
+      val archivesFolder = home resolve archives
+      controller.addArchive(archivesFolder)
+      // if no lmh root has been defined (e.g., in the custom mmtrc file), we use the archives folder
+      if (controller.getMathHub.isEmpty && archives != "mars") {
+        val cf = new MMTConfig
+        cf.addEntry(LMHConf(archivesFolder, true, None))
+        controller.loadConfig(cf,false)
+      }
       // status bar is not actually available yet at this point
       controller.report.addHandler(StatusBarLogger)
       controller.extman.addExtension(mmtListener)

src/mmt-api/src/main/info/kwarc/mmt/api/archives/lmh/MathHub.scala

@@ -14,6 +14,7 @@ import scala.util.Try
   * @param https should we use https or ssh for cloning?
   */
 class MathHub(val controller: Controller, var local: File, var remote: URI, var https: Boolean = true) extends LMHHub {
+
   /** implements git */
   protected val git: Git = OS.detect match {case Windows => new WindowsGit() case _ => UnixGit }
   // PATHS
@@ -170,10 +171,10 @@ class MathHub(val controller: Controller, var local: File, var remote: URI, var
       val success = git(local, "clone", rp, id).success
       if (!success) {
         if (lp.exists) {
-          log("git failed, deleting " + lp)
+          logError(s"git clone $rp failed, deleting $lp")
           lp.deleteDir
         } else {
-          log("git failed")
+          logError(s"git clone $rp failed")
         }
         return None
       }
@@ -183,7 +184,7 @@ class MathHub(val controller: Controller, var local: File, var remote: URI, var
         log(s"checking out ${version.get}")
         val vSuccess = git(lp, "checkout", "-f", version.get).success
         if (!vSuccess) {
-          log("checkout failed, Local version may differ from requested version. ")
+          logError("checkout failed, Local version may differ from requested version. ")
         }
       }
     }
@@ -203,7 +204,7 @@ class MathHub(val controller: Controller, var local: File, var remote: URI, var
       Some(new MathHubEntry(lp))
     } catch {
       case _: Exception =>
-        log(s"download failed, aborting")
+        logError(s"download of '$url' failed, aborting")
         None
     } finally {
       zip.delete

src/mmt-api/src/main/info/kwarc/mmt/api/frontend/Controller.scala

@@ -158,22 +158,18 @@ class Controller extends ROController with ActionHandling with Logger {
   /** integrate a configuration into the current state */
   def loadConfig(conf: MMTConfig, loadEverything: Boolean) {
        state.config.add(conf)
-
        // add entries to the namespace
        conf.getEntries(classOf[NamespaceConf]).foreach {case NamespaceConf(id,uri) =>
           state.nsMap = state.nsMap.add(id, uri)
        }
-
        // add archives to the MathPath
        conf.getEntries(classOf[MathPathConf]).foreach {c =>
          addArchive(c.local)
        }
-
        // update the lmh cache
        conf.getEntries(classOf[LMHConf]).foreach { c =>
          lmh = Some(new MathHub(this, c.local, c.remote.getOrElse(MathHub.defaultURL), c.https))
        }
-
        if (loadEverything) {
          loadAllArchives(conf)
          loadAllNeededTargets(conf)

src/mmt-api/src/main/info/kwarc/mmt/api/objects/ModuleOperators.scala

@@ -51,9 +51,9 @@ object Morph {
   }
 
   /** transform a morphism into a list of morphisms by using associativity of composition */
-  def associateComposition(m: Term): List[Term] = m match {
-    case OMCOMP(ms) => ms flatMap associateComposition
-    case _ => List(m)
+  def associateComposition(mors: List[Term]): List[Term] = mors flatMap {
+    case OMCOMP(ms) => associateComposition(ms)
+    case m => List(m)
   }
 
   /** pre: mor is a valid morphism and includes all implicit morphisms
@@ -62,19 +62,20 @@ object Morph {
     * @param preserveType if true, identity morphisms that restrict the type domain are preserved if they cannot be reduced; otherwise, they become OMCOMP()
     */
   def simplify(mor: Term, preserveType: Boolean = false)(implicit lib: Lookup): Term = {
-    val mS = OMCOMP(associateComposition(mor))
-    mS match {
-      case OMMOD(p) => mS
+    mor match {
+      case OMMOD(p) => mor
       case OMS(p) => // TODO dangerous assumption that [mpath] is always a PlainInclude!
         if (p.name.length == 1 && p.name.steps.head.isInstanceOf[ComplexStep])
           OMCOMP()
         else
-          mS
-      case OMIDENT(t) => if (preserveType) mS else OMCOMP()
+          mor
+      case OMIDENT(t) => if (preserveType) mor else OMCOMP()
       case OMINST(t,args) => mor
       case OMStructuralInclude(f,t) => mor
       case OMCOMP(ms) =>
-        var left = ms map {m => simplify(m,true)} //TODO can we skip simplification? Nothing much happens because there are no nested compositions anymore
+        val parts = associateComposition(ms)
+        var partsS = parts map {m => simplify(m,true)} //TODO can we skip simplification? Nothing much happens because there are no nested compositions anymore
+        var left = associateComposition(partsS) // usually redundant, but simplification may occasionally introduce a composition
         var result: List[Term] = Nil
         // we go through all morphisms m in 'ms', building the simplification in 'result' (in reverse order)
         // we put R = OMCOMP(result.reverse) for the morphism processed so far
@@ -181,12 +182,8 @@ object Morph {
           case OMIDENT(_) => false
           case _ => true 
         }
-        // aggregate to a morphism if necessary
-        result match {
-          case Nil => OMCOMP()
-          case h :: Nil => h
-          case msS => OMCOMP(msS)
-        }
+        // OMCOMP disappears if result has length 1
+        OMCOMP(result)
     }
   }