# HG changeset patch
# User wenzelm
# Date 1761414887 -7200
# Node ID 8d90bd0e4f39fc9ea4c694fcabaa83ec19dc7e22
# Parent  65d22b27471af3a548a58e84be3d2c9fb1c9efdb
more accurate Doc_Entry: print_html like Isabelle/jEdit, proper platform_path;

diff -r 65d22b27471a -r 8d90bd0e4f39 src/Tools/VSCode/extension/media/documentation.js
--- a/src/Tools/VSCode/extension/media/documentation.js	Sat Oct 25 19:52:22 2025 +0200
+++ b/src/Tools/VSCode/extension/media/documentation.js	Sat Oct 25 19:54:47 2025 +0200
@@ -41,24 +41,8 @@
           const entryItem = document.createElement("li");
           entryItem.classList.add("doc-entry");
 
-          let cleanedPath = entry.path.replace(/["]/g, "");
-          if (section.title.includes("Examples")) {
-            cleanedPath = cleanedPath.replace(/^.*?src\//, "src/");
-          }
-          if (section.title.includes("Release Notes")) {
-            cleanedPath = cleanedPath.replace(/^\$ISABELLE_HOME\//, "");
-          }
-
-          let displayText = cleanedPath;
-          const match = cleanedPath.match(/([^\/]+?)(?:\.pdf)?$/);
-          if (match) {
-            const filename = match[1];
-            const cleanTitle = entry.title.replace(/["']/g, "").trim();
-            displayText = `<b>${filename}</b>${cleanTitle ? ': ' + cleanTitle : ''}`;
-          }
-
           const entryLink = document.createElement("a");
-          entryLink.innerHTML = displayText;
+          entryLink.innerHTML = entry.print_html;
           entryLink.href = "#";
           entryLink.classList.add("doc-link");
 
@@ -75,7 +59,7 @@
             } else {
               selectedEntry = entryItem;
               entryItem.classList.add("selected");
-              open_document(entry.path);
+              open_document(entry.platform_path);
             }
           });
 
@@ -91,8 +75,8 @@
       container.appendChild(list);
     }
 
-    function open_document(path) {
-      vscode.postMessage({ command: "open_document", path: path });
+    function open_document(platform_path) {
+      vscode.postMessage({ command: "open_document", platform_path: platform_path });
     }
 
     window.onload = function () {
diff -r 65d22b27471a -r 8d90bd0e4f39 src/Tools/VSCode/extension/src/documentation_panel.ts
--- a/src/Tools/VSCode/extension/src/documentation_panel.ts	Sat Oct 25 19:52:22 2025 +0200
+++ b/src/Tools/VSCode/extension/src/documentation_panel.ts	Sat Oct 25 19:54:47 2025 +0200
@@ -68,7 +68,7 @@
 
     this._view.webview.onDidReceiveMessage(async message => {
       if (message.command === 'open_document') {
-        this._open_document(message.path);
+        this._open_document(message.platform_path);
       }
     });
 
@@ -86,28 +86,13 @@
     });
   }
 
-  private _open_document(filePath: string): void {
-    let cleanPath = filePath.replace(/^"+|"+$/g, '').trim();
-
-    const isabelleHome = process.env.ISABELLE_HOME;
-    if (isabelleHome && cleanPath.includes("$ISABELLE_HOME")) {
-      cleanPath = cleanPath.replace("$ISABELLE_HOME", isabelleHome);
-    }
+  private _open_document(platform_path: string): void {
+    const uri = Uri.file(platform_path);
 
-    if (cleanPath.startsWith("/cygdrive/")) {
-      const match = cleanPath.match(/^\/cygdrive\/([a-zA-Z])\/(.*)/);
-      if (match) {
-        const driveLetter = match[1].toUpperCase();
-        const rest = match[2].replace(/\//g, '\\');
-        cleanPath = `${driveLetter}:\\${rest}`;
-      }
+    if (platform_path.endsWith(".pdf")) {
+      commands.executeCommand("vscode.open", uri)
     }
-
-    const uri = Uri.file(cleanPath);
-
-    if (cleanPath.toLowerCase().endsWith(".pdf")) {
-      commands.executeCommand("vscode.open", uri)
-    } else {
+    else {
       workspace.openTextDocument(uri).then(document => {
         window.showTextDocument(document);
       });
diff -r 65d22b27471a -r 8d90bd0e4f39 src/Tools/VSCode/extension/src/lsp.ts
--- a/src/Tools/VSCode/extension/src/lsp.ts	Sat Oct 25 19:52:22 2025 +0200
+++ b/src/Tools/VSCode/extension/src/lsp.ts	Sat Oct 25 19:54:47 2025 +0200
@@ -173,8 +173,8 @@
   new NotificationType<InitRequest>("PIDE/documentation_request")
 
 export interface Doc_Entry {
-  title: string;
-  path: string;
+  print_html: string;
+  platform_path: string;
 }
 
 export interface Doc_Section {
diff -r 65d22b27471a -r 8d90bd0e4f39 src/Tools/VSCode/src/lsp.scala
--- a/src/Tools/VSCode/src/lsp.scala	Sat Oct 25 19:52:22 2025 +0200
+++ b/src/Tools/VSCode/src/lsp.scala	Sat Oct 25 19:54:47 2025 +0200
@@ -787,7 +787,9 @@
 
   object Doc_Entry {
     def apply(entry: Doc.Entry): JSON.T =
-      JSON.Object("title" -> entry.title, "path" -> entry.path.toString)
+      JSON.Object(
+        "print_html" -> entry.print_html,
+        "platform_path" -> File.platform_path(entry.path))
   }
 
   object Doc_Section {