added with_modes, with_default;
authorwenzelm
Mon Jul 23 16:45:02 2007 +0200 (2007-07-23)
changeset 2393479393cb9c0a6
parent 23933 e1a792312472
child 23935 2a4e42ec9a54
added with_modes, with_default;
src/Pure/General/print_mode.ML
src/Pure/Tools/nbe.ML
     1.1 --- a/src/Pure/General/print_mode.ML	Mon Jul 23 16:45:01 2007 +0200
     1.2 +++ b/src/Pure/General/print_mode.ML	Mon Jul 23 16:45:02 2007 +0200
     1.3 @@ -6,18 +6,31 @@
     1.4  mechanisms.
     1.5  *)
     1.6  
     1.7 -signature PRINT_MODE =
     1.8 +signature BASIC_PRINT_MODE =
     1.9  sig
    1.10    val print_mode: string list ref
    1.11    val print_mode_active: string -> bool
    1.12  end;
    1.13  
    1.14 +signature PRINT_MODE =
    1.15 +sig
    1.16 +  include BASIC_PRINT_MODE
    1.17 +  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
    1.18 +  val with_default: ('a -> 'b) -> 'a -> 'b
    1.19 +end;
    1.20 +
    1.21  structure PrintMode: PRINT_MODE =
    1.22  struct
    1.23  
    1.24  val print_mode = ref ([]: string list);
    1.25  fun print_mode_active s = member (op =) (! print_mode) s;
    1.26  
    1.27 +fun with_modes modes f x = CRITICAL (fn () =>
    1.28 +  setmp print_mode (modes @ ! print_mode) f x);
    1.29 +
    1.30 +fun with_default f x = setmp print_mode [] f x;
    1.31 +
    1.32  end;
    1.33  
    1.34 -open PrintMode;
    1.35 +structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
    1.36 +open BasicPrintMode;
     2.1 --- a/src/Pure/Tools/nbe.ML	Mon Jul 23 16:45:01 2007 +0200
     2.2 +++ b/src/Pure/Tools/nbe.ML	Mon Jul 23 16:45:02 2007 +0200
     2.3 @@ -190,7 +190,7 @@
     2.4      val ct = Thm.cterm_of thy t;
     2.5      val (_, t') = (Logic.dest_equals o Thm.prop_of o normalization_conv) ct;
     2.6      val ty = Term.type_of t';
     2.7 -    val p = Library.setmp print_mode (modes @ ! print_mode) (fn () =>
     2.8 +    val p = PrintMode.with_modes modes (fn () =>
     2.9        Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
    2.10          Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)]) ();
    2.11    in Pretty.writeln p end;