# HG changeset patch
# User wenzelm
# Date 1543176698 -3600
# Node ID 3c29edccf73907e8ca7963678e5f2dbc9e17013d
# Parent  6bd63c94cf62e7293e50e4f2fdc6c2593de77faf
expose latex mode operations, to facilitate adhoc changes to it;

diff -r 6bd63c94cf62 -r 3c29edccf739 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Nov 25 21:10:55 2018 +0100
+++ b/src/Pure/Thy/latex.ML	Sun Nov 25 21:11:38 2018 +0100
@@ -29,6 +29,9 @@
   val isabelle_body: string -> text list -> text list
   val theory_entry: string -> string
   val latexN: string
+  val latex_output: string -> string * int
+  val latex_markup: string * Properties.T -> Markup.output
+  val latex_indent: string -> int -> string
 end;
 
 structure Latex: LATEX =
@@ -241,7 +244,7 @@
   let val syms = Symbol.explode str
   in (output_symbols syms, length_symbols syms) end;
 
-fun latex_markup (s, _) =
+fun latex_markup (s, _: Properties.T) =
   if s = Markup.commandN orelse s = Markup.keyword1N orelse s = Markup.keyword3N
   then ("\\isacommand{", "}")
   else if s = Markup.keyword2N