removed Emacs legacy;
authorwenzelm
Sun Dec 10 14:50:44 2017 +0100 (17 months ago)
changeset 671754e5ba4b23731
parent 67174 258e1394e76a
child 67176 13b5c3ff1954
removed Emacs legacy;
src/Pure/Thy/latex.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Sun Dec 10 14:45:12 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Sun Dec 10 14:50:44 2017 +0100
     1.3 @@ -24,7 +24,6 @@
     1.4    val begin_tag: string -> string
     1.5    val end_tag: string -> string
     1.6    val environment: string -> string -> string
     1.7 -  val tex_trailer: string
     1.8    val isabelle_theory: Position.T -> string -> string -> string
     1.9    val symbol_source: (string -> bool) * (string -> bool) ->
    1.10      string -> Symbol.symbol list -> string
    1.11 @@ -235,17 +234,11 @@
    1.12  fun environment name =
    1.13    enclose ("%\n\\begin{" ^ output_name name ^ "}%\n") ("%\n\\end{" ^ output_name name ^ "}");
    1.14  
    1.15 -val tex_trailer =
    1.16 -  "%%% Local Variables:\n\
    1.17 -  \%%% mode: latex\n\
    1.18 -  \%%% TeX-master: \"root\"\n\
    1.19 -  \%%% End:\n";
    1.20 -
    1.21  fun isabelle_theory pos name txt =
    1.22    output_file pos ^
    1.23    "\\begin{isabellebody}%\n\
    1.24    \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
    1.25 -  "%\n\\end{isabellebody}%\n" ^ tex_trailer;
    1.26 +  "%\n\\end{isabellebody}%\n";
    1.27  
    1.28  fun symbol_source known name syms =
    1.29    isabelle_theory Position.none name
     2.1 --- a/src/Pure/Thy/present.ML	Sun Dec 10 14:45:12 2017 +0100
     2.2 +++ b/src/Pure/Thy/present.ML	Sun Dec 10 14:50:44 2017 +0100
     2.3 @@ -213,7 +213,7 @@
     2.4    File.write_buffer (Path.append path (tex_path name)) src;
     2.5  
     2.6  fun write_tex_index tex_index path =
     2.7 -  write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
     2.8 +  write_tex (index_buffer tex_index) doc_indexN path;
     2.9  
    2.10  fun finish () =
    2.11    with_session_info () (fn {name, chapter, info, info_path, doc_format,