clarified file names;
authorwenzelm
Wed, 09 Nov 2022 13:33:32 +0100
changeset 76490 deded566d423
parent 76489 8c9830109ab2
child 76491 2c37c10d6884
clarified file names;
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)
   }