--- a/src/Pure/General/symbol.ML Sat Jan 27 10:27:57 2018 +0100
+++ b/src/Pure/General/symbol.ML Sat Jan 27 16:37:41 2018 +0100
@@ -66,6 +66,12 @@
val trim_blanks: string -> string
val bump_init: string -> string
val bump_string: string -> string
+ val sub: symbol
+ val sup: symbol
+ val bold: symbol
+ val make_sub: string -> string
+ val make_sup: string -> string
+ val make_bold: string -> string
val length: symbol list -> int
val output: string -> Output.output * int
end;
@@ -464,6 +470,20 @@
in implode (rev ss' @ qs) end;
+(* styles *)
+
+val sub = "\092<^sub>";
+val sup = "\092<^sup>";
+val bold = "\092<^bold>";
+
+fun make_style sym =
+ Symbol.explode #> maps (fn s => [sym, s]) #> implode;
+
+val make_sub = make_style sub;
+val make_sup = make_style sup;
+val make_bold = make_style bold;
+
+
(** symbol output **)