support for PDF.js: platform-independent PDF viewer;
authorwenzelm
Sun, 20 Feb 2022 15:30:07 +0100
changeset 75105 03115c9eea00
parent 75104 08bb0d32b2e3
child 75106 c2570d25d512
support for PDF.js: platform-independent PDF viewer;
Admin/components/components.sha1
Admin/components/main
etc/build.props
src/Pure/Admin/build_pdfjs.scala
src/Pure/General/http.scala
src/Pure/System/isabelle_tool.scala
src/Tools/jEdit/src/document_model.scala
--- a/Admin/components/components.sha1	Sun Feb 20 15:22:12 2022 +0100
+++ b/Admin/components/components.sha1	Sun Feb 20 15:30:07 2022 +0100
@@ -291,6 +291,7 @@
 ddb3b438430d9565adbf5e3d913bd52af8337511  opam-2.0.6.tar.gz
 fc66802c169f44511d3be30435eb89a11e635742  opam-2.0.7.tar.gz
 108e947d17e9aa6170872614492d8f647802f483  opam-2.1.0.tar.gz
+f8d0218371457eabe2b4214427d9570de92ed861  pdfjs-2.12.313.tar.gz
 1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb  polyml-5.4.1.tar.gz
 a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56  polyml-5.5.0-1.tar.gz
 7d604a99355efbfc1459d80db3279ffa7ade3e39  polyml-5.5.0-2.tar.gz
--- a/Admin/components/main	Sun Feb 20 15:22:12 2022 +0100
+++ b/Admin/components/main	Sun Feb 20 15:30:07 2022 +0100
@@ -18,6 +18,7 @@
 minisat-2.2.1-1
 nunchaku-0.5
 opam-2.0.7
+pdfjs-2.12.313
 polyml-test-15c840d48c9a
 postgresql-42.2.24
 scala-2.13.5
--- a/etc/build.props	Sun Feb 20 15:22:12 2022 +0100
+++ b/etc/build.props	Sun Feb 20 15:30:07 2022 +0100
@@ -22,6 +22,7 @@
   src/Pure/Admin/build_jedit.scala \
   src/Pure/Admin/build_log.scala \
   src/Pure/Admin/build_minisat.scala \
+  src/Pure/Admin/build_pdfjs.scala \
   src/Pure/Admin/build_polyml.scala \
   src/Pure/Admin/build_release.scala \
   src/Pure/Admin/build_spass.scala \
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_pdfjs.scala	Sun Feb 20 15:30:07 2022 +0100
@@ -0,0 +1,105 @@
+/*  Title:      Pure/Admin/build_pdfjs.scala
+    Author:     Makarius
+
+Build Isabelle component for Mozilla PDF.js.
+
+See also:
+
+  - https://github.com/mozilla/pdf.js
+  - https://github.com/mozilla/pdf.js/releases
+  - https://github.com/mozilla/pdf.js/wiki/Setup-PDF.js-in-a-website
+*/
+
+package isabelle
+
+
+object Build_PDFjs
+{
+  /* build pdfjs component */
+
+  val default_url = "https://github.com/mozilla/pdf.js/releases/download"
+  val default_version = "2.12.313"
+
+  def build_pdfjs(
+    base_url: String = default_url,
+    version: String = default_version,
+    target_dir: Path = Path.current,
+    progress: Progress = new Progress): Unit =
+  {
+    Isabelle_System.require_command("unzip", test = "-h")
+
+
+    /* component name */
+
+    val component = "pdfjs-" + version
+    val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component))
+    progress.echo("Component " + component_dir)
+
+
+    /* download */
+
+    val download_url = base_url + "/v" + version
+    Isabelle_System.with_tmp_file("archive", ext = "zip")(archive_file =>
+    {
+      Isabelle_System.download_file(download_url + "/pdfjs-" + version + "-dist.zip",
+        archive_file, progress = progress)
+      Isabelle_System.bash("unzip -x " + File.bash_path(archive_file),
+        cwd = component_dir.file).check
+    })
+
+
+    /* settings */
+
+    val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+    File.write(etc_dir + Path.basic("settings"),
+      """# -*- shell-script -*- :mode=shellscript:
+
+ISABELLE_PDFJS_HOME="$COMPONENT"
+""")
+
+
+    /* README */
+
+    File.write(component_dir + Path.basic("README"),
+      """This is PDF.js from
+""" + download_url + """
+
+
+        Makarius
+        """ + Date.Format.date(Date.now()) + "\n")
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("build_pdfjs", "build component for Mozilla PDF.js",
+      Scala_Project.here, args =>
+    {
+      var target_dir = Path.current
+      var base_url = default_url
+      var version = default_version
+
+      val getopts = Getopts("""
+Usage: isabelle build_pdfjs [OPTIONS]
+
+  Options are:
+    -D DIR       target directory (default ".")
+    -U URL       download URL (default: """" + default_url + """")
+    -V VERSION   version (default: """" + default_version + """")
+
+  Build component for PDF.js.
+""",
+        "D:" -> (arg => target_dir = Path.explode(arg)),
+        "U:" -> (arg => base_url = arg),
+        "V:" -> (arg => version = arg))
+
+      val more_args = getopts(args)
+      if (more_args.nonEmpty) getopts.usage()
+
+      val progress = new Console_Progress()
+
+      build_pdfjs(base_url = base_url, version = version, target_dir = target_dir,
+        progress = progress)
+    })
+}
--- 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
--- a/src/Pure/System/isabelle_tool.scala	Sun Feb 20 15:22:12 2022 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Sun Feb 20 15:30:07 2022 +0100
@@ -223,6 +223,7 @@
   Build_JDK.isabelle_tool,
   Build_JEdit.isabelle_tool,
   Build_Minisat.isabelle_tool,
+  Build_PDFjs.isabelle_tool,
   Build_PolyML.isabelle_tool1,
   Build_PolyML.isabelle_tool2,
   Build_SPASS.isabelle_tool,
--- a/src/Tools/jEdit/src/document_model.scala	Sun Feb 20 15:22:12 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Feb 20 15:30:07 2022 +0100
@@ -313,6 +313,7 @@
   def http_handlers(http_root: String): List[HTTP.Handler] =
   {
     val fonts_root = http_root + "/fonts"
+    val pdfjs_root = http_root + "/pdfjs"
     val preview_root = http_root + "/preview"
 
     val html =
@@ -339,7 +340,7 @@
           HTTP.Response.html(document.content)
         })
 
-    List(HTTP.welcome(http_root), HTTP.fonts(fonts_root), html)
+    List(HTTP.welcome(http_root), HTTP.fonts(fonts_root), HTTP.pdfjs(pdfjs_root), html)
   }
 }