# HG changeset patch
# User wenzelm
# Date 1601128961 -7200
# Node ID a756e464e9e3eed44bca74d4fb76d4c5c1e5f22d
# Parent  564012e31db17aa7d7a56fac38706787b21b6b69
tuned signature;

diff -r 564012e31db1 -r a756e464e9e3 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Sep 26 14:29:46 2020 +0200
+++ b/src/Pure/Thy/present.ML	Sat Sep 26 16:02:41 2020 +0200
@@ -6,6 +6,7 @@
 
 signature PRESENT =
 sig
+  val tex_path: string -> Path.T
   val get_bibtex_entries: theory -> string list
   val theory_qualifier: theory -> string
   val document_option: Options.T -> {enabled: bool, disabled: bool}
@@ -31,7 +32,7 @@
 val readme_html_path = Path.basic "README.html";
 val doc_indexN = "session";
 val session_graph_path = Path.basic "session_graph.pdf";
-fun document_path name = Path.basic name |> Path.ext "pdf";
+val document_path = Path.ext "pdf" o Path.basic;
 
 fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));