Add lfcatalog target and partially revert #335

After comments from @florian-rabe, this commit restores several
auxiliary files for lfcatalog, after they had been removed in PR #335.

Furthhermore, this commit partially restores a modified version of the
`deployFull` target called `deployLFCatalog`. This can be used to
generate a standalone lfcatalog.jar file. Finally, this commit creates
tests for the new behaviour.

.gitignore

@@ -12,10 +12,14 @@ src/mmt-sbt-settings
 # mmtrc --created by installed
 deploy/mmtrc
 
-# compiled stuff
+# 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

.travis.yml

@@ -123,6 +123,36 @@ jobs:
       script:
         - "cd src && (cat /dev/null | sbt ++2.12.3 deploy) && cd .."
         - '[[ -f "deploy/mmt.jar" ]]'
+    - dist: trusty
+      env:
+        - "INFO='Check lfcatalog.jar generation using `sbt deployLFCatalog`'"
+        - 'SBT_VERSION_CMD="^validate"'
+      jdk: openjdk8
+      language: scala
+      scala: "2.12.3"
+      script:
+        - "cd src && (cat /dev/null | sbt ++2.12.3 deployLFCatalog) && cd .."
+        - '[[ -f "deploy/lfcatalog/lfcatalog.jar" ]]'
+    - dist: trusty
+      env:
+        - "INFO='Check lfcatalog.jar generation using `sbt deployLFCatalog`'"
+        - 'SBT_VERSION_CMD="^validate"'
+      jdk: oraclejdk8
+      language: scala
+      scala: "2.12.3"
+      script:
+        - "cd src && (cat /dev/null | sbt ++2.12.3 deployLFCatalog) && cd .."
+        - '[[ -f "deploy/lfcatalog/lfcatalog.jar" ]]'
+    - dist: trusty
+      env:
+        - "INFO='Check lfcatalog.jar generation using `sbt deployLFCatalog`'"
+        - 'SBT_VERSION_CMD="^validate"'
+      jdk: oraclejdk9
+      language: scala
+      scala: "2.12.3"
+      script:
+        - "cd src && (cat /dev/null | sbt ++2.12.3 deployLFCatalog) && cd .."
+        - '[[ -f "deploy/lfcatalog/lfcatalog.jar" ]]'
     - dist: trusty
       env:
         - "INFO='Check that apidoc generation works'"

deploy/lfcatalog/build.txt

@@ -0,0 +1 @@
+To build the file "lfcatalog.jar", use "sbt deployLFCatalog"

deploy/lfcatalog/readme.txt

@@ -0,0 +1,106 @@
+-------------------------------
+How to run
+-------------------------------
+
+Usage: java -jar lfcatalog.jar (--port <port>)? (location|+inclusion|-exclusion)*
+
+  location === absolute path to a file or directory
+  inclusion === name
+  exclusion === name
+  name === file or directory name pattern, without its path. Star is the only special character and matches any sequence of characters.
+
+  A folder is crawled iff it doesn't match any exclusion pattern.
+  A file is crawled iff it matches at least one inclusion pattern, but no exclusion pattern. However, if no inclusion patterns are provided, only the second condition remains.
+  The default port is 8080 on localhost.
+
+
+-------------------------------
+Command-line user input
+-------------------------------
+
+absolute-disk-path          // add a location
+delete absolute-disk-path   // delete a location
+errors                      // print all files with errors, together with the last error message for each
+exit                        // exit the server
+
+
+-------------------------------
+HTTP get server commands
+-------------------------------
+
+-------               -----                  ------
+Request               Query                  Effect
+-------               -----                  ------
+ <none>                                 print this readme
+ help                                   print this readme
+ admin                                  print the admin page
+ admin      ?      addLocation=         add a disk location to the list of watched locations
+ admin      ?      addInclusion=        add an inclusion pattern (with * replacing any 
+                                        sequence of chars)
+ admin      ?      addExclusion=        add an exclusion pattern (with * replacing any 
+                                        sequence of chars)
+ crawlAll                               crawl all files that have been modified since last check
+ exit                                   shutdown the server
+
+ getMetaText  ?    uri=                 print the semantic comment associated with the entity 
+                                        given by URI/file location
+ getMeta      ?    uri=                 print the XML representation of the semantic comment 
+                                        associated with the entity given by the URI/file location
+ getText      ?    uri=                 retrieve the entity from disk (given by URI/file location)
+ getDependencies ? uri=                 print the dependencies of the entity given by URI
+ getChildren     ? uri=                 print the children of the entity given by URI
+ getPosition  ?    uri=                 print the file and position within file of the entity
+                                        given by URI
+ getPositionInHeader ? uri=             print, in the HTTP header, the file and position within
+                                        file of the entity given by URI
+ getOmdoc     ?    url=                 print the Omdoc skeleton of the document given by its
+                                        disk address
+ getNamespaces   ? url=                 print the namespaces introduced by the document given by 
+                                        its disk address
+ getNamespaces                          print the namespaces introduced by all the documents
+ getModules     ? uri=                  print the modules declared in the given namespace
+
+-------------------------------
+API (see apidocs for more details)
+-------------------------------
+
+// create a Catalog and web server
+catalog = new info.kwarc.mmt.lf.Catalog(locations: HashSet[String] = new HashSet(), 
+                                        inclusions: HashSet[String] = new HashSet("*.elf"), 
+                                        exclusions: HashSet[String] = new HashSet(".svn"), 
+                                        port: Int = 8080, 
+                                        searchPort: Boolean = false,
+                                        log: String => Unit = println,
+                                        crawlingInterval: Int = 5, 
+                                        deletingInterval: Int = 17)
+catalog.init      // throws PortUnavailable if the port is in use
+
+// getters
+catalog.queryURI = "http://localhost:"+port+"/getText"
+catalog.urlToDocument         : HashMap[URI, Document] 
+catalog.uriToNamedBlock       : HashMap[URI, NamedBlock]
+catalog.uriToModulesDeclared  : HashMap[URI, LinkedHashSet[URI]]
+catalog.getPosition(stringUri : String) : String
+catalog.getText(stringUri : String) : String
+catalog.getMeta(stringUri : String, asText : Boolean = false) : String
+catalog.getDependencies(stringUri : String) : Array[String]
+catalog.getChildren(stringUri : String) : Array[String]
+catalog.getNamespaces(stringUrl : String) : Array[String]
+catalog.getNamespaces : Array[String]
+catalog.getModulesInNamespace    : Array[String]
+
+catalog.getOmdoc(stringUrl : String) : String    // only a skeleton
+catalog.writeOmdocToFile(stringUrl : String)     // only a skeleton
+
+// setters
+catalog.addInclusion(pattern : String)
+catalog.addExclusion(pattern : String)
+catalog.addStringLocation(locationName : String)
+catalog.deleteStringLocation(locationName : String)
+
+// crawling on demand
+catalog.crawlAll
+catalog.crawl(location: File)
+catalog.uncrawl(url: String)
+
+catalog.destroy

deploy/lfcatalog/run.bat.example

@@ -0,0 +1 @@
+java -jar lfcatalog.jar +*.elf C:\other\ombase\source

src/build.sbt

@@ -53,6 +53,7 @@ testOptions in Test += Tests.Argument("-oI")
 // =================================
 
 val deploy = TaskKey[Unit]("deploy", "copies packaged jars for MMT projects to deploy location.")
+val deployLFCatalog = TaskKey[Unit]("deployLFCatalog", "builds a stand-alone lfcatalog.jar")
 val install = TaskKey[Unit]("install", "copies jedit jars to local jedit installation folder.")
 
 // =================================
@@ -377,6 +378,10 @@ lazy val lfcatalog = (project in file("lfcatalog")).
   settings(commonSettings("lfcatalog")).
   settings(
     scalaSource in Compile := baseDirectory.value / "src",
+    publishTo := Some(Resolver.file("file", Utils.deploy.toJava / " main")),
+    deployLFCatalog := {
+      assembly in Compile map Utils.deployTo(Utils.deploy / "lfcatalog" / "lfcatalog.jar")
+    }.value, 
     unmanagedJars in Compile += Utils.lib.toJava / "scala-xml.jar"
   )
 

src/travis.sbt

@@ -65,6 +65,7 @@ travisConfig := {
 
     TravisStage("DeployCheck", "check that the 'apidoc' and 'deploy' targets work")(
       TravisJob("Check mmt.jar generation using `sbt deploy`", sbt("deploy", file("deploy/mmt.jar"))),
+      TravisJob("Check lfcatalog.jar generation using `sbt deployLFCatalog`", sbt("deployLFCatalog", file("deploy/lfcatalog/lfcatalog.jar"))),
       TravisJob("Check that apidoc generation works", sbt("apidoc", dir("apidoc")))
     ),