diff --git a/src/ulo-storage-applications/pom.xml b/src/ulo-storage-applications/pom.xml
index e7cb484d2b3a3a2900d394d07504d2338ac25726..489b550a0e62b842351a020b981b401fc49db202 100644
--- a/src/ulo-storage-applications/pom.xml
+++ b/src/ulo-storage-applications/pom.xml
@@ -44,6 +44,14 @@
<mainClass>info.mathhub.uloapi.html.Main</mainClass>
</configuration>
</plugin>
+ <plugin>
+ <groupId>org.apache.maven.plugins</groupId>
+ <artifactId>maven-compiler-plugin</artifactId>
+ <configuration>
+ <source>11</source>
+ <target>11</target>
+ </configuration>
+ </plugin>
</plugins>
</build>
diff --git a/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/AFP.java b/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/AFP.java
new file mode 100644
index 0000000000000000000000000000000000000000..09e20eeec7e7a3c0d9a61ce0213c3984036b6da6
--- /dev/null
+++ b/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/AFP.java
@@ -0,0 +1,131 @@
+package info.mathhub.uloapi.html;
+
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.net.URI;
+import java.net.URISyntaxException;
+import java.util.Arrays;
+import java.util.List;
+import java.util.regex.Pattern;
+import java.util.stream.Collectors;
+
+/**
+ * Provide functionality for dealing with URI to the Isabelle AFP
+ * export.
+ */
+public class AFP {
+ private static final Logger log = LoggerFactory.getLogger(AFP.class);
+
+ private AFP() {}
+
+ /**
+ * Given an sourceref address from the Isabelle AFP export, try to return an URL to the original
+ * source document.
+ *
+ * This implementation is very specific, it will only work for the specific AFP export were
+ * are dealing with. As of writing this, it is reachable at http://gl.mathhub.info/Isabelle/AFP,
+ * for our experiments we used commit 346f2887.
+ *
+ * @return The URL to the original document, viewable in a web browser. Returns {@code null} if
+ * no URL could be inferred.
+ */
+ public static String sourceUrlFor(String exportIri) {
+ // parse IRI as URI so we can look at the different parts
+
+ URI uri;
+
+ try {
+ uri = new URI(exportIri);
+ } catch (URISyntaxException e) {
+ log.warn("got bad IRI={} error=malformed exception={}", exportIri, e);
+ return null;
+ }
+
+ // we only support this particular host
+
+ if (!uri.getHost().equals("isabelle.in.tum.de")) {
+ log.warn("got bad IRI={} error=bad host", exportIri);
+ return null;
+ }
+
+ // get the path from the full URI
+
+ final String path = uri.getPath();
+
+ if (path == null) {
+ log.warn("got bad IRI={} error=no path", exportIri);
+ return null;
+ }
+
+ log.info("working w/ path={}", path);
+
+ // split into components; we expect there to be at least four
+
+ final List<String> components = splitPath(path, '/');
+ log.info("working w/ components={}", components);
+
+ if (components.size() < 4) {
+ log.warn("got bad IRI={} error=too few components expected=4+ got={}", exportIri, components.size());
+ return null;
+ }
+
+ // evaluate the first two components, which should be fixed
+
+ if (!components.get(0).equals("source")) {
+ log.warn("got bad IRI={} error=bad first component expected=source got={}", exportIri, components.get(0));
+ return null;
+ }
+
+ if (!components.get(1).equals("HOL")) {
+ log.warn("got bad IRI={} error=bad second component expected=HOL got={}", exportIri, components.get(1));
+ return null;
+ }
+
+ // the third component is the library, that is the collection the target
+ // file is in
+
+ final String library = components.get(2);
+
+ // the fourth component is the target package with a lot of cruft
+
+ final String end = ".theory";
+ final String packageWithCruft = components.get(3);
+ final int endIdx = packageWithCruft.indexOf(end);
+
+ if (endIdx == -1) {
+ log.warn("got bad IRI={} error=missing .theory extension", exportIri);
+ return null;
+ }
+
+ final String packageName = packageWithCruft.substring(0, endIdx + end.length());
+
+ // from the package we need to infer the filename
+
+ final List<String> packageComponents = splitPath(packageName, '.');
+
+ log.info("working w/ package={} components={}", packageName, packageComponents);
+
+ if (packageComponents.size() < 2) {
+ throw new IllegalStateException("too few components in IRI=" + exportIri);
+ }
+
+ if (!packageComponents.get(packageComponents.size() - 1).equals("theory")) {
+ throw new IllegalStateException("last component should be .theory, IRI=" + exportIri);
+ }
+
+ final String file = packageComponents.get(packageComponents.size() - 2);
+
+ // finally we can generate the URL
+
+ return String.format(
+ "https://isabelle.in.tum.de/dist/library/HOL/%s/%s.html",
+ library, file
+ );
+ }
+
+ private static List<String> splitPath(String path, char sep) {
+ final String[] components = path.split(Pattern.quote(String.valueOf(sep)));
+ return Arrays.stream(components).map(String::trim).filter(s -> !s.isEmpty()).collect(Collectors.toList());
+ }
+}
diff --git a/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/Routes.java b/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/Routes.java
index 4e6b100dd85e6c09dbd13ba28602f5b75876c605..c0c282f2b3552cf2a2891ac5a0b31bdda13cd8e2 100644
--- a/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/Routes.java
+++ b/src/ulo-storage-applications/src/main/java/info/mathhub/uloapi/html/Routes.java
@@ -83,11 +83,13 @@ public class Routes {
final String uri = Base64.decode(base64uri);
final Meta meta = query.getMeta(uri);
+ final String afpUrl = AFP.sourceUrlFor(meta.sourceref);
final List<PrintableIRI> uses = PrintableIRI.convert(query.getUses(uri));
final Map<String, Object> model = new HashMap<>();
model.put("uri", uri);
model.put("meta", meta);
+ model.put("afp_url", afpUrl);
model.put("uses", uses);
return new ModelAndView(withGlobals(model), "explore_node.flt");
diff --git a/src/ulo-storage-applications/src/main/resources/spark/template/freemarker/explore_node.flt b/src/ulo-storage-applications/src/main/resources/spark/template/freemarker/explore_node.flt
index 2cf4638fb15494e489e7ee2996b6e68c0fd8a9e5..d47e28ec6b5aee75f5f38109d7ba7445f3490548 100644
--- a/src/ulo-storage-applications/src/main/resources/spark/template/freemarker/explore_node.flt
+++ b/src/ulo-storage-applications/src/main/resources/spark/template/freemarker/explore_node.flt
@@ -41,6 +41,11 @@
<li>
<code>${meta.sourceref}</code>
</li>
+ <#if afp_url??>
+ <li>
+ <a href="${afp_url}">Original Isabelle Source</a> (Experimental. Link might lead to the void.)
+ </li>
+ </#if>
</ul>
<h3>Node uses...</h3>