equal
deleted
inserted
replaced
4 Theory presentation: HTML and PDF-LaTeX documents. |
4 Theory presentation: HTML and PDF-LaTeX documents. |
5 *) |
5 *) |
6 |
6 |
7 signature PRESENT = |
7 signature PRESENT = |
8 sig |
8 sig |
|
9 val tex_path: string -> Path.T |
9 val get_bibtex_entries: theory -> string list |
10 val get_bibtex_entries: theory -> string list |
10 val theory_qualifier: theory -> string |
11 val theory_qualifier: theory -> string |
11 val document_option: Options.T -> {enabled: bool, disabled: bool} |
12 val document_option: Options.T -> {enabled: bool, disabled: bool} |
12 val document_variants: Options.T -> (string * string) list |
13 val document_variants: Options.T -> (string * string) list |
13 val init: HTML.symbols -> bool -> Path.T -> bool -> string -> (string * string) list -> |
14 val init: HTML.symbols -> bool -> Path.T -> bool -> string -> (string * string) list -> |
29 val html_path = html_ext o Path.basic; |
30 val html_path = html_ext o Path.basic; |
30 val index_path = Path.basic "index.html"; |
31 val index_path = Path.basic "index.html"; |
31 val readme_html_path = Path.basic "README.html"; |
32 val readme_html_path = Path.basic "README.html"; |
32 val doc_indexN = "session"; |
33 val doc_indexN = "session"; |
33 val session_graph_path = Path.basic "session_graph.pdf"; |
34 val session_graph_path = Path.basic "session_graph.pdf"; |
34 fun document_path name = Path.basic name |> Path.ext "pdf"; |
35 val document_path = Path.ext "pdf" o Path.basic; |
35 |
36 |
36 fun show_path path = Path.implode (Path.expand (File.full_path Path.current path)); |
37 fun show_path path = Path.implode (Path.expand (File.full_path Path.current path)); |
37 |
38 |
38 |
39 |
39 |
40 |