Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
expose latex mode operations, to facilitate adhoc changes to it;
authorwenzelm
Sun, 25 Nov 2018 21:11:38 +0100
changeset 69346 3c29edccf739
parent 69345 6bd63c94cf62
child 69347 54b95d2ec040
child 69420 85b0df070afe
expose latex mode operations, to facilitate adhoc changes to it;
src/Pure/Thy/latex.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle