src/Pure/General/print_mode.ML
changeset 61957 301833d9013a
parent 39124 9bac2f4cfd6e
child 62542 b27b7c2200b9
--- a/src/Pure/General/print_mode.ML	Mon Dec 28 23:13:33 2015 +0100
+++ b/src/Pure/General/print_mode.ML	Tue Dec 29 14:58:15 2015 +0100
@@ -18,6 +18,7 @@
 sig
   include BASIC_PRINT_MODE
   val input: string
+  val ASCII: string
   val internal: string
   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
@@ -28,6 +29,7 @@
 struct
 
 val input = "input";
+val ASCII = "ASCII";
 val internal = "internal";
 
 val print_mode = Unsynchronized.ref ([]: string list);