discontinued obsolete print mode;
authorwenzelm
Tue Jun 06 13:13:25 2017 +0200 (2017-06-06)
changeset 66020a31760eee09d
parent 66019 69b5ef78fb07
child 66021 08ab52fb9db5
discontinued obsolete print mode;
src/HOL/Tools/ATP/atp_util.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/Pure/General/symbol.ML
src/Pure/System/isabelle_process.ML
src/Pure/Thy/latex.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Mon Jun 05 23:55:58 2017 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Jun 06 13:13:25 2017 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4  
     1.5  val subscript = implode o map (prefix "\<^sub>") o raw_explode  (* FIXME Symbol.explode (?) *)
     1.6  fun nat_subscript n =
     1.7 -  n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
     1.8 +  n |> string_of_int |> not (print_mode_active Print_Mode.ASCII) ? subscript
     1.9  
    1.10  val unquote_tvar = perhaps (try (unprefix "'"))
    1.11  val unquery_var = perhaps (try (unprefix "?"))
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Jun 05 23:55:58 2017 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Jun 06 13:13:25 2017 +0200
     2.3 @@ -69,7 +69,7 @@
     2.4    fun merge data = AList.merge (op =) (K true) data
     2.5  )
     2.6  
     2.7 -fun xsym s s' () = if print_mode_active Symbol.xsymbolsN then s else s'
     2.8 +fun xsym s s' () = if not (print_mode_active Print_Mode.ASCII) then s else s'
     2.9  
    2.10  val irrelevant = "_"
    2.11  val unknown = "?"
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Jun 05 23:55:58 2017 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Tue Jun 06 13:13:25 2017 +0200
     3.3 @@ -236,7 +236,7 @@
     3.4  val subscript = implode o map (prefix "\<^sub>") o Symbol.explode
     3.5  
     3.6  fun nat_subscript n =
     3.7 -  n |> signed_string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
     3.8 +  n |> signed_string_of_int |> not (print_mode_active Print_Mode.ASCII) ? subscript
     3.9  
    3.10  fun flip_polarity Pos = Neg
    3.11    | flip_polarity Neg = Pos
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Jun 05 23:55:58 2017 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Tue Jun 06 13:13:25 2017 +0200
     4.3 @@ -300,7 +300,7 @@
     4.4        (s ^ (term
     4.5              |> singleton (Syntax.uncheck_terms ctxt)
     4.6              |> annotate_types_in_term ctxt
     4.7 -            |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
     4.8 +            |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
     4.9              |> simplify_spaces
    4.10              |> maybe_quote keywords),
    4.11         ctxt |> perhaps (try (Variable.auto_fixes term)))
    4.12 @@ -320,7 +320,7 @@
    4.13  
    4.14      fun of_free (s, T) =
    4.15        maybe_quote keywords s ^ " :: " ^
    4.16 -      maybe_quote keywords (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
    4.17 +      maybe_quote keywords (simplify_spaces (Print_Mode.setmp [] (Syntax.string_of_typ ctxt) T))
    4.18  
    4.19      fun add_frees xs (s, ctxt) =
    4.20        (s ^ space_implode " and " (map of_free xs), ctxt |> fold Variable.auto_fixes (map Free xs))
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jun 05 23:55:58 2017 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 06 13:13:25 2017 +0200
     5.3 @@ -22,7 +22,6 @@
     5.4    val thms_of_name : Proof.context -> string -> thm list
     5.5    val one_day : Time.time
     5.6    val one_year : Time.time
     5.7 -  val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
     5.8    val hackish_string_of_term : Proof.context -> term -> string
     5.9    val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
    5.10  end;
    5.11 @@ -138,12 +137,9 @@
    5.12  val one_day = seconds (24.0 * 60.0 * 60.0)
    5.13  val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
    5.14  
    5.15 -fun with_vanilla_print_mode f x =
    5.16 -  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
    5.17 -
    5.18  fun hackish_string_of_term ctxt =
    5.19    (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
    5.20 -  #> *) with_vanilla_print_mode (Syntax.string_of_term ctxt)
    5.21 +  #> *) Print_Mode.setmp [] (Syntax.string_of_term ctxt)
    5.22    #> YXML.content_of
    5.23    #> simplify_spaces
    5.24  
     6.1 --- a/src/Pure/General/symbol.ML	Mon Jun 05 23:55:58 2017 +0200
     6.2 +++ b/src/Pure/General/symbol.ML	Tue Jun 06 13:13:25 2017 +0200
     6.3 @@ -64,7 +64,6 @@
     6.4    val bump_init: string -> string
     6.5    val bump_string: string -> string
     6.6    val length: symbol list -> int
     6.7 -  val xsymbolsN: string
     6.8    val output: string -> Output.output * int
     6.9  end;
    6.10  
    6.11 @@ -466,11 +465,6 @@
    6.12  
    6.13  fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
    6.14  
    6.15 -
    6.16 -(* print mode *)
    6.17 -
    6.18 -val xsymbolsN = "xsymbols";
    6.19 -
    6.20  fun output s = (s, sym_length (Symbol.explode s));
    6.21  
    6.22  
     7.1 --- a/src/Pure/System/isabelle_process.ML	Mon Jun 05 23:55:58 2017 +0200
     7.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jun 06 13:13:25 2017 +0200
     7.3 @@ -188,7 +188,7 @@
     7.4  (* init protocol *)
     7.5  
     7.6  val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
     7.7 -val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
     7.8 +val default_modes2 = [isabelle_processN, Pretty.symbolicN];
     7.9  
    7.10  val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn socket =>
    7.11    let
     8.1 --- a/src/Pure/Thy/latex.ML	Mon Jun 05 23:55:58 2017 +0200
     8.2 +++ b/src/Pure/Thy/latex.ML	Tue Jun 06 13:13:25 2017 +0200
     8.3 @@ -206,7 +206,7 @@
     8.4  (* print mode *)
     8.5  
     8.6  val latexN = "latex";
     8.7 -val modes = [latexN, Symbol.xsymbolsN];
     8.8 +val modes = [latexN];
     8.9  
    8.10  fun latex_output str =
    8.11    let val syms = Symbol.explode str