# HG changeset patch
# User wenzelm
# Date 1667997212 -3600
# Node ID deded566d423915a2c63faeba669487e5aa4af76
# Parent  8c9830109ab2dfcb2d9d2fe493d79405aebfc44a
clarified file names;

diff -r 8c9830109ab2 -r deded566d423 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 13:21:18 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 13:33:32 2022 +0100
@@ -18,8 +18,10 @@
 
 
 object Document_Dockable {
-  def document_output(): Path =
-    Path.explode("$ISABELLE_HOME_USER/document/root.pdf")
+  def document_output(name: String = "document"): Path = {
+    val dir = Path.explode("$ISABELLE_HOME_USER/document_output")
+    if (name.isEmpty) dir else dir + Path.explode(name)
+  }
 
   object Status extends Enumeration {
     val WAITING = Value("waiting")
@@ -162,7 +164,7 @@
   }
 
   private def view_document(): Unit = {
-    val path = Document_Dockable.document_output()
+    val path = Document_Dockable.document_output().pdf
     if (path.is_file) Isabelle_System.pdf_viewer(path)
   }