--- 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
--- 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)
+ }
+ }
}
--- 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();
--- 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
--- 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)
+ }
}