equal
deleted
inserted
replaced
18 val init_theory: string -> unit |
18 val init_theory: string -> unit |
19 val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit |
19 val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit |
20 type token |
20 type token |
21 val basic_token: OuterLex.token -> token |
21 val basic_token: OuterLex.token -> token |
22 val markup_token: string * string -> token |
22 val markup_token: string * string -> token |
|
23 val markup_env_token: string * string -> token |
23 val verbatim_token: string -> token |
24 val verbatim_token: string -> token |
24 val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit |
25 val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit |
25 val token_source: string -> (unit -> token list) -> unit |
26 val token_source: string -> (unit -> token list) -> unit |
26 val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory |
27 val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory |
27 val result: string -> string -> thm -> unit |
28 val result: string -> string -> thm -> unit |
373 |
374 |
374 |
375 |
375 type token = Latex.token; |
376 type token = Latex.token; |
376 val basic_token = Latex.Basic; |
377 val basic_token = Latex.Basic; |
377 val markup_token = Latex.Markup; |
378 val markup_token = Latex.Markup; |
|
379 val markup_env_token = Latex.MarkupEnv; |
378 val verbatim_token = Latex.Verbatim; |
380 val verbatim_token = Latex.Verbatim; |
379 |
381 |
380 fun old_symbol_source name mk_text = |
382 fun old_symbol_source name mk_text = |
381 with_session () (fn _ => add_tex_source name (Latex.old_symbol_source name (mk_text ()))); |
383 with_session () (fn _ => add_tex_source name (Latex.old_symbol_source name (mk_text ()))); |
382 |
384 |