# HG changeset patch
# User wenzelm
# Date 1739453210 -3600
# Node ID 2ecab61b59f3889c44d0a21f28e11c49ddf0f530
# Parent  1af962db8ca61ce3d0b6d23f4522a0681853c71c
expose bundle $ISABELLE_BROWSER_INFO_LIBRARY via HTTP;

diff -r 1af962db8ca6 -r 2ecab61b59f3 NEWS
--- a/NEWS	Thu Feb 13 14:16:11 2025 +0100
+++ b/NEWS	Thu Feb 13 14:26:50 2025 +0100
@@ -158,6 +158,10 @@
 
 *** Isabelle/jEdit Prover IDE ***
 
+* Action isabelle.browser_info or menu "Plugins / Isabelle / Browse HTML
+Library" opens a web browser on the HTML library that is distributed
+with Isabelle (if available, see $ISABELLE_HOME/lib/browser_info.db).
+
 * Action isabelle.select_structure (with keyboard shortcut C+7) extends
 the editor selection by adding the enclosing formal structure, based on
 formal markup by the prover. Repeated invocation of this action extends
diff -r 1af962db8ca6 -r 2ecab61b59f3 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Thu Feb 13 14:16:11 2025 +0100
+++ b/src/Pure/General/http.scala	Thu Feb 13 14:26:50 2025 +0100
@@ -31,6 +31,16 @@
     def file_mime_type(file: JFile): String =
       Option(Files.probeContentType(file.toPath)).getOrElse(default_mime_type)
 
+    def bytes_mime_type(bytes: Bytes, ext: String = ""): String =
+      if (ext.isEmpty) default_mime_type
+      else {
+        Isabelle_System.with_tmp_file("tmp", ext = ext) { tmp_path =>
+          val n = if (bytes.size < 4096) bytes.size.toInt else 4096
+          Bytes.write(tmp_path, bytes.slice(0, n))
+          file_mime_type(tmp_path.file)
+        }
+      }
+
     def apply(
         bytes: Bytes,
         file_name: String = "",
@@ -341,7 +351,8 @@
   /** Isabelle services **/
 
   def isabelle_services: List[Service] =
-    List(Welcome_Service, Fonts_Service, CSS_Service, PDFjs_Service, Docs_Service)
+    List(Welcome_Service, Fonts_Service, CSS_Service, PDFjs_Service, Docs_Service,
+      Browser_Info_Service)
 
 
   /* welcome */
@@ -424,4 +435,35 @@
     override def apply(request: Request): Option[Response] =
       doc_request(request) orElse super.apply(request)
   }
+
+
+  /* browser info */
+
+  object Browser_Info_Service extends Browser_Info()
+
+  class Browser_Info(
+    name: String = "browser_info",
+    database: Path = Path.explode("$ISABELLE_BROWSER_INFO_LIBRARY"),
+    compress_cache: Compress.Cache = Compress.Cache.none
+  ) extends Service(name) {
+
+    override def apply(request: Request): Option[Response] = {
+      val entry_name = request.uri_path.map(_.implode).getOrElse("")
+
+      val proper_response =
+        for (entry <- File_Store.database_entry(database, entry_name))
+        yield {
+          val bytes = entry.content(compress_cache = compress_cache)
+          val mime_type = Content.bytes_mime_type(bytes, ext = Url.get_ext(entry_name))
+          Response.content(HTTP.Content(bytes, mime_type = mime_type))
+        }
+
+      def error_response: Response = {
+        val msg = "Cannot access database " + database.expand + " entry " + quote(entry_name)
+        HTTP.Response.text(Output.error_message_text(msg))
+      }
+
+      Some(proper_response getOrElse error_response)
+    }
+  }
 }
diff -r 1af962db8ca6 -r 2ecab61b59f3 src/Tools/jEdit/jedit_main/actions.xml
--- a/src/Tools/jEdit/jedit_main/actions.xml	Thu Feb 13 14:16:11 2025 +0100
+++ b/src/Tools/jEdit/jedit_main/actions.xml	Thu Feb 13 14:26:50 2025 +0100
@@ -2,6 +2,11 @@
 <!DOCTYPE ACTIONS SYSTEM "actions.dtd">
 
 <ACTIONS>
+	<ACTION NAME="isabelle.browser-info">
+	  <CODE>
+	    isabelle.jedit.Isabelle.open_browser_info(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.set-continuous-checking">
 	  <CODE>
 	    isabelle.jedit.Isabelle.set_continuous_checking();
diff -r 1af962db8ca6 -r 2ecab61b59f3 src/Tools/jEdit/jedit_main/plugin.props
--- a/src/Tools/jEdit/jedit_main/plugin.props	Thu Feb 13 14:16:11 2025 +0100
+++ b/src/Tools/jEdit/jedit_main/plugin.props	Thu Feb 13 14:26:50 2025 +0100
@@ -30,6 +30,7 @@
 #menu actions and dockables
 plugin.isabelle.jedit_main.Plugin.menu.label=Isabelle
 plugin.isabelle.jedit_main.Plugin.menu= \
+  isabelle.browser-info \
   isabelle-export-browser \
   isabelle-session-browser \
   isabelle.preview \
@@ -51,6 +52,7 @@
   isabelle-syslog \
   isabelle-theories \
   isabelle-timing
+isabelle.browser-info.label=Browse HTML library
 isabelle-debugger.label=Debugger panel
 isabelle-debugger.title=Debugger
 isabelle-document.label=Document panel
diff -r 1af962db8ca6 -r 2ecab61b59f3 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Feb 13 14:16:11 2025 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Feb 13 14:26:50 2025 +0100
@@ -593,4 +593,14 @@
 
   def java_monitor(view: View): Unit =
     Java_Monitor.java_monitor_external(view, look_and_feel = GUI.current_laf())
+
+
+  /* HTTP browser_info */
+
+  def open_browser_info(view: View): Unit = {
+    val url =
+      Url.append_path(PIDE.plugin.http_server.url,
+        Url.append_path(HTTP.Browser_Info_Service.name, "index.html"))
+    PIDE.editor.hyperlink_url(url).follow(view)
+  }
 }