src/Pure/General/http.scala
changeset 75105 03115c9eea00
parent 75104 08bb0d32b2e3
child 75106 c2570d25d512
--- a/src/Pure/General/http.scala	Sun Feb 20 15:22:12 2022 +0100
+++ b/src/Pure/General/http.scala	Sun Feb 20 15:30:07 2022 +0100
@@ -169,6 +169,10 @@
     val empty: Response = apply()
     def text(s: String): Response = apply(Bytes(s), mime_type_text)
     def html(s: String): Response = apply(Bytes(s), mime_type_html)
+
+    def content(content: Content): Response = apply(content.bytes, content.mime_type)
+    def read(file: JFile): Response = content(read_content(file))
+    def read(path: Path): Response = content(read_content(path))
   }
 
   class Response private[HTTP](val bytes: Bytes, val content_type: String)
@@ -272,7 +276,7 @@
   /** Isabelle resources **/
 
   lazy val isabelle_resources: List[Handler] =
-    List(welcome(), fonts())
+    List(welcome(), fonts(), pdfjs())
 
 
   /* welcome */
@@ -302,4 +306,18 @@
             { case entry if uri_name == root + "/" + entry.path.file_name => Response(entry.bytes) })
         }
       })
-}
+
+
+  /* pdfjs */
+
+  def pdfjs(root: String = "/pdfjs"): Handler =
+    Handler.get(root, arg =>
+    {
+      for {
+        name <- Library.try_unprefix(root, arg.uri.getPath).map(_.dropWhile(_ == '/'))
+        if Path.is_valid(name)
+        path = Path.explode("$ISABELLE_PDFJS_HOME") + Path.explode(name)
+        if path.is_file
+      } yield Response.read(path)
+    })
+}
\ No newline at end of file