src/Pure/General/symbol.ML

   val source: bool -> (string, 'a) Source.source ->
     (symbol, (string, 'a) Source.source) Source.source
   val explode: string -> symbol list
   val input: string -> string
   val add_mode: string -> (string -> string * real) -> unit
+  val isabelle_fontN: string
+  val symbolsN: string
+  val xsymbolsN: string
   val output: string -> string
   val output_width: string -> string * real
 end;
 
 structure Symbol: SYMBOL =

   in (implode (map char cs), real (sym_length cs)) end;
 
 
 (* maintain modes *)
 
-val modes = ref (Symtab.make [("isabelle_font", isabelle_font_output)]);
+val isabelle_fontN = "isabelle_font";
+val symbolsN = "symbols";
+val xsymbolsN = "xsymbols";
+
+val modes = ref (Symtab.make [(isabelle_fontN, isabelle_font_output)]);
 
 fun lookup_mode name = Symtab.lookup (! modes, name);
 
 fun add_mode name f =
  (if is_none (lookup_mode name) then ()