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