# HG changeset patch
# User wenzelm
# Date 1517067461 -3600
# Node ID 166c1659ac75a49c67859c0c1205d95a6420e692
# Parent  a6f5a78712af536340567e058e059453843efc42
more operations;

diff -r a6f5a78712af -r 166c1659ac75 src/Pure/General/symbol.ML
--- 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 **)