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);