# HG changeset patch
# User wenzelm
# Date 1645473001 -3600
# Node ID 7bf685cbc7899dcc925ee7de39e8a9acbd9cbc6c
# Parent  6fd8e482c9ce77a31ed7e6b33ed6abc4ffc35b0d
HTTP view of Isabelle PDF documentation;

diff -r 6fd8e482c9ce -r 7bf685cbc789 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Mon Feb 21 20:31:30 2022 +0100
+++ b/src/Pure/General/http.scala	Mon Feb 21 20:50:01 2022 +0100
@@ -302,7 +302,7 @@
   /** Isabelle services **/
 
   def isabelle_services: List[Service] =
-    List(new Welcome(), new Fonts(), new PDFjs())
+    List(new Welcome(), new Fonts(), new PDFjs(), new Docs())
 
 
   /* welcome */
@@ -348,4 +348,23 @@
         s = p.implode if s.startsWith("build/") || s.startsWith("web/")
       } yield Response.read(path)
   }
-}
\ No newline at end of file
+
+
+  /* docs */
+
+  class Docs(name: String = "docs") extends PDFjs(name)
+  {
+    private val doc_contents = isabelle.Doc.main_contents()
+
+    def doc_request(request: Request): Option[Response] =
+      for {
+        p <- request.uri_path if p.is_pdf
+        s = p.implode if s.startsWith("pdf/")
+        name = p.base.split_ext._1.implode
+        doc <- doc_contents.docs.find(_.name == name)
+      } yield Response.read(doc.path.pdf)
+
+    override def apply(request: Request): Option[Response] =
+      doc_request(request) orElse super.apply(request)
+  }
+}
diff -r 6fd8e482c9ce -r 7bf685cbc789 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Mon Feb 21 20:31:30 2022 +0100
+++ b/src/Pure/General/path.scala	Mon Feb 21 20:50:01 2022 +0100
@@ -215,6 +215,7 @@
     }
   def is_java: Boolean = ends_with(".java")
   def is_scala: Boolean = ends_with(".scala")
+  def is_pdf: Boolean = ends_with(".pdf")
 
   def ext(e: String): Path =
     if (e == "") this