# HG changeset patch
# User wenzelm
# Date 1496747605 -7200
# Node ID a31760eee09de2329747999b394d89c9c531a89d
# Parent  69b5ef78fb07b98f49d2fbf522ecfd7b3d487753
discontinued obsolete print mode;

diff -r 69b5ef78fb07 -r a31760eee09d src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Mon Jun 05 23:55:58 2017 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Jun 06 13:13:25 2017 +0200
@@ -126,7 +126,7 @@
 
 val subscript = implode o map (prefix "\<^sub>") o raw_explode  (* FIXME Symbol.explode (?) *)
 fun nat_subscript n =
-  n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
+  n |> string_of_int |> not (print_mode_active Print_Mode.ASCII) ? subscript
 
 val unquote_tvar = perhaps (try (unprefix "'"))
 val unquery_var = perhaps (try (unprefix "?"))
diff -r 69b5ef78fb07 -r a31760eee09d src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Jun 05 23:55:58 2017 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 06 13:13:25 2017 +0200
@@ -69,7 +69,7 @@
   fun merge data = AList.merge (op =) (K true) data
 )
 
-fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s'
+fun xsym s s' () = if not (print_mode_active Print_Mode.ASCII) then s else s'
 
 val irrelevant = "_"
 val unknown = "?"
diff -r 69b5ef78fb07 -r a31760eee09d src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Jun 05 23:55:58 2017 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Jun 06 13:13:25 2017 +0200
@@ -236,7 +236,7 @@
 val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
 
 fun nat_subscript n =
-  n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
+  n |> signed_string_of_int |> not (print_mode_active Print_Mode.ASCII) ? subscript
 
 fun flip_polarity Pos = Neg
   | flip_polarity Neg = Pos
diff -r 69b5ef78fb07 -r a31760eee09d src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Jun 05 23:55:58 2017 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Jun 06 13:13:25 2017 +0200
@@ -300,7 +300,7 @@
       (s ^ (term
             |> singleton (Syntax.uncheck_terms ctxt)
             |> annotate_types_in_term ctxt
-            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
+            |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
             |> simplify_spaces
             |> maybe_quote keywords),
        ctxt |> perhaps (try (Variable.auto_fixes term)))
@@ -320,7 +320,7 @@
 
     fun of_free (s, T) =
       maybe_quote keywords s ^ " :: " ^
-      maybe_quote keywords (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
+      maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
 
     fun add_frees xs (s, ctxt) =
       (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
diff -r 69b5ef78fb07 -r a31760eee09d src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jun 05 23:55:58 2017 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 06 13:13:25 2017 +0200
@@ -22,7 +22,6 @@
   val thms_of_name : Proof.context -> string -> thm list
   val one_day : Time.time
   val one_year : Time.time
-  val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
   val hackish_string_of_term : Proof.context -> term -> string
   val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
 end;
@@ -138,12 +137,9 @@
 val one_day = seconds (24.0 * 60.0 * 60.0)
 val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
 
-fun with_vanilla_print_mode f x =
-  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
-
 fun hackish_string_of_term ctxt =
   (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
-  #> *) with_vanilla_print_mode (Syntax.string_of_term ctxt)
+  #> *) Print_Mode.setmp [] (Syntax.string_of_term ctxt)
   #> YXML.content_of
   #> simplify_spaces
 
diff -r 69b5ef78fb07 -r a31760eee09d src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Mon Jun 05 23:55:58 2017 +0200
+++ b/src/Pure/General/symbol.ML	Tue Jun 06 13:13:25 2017 +0200
@@ -64,7 +64,6 @@
   val bump_init: string -> string
   val bump_string: string -> string
   val length: symbol list -> int
-  val xsymbolsN: string
   val output: string -> Output.output * int
 end;
 
@@ -466,11 +465,6 @@
 
 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
 
-
-(* print mode *)
-
-val xsymbolsN = "xsymbols";
-
 fun output s = (s, sym_length (Symbol.explode s));
 
 
diff -r 69b5ef78fb07 -r a31760eee09d src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Jun 05 23:55:58 2017 +0200
+++ b/src/Pure/System/isabelle_process.ML	Tue Jun 06 13:13:25 2017 +0200
@@ -188,7 +188,7 @@
 (* init protocol *)
 
 val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
-val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
+val default_modes2 = [isabelle_processN, Pretty.symbolicN];
 
 val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn socket =>
   let
diff -r 69b5ef78fb07 -r a31760eee09d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Mon Jun 05 23:55:58 2017 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Jun 06 13:13:25 2017 +0200
@@ -206,7 +206,7 @@
 (* print mode *)
 
 val latexN = "latex";
-val modes = [latexN, Symbol.xsymbolsN];
+val modes = [latexN];
 
 fun latex_output str =
   let val syms = Symbol.explode str