# HG changeset patch
# User wenzelm
# Date 939226368 -7200
# Node ID b2538dccc21ef5faa4083509ca0ee82418408383
# Parent  f9f8660de23ff5ce09a404ebf473581549efe401
Latex.token;

diff -r f9f8660de23f -r b2538dccc21e src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Oct 06 18:12:35 1999 +0200
+++ b/src/Pure/Thy/present.ML	Wed Oct 06 18:12:48 1999 +0200
@@ -17,7 +17,10 @@
   val finish: unit -> unit
   val init_theory: string -> unit
   val verbatim_source: string -> (unit -> string list) -> unit
-  val token_source: string -> (unit -> (OuterLex.token * string option) list) -> unit
+  type token
+  val basic_token: OuterLex.token -> token
+  val markup_token: string * string -> token
+  val token_source: string -> (unit -> token list) -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
   val result: string -> string -> thm -> unit
   val results: string -> string -> thm list -> unit
@@ -325,7 +328,7 @@
     val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
 
     fun finish_node (a, {tex_source, html_source = _, html}) =
-     (apsome (fn p => Buffer.write (Path.append p (tex_path a)) tex_source) doc_prefix;
+     (apsome (fn p => Buffer.write_nonempty (Path.append p (tex_path a)) tex_source) doc_prefix;
       Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
   in
     seq finish_node (Symtab.dest theories);
@@ -347,6 +350,11 @@
 fun verbatim_source name mk_text =
   with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ())));
 
+
+type token = Latex.token;
+val basic_token = Latex.Basic;
+val markup_token = Latex.Markup;
+
 fun token_source name mk_toks =
   with_session () (fn _ => add_tex_source name (Latex.token_source (mk_toks ())));