# HG changeset patch
# User wenzelm
# Date 1274976637 -7200
# Node ID f652333bbf8ecb40143bda6329efd92446492b8c
# Parent  01aa36932739aba386f59923b2f44752ab104d60
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;

diff -r 01aa36932739 -r f652333bbf8e NEWS
--- a/NEWS	Thu May 27 17:41:27 2010 +0200
+++ b/NEWS	Thu May 27 18:10:37 2010 +0200
@@ -503,6 +503,7 @@
   OuterSyntax   ~>  Outer_Syntax
   SpecParse     ~>  Parse_Spec
   TypeInfer     ~>  Type_Infer
+  PrintMode     ~>  Print_Mode
 
 Note that "open Legacy" simplifies porting of sources, but forgetting
 to remove it again will complicate porting again in the future.
diff -r 01aa36932739 -r f652333bbf8e src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu May 27 17:41:27 2010 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu May 27 18:10:37 2010 +0200
@@ -148,7 +148,7 @@
 ML {*
   fun check_syntax ctxt thm expected =
     let
-      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
+      val obtained = Print_Mode.setmp [] (Display.string_of_thm ctxt) thm;
     in
       if obtained <> expected
       then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
diff -r 01aa36932739 -r f652333bbf8e src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu May 27 18:10:37 2010 +0200
@@ -200,7 +200,7 @@
                            handle TERM _ => ct)
     in
         quote (
-        PrintMode.setmp [] (
+        Print_Mode.setmp [] (
         setmp_CRITICAL show_brackets false (
         setmp_CRITICAL show_all_types true (
         setmp_CRITICAL Syntax.ambiguity_is_error false (
@@ -239,14 +239,14 @@
               | SMART_STRING =>
                   error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
     in
-      PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
+      Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
     end
     handle ERROR mesg => simple_smart_string_of_cterm ct
 
 val smart_string_of_thm = smart_string_of_cterm o cprop_of
 
-fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
-fun prin t = writeln (PrintMode.setmp []
+fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
+fun prin t = writeln (Print_Mode.setmp []
   (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
 fun pth (HOLThm(ren,thm)) =
     let
diff -r 01aa36932739 -r f652333bbf8e src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu May 27 18:10:37 2010 +0200
@@ -56,7 +56,7 @@
 (*Prints an exception, then fails*)
 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
 
-val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
+val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
 
 fun mk_meta_eq th =
     (case concl_of th of
diff -r 01aa36932739 -r f652333bbf8e src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu May 27 18:10:37 2010 +0200
@@ -32,7 +32,7 @@
 oracle mc_eindhoven_oracle =
 {*
 let
-  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
+  val eindhoven_term = Print_Mode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
 
   fun call_mc s =
     let
diff -r 01aa36932739 -r f652333bbf8e src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 18:10:37 2010 +0200
@@ -487,7 +487,7 @@
         make_string sign (trm::list) =
            Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list
 in
-  PrintMode.setmp ["Mucke"] (make_string sign) terms
+  Print_Mode.setmp ["Mucke"] (make_string sign) terms
 end;
 
 fun callmc s =
diff -r 01aa36932739 -r f652333bbf8e src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Thu May 27 18:10:37 2010 +0200
@@ -439,7 +439,7 @@
 
    fun string_of_typ T =
       setmp_CRITICAL show_sorts true
-       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
+       (Print_Mode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
    val fixestate = (case state_type of
          NONE => []
        | SOME s =>
diff -r 01aa36932739 -r f652333bbf8e src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 27 18:10:37 2010 +0200
@@ -483,7 +483,7 @@
         val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
         val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
         val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
-                      PrintMode.setmp [] multiline_string_for_scope scope
+                      Print_Mode.setmp [] multiline_string_for_scope scope
         val kodkod_sat_solver =
           Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
         val bit_width = if bits = 0 then 16 else bits + 1
diff -r 01aa36932739 -r f652333bbf8e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 18:10:37 2010 +0200
@@ -3306,7 +3306,7 @@
              Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
              @ maps pretty_entry xs
           end
-    val p = PrintMode.with_modes print_modes (fn () =>
+    val p = Print_Mode.with_modes print_modes (fn () =>
       Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
         @ pretty_stat)) ();
diff -r 01aa36932739 -r f652333bbf8e src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 18:10:37 2010 +0200
@@ -911,7 +911,7 @@
 fun string_for_proof ctxt i n =
   let
     fun fix_print_mode f =
-      PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                       (print_mode_value ())) f
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =
diff -r 01aa36932739 -r f652333bbf8e src/HOLCF/IOA/meta_theory/automaton.ML
--- a/src/HOLCF/IOA/meta_theory/automaton.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Thu May 27 18:10:37 2010 +0200
@@ -18,8 +18,8 @@
 structure Automaton: AUTOMATON =
 struct
 
-val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
-val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
+val string_of_typ = Print_Mode.setmp [] o Syntax.string_of_typ_global;
+val string_of_term = Print_Mode.setmp [] o Syntax.string_of_term_global;
 
 exception malformed;
 
diff -r 01aa36932739 -r f652333bbf8e src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/General/print_mode.ML	Thu May 27 18:10:37 2010 +0200
@@ -22,7 +22,7 @@
   val closure: ('a -> 'b) -> 'a -> 'b
 end;
 
-structure PrintMode: PRINT_MODE =
+structure Print_Mode: PRINT_MODE =
 struct
 
 val input = "input";
@@ -49,5 +49,5 @@
 
 end;
 
-structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
-open BasicPrintMode;
+structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
+open Basic_Print_Mode;
diff -r 01aa36932739 -r f652333bbf8e src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Thu May 27 18:10:37 2010 +0200
@@ -355,7 +355,7 @@
     |> snd
     |> Sign.add_const_constraint (c', SOME ty')
     |> Sign.notation true prmode [(Const (c', ty'), mx)]
-    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
+    |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
   end;
 
 
diff -r 01aa36932739 -r f652333bbf8e src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu May 27 18:10:37 2010 +0200
@@ -281,7 +281,7 @@
 
 fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
   (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
-    PrintMode.with_modes modes (Toplevel.print_state true) state));
+    Print_Mode.with_modes modes (Toplevel.print_state true) state));
 
 val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
 val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
@@ -488,7 +488,7 @@
   in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
 
 fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
-  PrintMode.with_modes modes (fn () =>
+  Print_Mode.with_modes modes (fn () =>
     writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
 
 in
diff -r 01aa36932739 -r f652333bbf8e src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Thu May 27 18:10:37 2010 +0200
@@ -200,8 +200,8 @@
   in
     not (is_class andalso (same_shape orelse class_global)) ?
       (Context.mapping_result
-        (Sign.add_abbrev PrintMode.internal arg)
-        (ProofContext.add_abbrev PrintMode.internal arg)
+        (Sign.add_abbrev Print_Mode.internal arg)
+        (ProofContext.add_abbrev Print_Mode.internal arg)
       #-> (fn (lhs' as Const (d, _), _) =>
           same_shape ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
@@ -225,7 +225,7 @@
   in
     lthy |>
      (if is_locale then
-        Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
+        Local_Theory.theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
         #-> (fn (lhs, _) =>
           let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in
             syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
@@ -235,7 +235,7 @@
         Local_Theory.theory
           (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
            Sign.notation true prmode [(lhs, mx3)])))
-    |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
+    |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
     |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
   end;
 
diff -r 01aa36932739 -r f652333bbf8e src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu May 27 18:10:37 2010 +0200
@@ -93,7 +93,7 @@
   let
     val kind = ThySyntax.span_kind span;
     val toks = ThySyntax.span_content span;
-    val text = implode (map (PrintMode.setmp [] ThySyntax.present_token) toks);
+    val text = implode (map (Print_Mode.setmp [] ThySyntax.present_token) toks);
   in
     (case kind of
       ThySyntax.Command name => parse_command name text
diff -r 01aa36932739 -r f652333bbf8e src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/ROOT.ML	Thu May 27 18:10:37 2010 +0200
@@ -310,6 +310,7 @@
 structure OuterSyntax = Outer_Syntax;
 structure SpecParse = Parse_Spec;
 structure TypeInfer = Type_Infer;
+structure PrintMode = Print_Mode;
 
 end;
 
diff -r 01aa36932739 -r f652333bbf8e src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Thu May 27 18:10:37 2010 +0200
@@ -259,7 +259,7 @@
 
 type mode = string * bool;
 val mode_default = ("", true);
-val mode_input = (PrintMode.input, true);
+val mode_input = (Print_Mode.input, true);
 
 
 (* empty_syntax *)
diff -r 01aa36932739 -r f652333bbf8e src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/Thy/html.ML	Thu May 27 18:10:37 2010 +0200
@@ -42,7 +42,7 @@
 (* mode *)
 
 val htmlN = "HTML";
-fun html_mode f x = PrintMode.with_modes [htmlN] f x;
+fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
 
 
 (* common markup *)
diff -r 01aa36932739 -r f652333bbf8e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu May 27 18:10:37 2010 +0200
@@ -153,7 +153,7 @@
       | expand (Antiquote.Antiq (ss, (pos, _))) =
           let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
             options opts (fn () => command src state) ();  (*preview errors!*)
-            PrintMode.with_modes (! modes @ Latex.modes)
+            Print_Mode.with_modes (! modes @ Latex.modes)
               (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
           end
       | expand (Antiquote.Open _) = ""
@@ -429,7 +429,7 @@
   ("display", setmp_CRITICAL display o boolean),
   ("break", setmp_CRITICAL break o boolean),
   ("quotes", setmp_CRITICAL quotes o boolean),
-  ("mode", fn s => fn f => PrintMode.with_modes [s] f),
+  ("mode", fn s => fn f => Print_Mode.with_modes [s] f),
   ("margin", setmp_CRITICAL Pretty.margin_default o integer),
   ("indent", setmp_CRITICAL indent o integer),
   ("source", setmp_CRITICAL source o boolean),
diff -r 01aa36932739 -r f652333bbf8e src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/codegen.ML	Thu May 27 18:10:37 2010 +0200
@@ -109,9 +109,9 @@
 
 val margin = Unsynchronized.ref 80;
 
-fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
+fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
 
-val str = PrintMode.setmp [] Pretty.str;
+val str = Print_Mode.setmp [] Pretty.str;
 
 (**** Mixfix syntax ****)
 
diff -r 01aa36932739 -r f652333bbf8e src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/consts.ML	Thu May 27 18:10:37 2010 +0200
@@ -270,7 +270,7 @@
   let
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
-    val force_expand = mode = PrintMode.internal;
+    val force_expand = mode = Print_Mode.internal;
 
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
       error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
diff -r 01aa36932739 -r f652333bbf8e src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Thu May 27 18:10:37 2010 +0200
@@ -105,19 +105,19 @@
 infixr 5 @|;
 fun x @@ y = [x, y];
 fun xs @| y = xs @ [y];
-val str = PrintMode.setmp [] Pretty.str;
+val str = Print_Mode.setmp [] Pretty.str;
 val concat = Pretty.block o Pretty.breaks;
-fun enclose l r = PrintMode.setmp [] (Pretty.enclose l r);
+fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
 val brackets = enclose "(" ")" o Pretty.breaks;
-fun enum sep l r = PrintMode.setmp [] (Pretty.enum sep l r);
+fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
 fun enum_default default sep l r [] = str default
   | enum_default default sep l r xs = enum sep l r xs;
 fun semicolon ps = Pretty.block [concat ps, str ";"];
 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
-fun indent i = PrintMode.setmp [] (Pretty.indent i);
+fun indent i = Print_Mode.setmp [] (Pretty.indent i);
 
-fun string_of_pretty width p = PrintMode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
-fun writeln_pretty width p = writeln (PrintMode.setmp [] (Pretty.string_of_margin width) p);
+fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
+fun writeln_pretty width p = writeln (Print_Mode.setmp [] (Pretty.string_of_margin width) p);
 
 
 (** names and variable name contexts **)
diff -r 01aa36932739 -r f652333bbf8e src/Tools/WWW_Find/html_unicode.ML
--- a/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 18:10:37 2010 +0200
@@ -19,7 +19,7 @@
 (* mode *)
 
 val htmlunicodeN = "HTMLUnicode";
-fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
+fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
 
 (* symbol output *)
 
diff -r 01aa36932739 -r f652333bbf8e src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Tools/nbe.ML	Thu May 27 18:10:37 2010 +0200
@@ -620,7 +620,7 @@
     val t' = norm thy t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
+    val p = Print_Mode.with_modes modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;
diff -r 01aa36932739 -r f652333bbf8e src/Tools/value.ML
--- a/src/Tools/value.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Tools/value.ML	Thu May 27 18:10:37 2010 +0200
@@ -47,7 +47,7 @@
       | SOME name => value_select name ctxt t;
     val ty' = Term.type_of t';
     val ctxt' = Variable.auto_fixes t' ctxt;
-    val p = PrintMode.with_modes modes (fn () =>
+    val p = Print_Mode.with_modes modes (fn () =>
       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   in Pretty.writeln p end;