--- 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)
}