src/Pure/Thy/present.ML
changeset 72310 a756e464e9e3
parent 72309 564012e31db1
child 72321 09d1d7332185
equal deleted inserted replaced
72309:564012e31db1 72310:a756e464e9e3
     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