discontinued special status of structure Printer;
authorwenzelm
Fri Apr 08 15:48:14 2011 +0200 (2011-04-08)
changeset 42289dafae095d733
parent 42288 2074b31650e6
child 42290 b1f544c84040
discontinued special status of structure Printer;
doc-src/LaTeXsugar/Sugar/Sugar.thy
doc-src/LaTeXsugar/Sugar/document/Sugar.tex
src/HOL/Tools/Datatype/datatype_data.ML
src/Pure/Isar/attrib.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Apr 08 15:02:11 2011 +0200
     1.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Apr 08 15:48:14 2011 +0200
     1.3 @@ -132,12 +132,12 @@
     1.4  This \verb!no_vars! business can become a bit tedious.
     1.5  If you would rather never see question marks, simply put
     1.6  \begin{quote}
     1.7 -@{ML "show_question_marks_default := false"}\verb!;!
     1.8 +@{ML "Printer.show_question_marks_default := false"}\verb!;!
     1.9  \end{quote}
    1.10  at the beginning of your file \texttt{ROOT.ML}.
    1.11  The rest of this document is produced with this flag set to \texttt{false}.
    1.12  
    1.13 -Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
    1.14 +Hint: Setting @{ML Printer.show_question_marks_default} to \texttt{false} only
    1.15  suppresses question marks; variables that end in digits,
    1.16  e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
    1.17  e.g. @{text"x1.0"}, their internal index. This can be avoided by
     2.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Apr 08 15:02:11 2011 +0200
     2.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Apr 08 15:48:14 2011 +0200
     2.3 @@ -173,12 +173,12 @@
     2.4  This \verb!no_vars! business can become a bit tedious.
     2.5  If you would rather never see question marks, simply put
     2.6  \begin{quote}
     2.7 -\verb|show_question_marks_default := false|\verb!;!
     2.8 +\verb|Printer.show_question_marks_default := false|\verb!;!
     2.9  \end{quote}
    2.10  at the beginning of your file \texttt{ROOT.ML}.
    2.11  The rest of this document is produced with this flag set to \texttt{false}.
    2.12  
    2.13 -Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
    2.14 +Hint: Setting \verb|Printer.show_question_marks_default| to \texttt{false} only
    2.15  suppresses question marks; variables that end in digits,
    2.16  e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isaliteral{2E}{\isachardot}}{\isadigit{0}}},
    2.17  e.g. \isa{x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}}, their internal index. This can be avoided by
     3.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 08 15:02:11 2011 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 08 15:48:14 2011 +0200
     3.3 @@ -244,7 +244,7 @@
     3.4        val (vs, cos) = the_spec thy dtco;
     3.5        val ty = Type (dtco, map TFree vs);
     3.6        val pretty_typ_bracket =
     3.7 -        Syntax.pretty_typ (Config.put Syntax.pretty_priority (Syntax.max_pri + 1) ctxt);
     3.8 +        Syntax.pretty_typ (Config.put pretty_priority (Syntax.max_pri + 1) ctxt);
     3.9        fun pretty_constr (co, tys) =
    3.10          Pretty.block (Pretty.breaks
    3.11            (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
     4.1 --- a/src/Pure/Isar/attrib.ML	Fri Apr 08 15:02:11 2011 +0200
     4.2 +++ b/src/Pure/Isar/attrib.ML	Fri Apr 08 15:48:14 2011 +0200
     4.3 @@ -382,14 +382,14 @@
     4.4      val config = coerce config_value;
     4.5    in (config, register_config config_value) end;
     4.6  
     4.7 -val config_bool   = declare_config Config.Bool Config.bool false;
     4.8 -val config_int    = declare_config Config.Int Config.int false;
     4.9 -val config_real   = declare_config Config.Real Config.real false;
    4.10 +val config_bool = declare_config Config.Bool Config.bool false;
    4.11 +val config_int = declare_config Config.Int Config.int false;
    4.12 +val config_real = declare_config Config.Real Config.real false;
    4.13  val config_string = declare_config Config.String Config.string false;
    4.14  
    4.15 -val config_bool_global   = declare_config Config.Bool Config.bool true;
    4.16 -val config_int_global    = declare_config Config.Int Config.int true;
    4.17 -val config_real_global   = declare_config Config.Real Config.real true;
    4.18 +val config_bool_global = declare_config Config.Bool Config.bool true;
    4.19 +val config_int_global = declare_config Config.Int Config.int true;
    4.20 +val config_real_global = declare_config Config.Real Config.real true;
    4.21  val config_string_global = declare_config Config.String Config.string true;
    4.22  
    4.23  end;
    4.24 @@ -401,11 +401,11 @@
    4.25   (register_config Ast.trace_raw #>
    4.26    register_config Ast.stat_raw #>
    4.27    register_config Syntax.positions_raw #>
    4.28 -  register_config Syntax.show_brackets_raw #>
    4.29 -  register_config Syntax.show_sorts_raw #>
    4.30 -  register_config Syntax.show_types_raw #>
    4.31 -  register_config Syntax.show_structs_raw #>
    4.32 -  register_config Syntax.show_question_marks_raw #>
    4.33 +  register_config Printer.show_brackets_raw #>
    4.34 +  register_config Printer.show_sorts_raw #>
    4.35 +  register_config Printer.show_types_raw #>
    4.36 +  register_config Printer.show_structs_raw #>
    4.37 +  register_config Printer.show_question_marks_raw #>
    4.38    register_config Syntax.ambiguity_level_raw #>
    4.39    register_config Syntax_Trans.eta_contract_raw #>
    4.40    register_config ML_Context.trace_raw #>
     5.1 --- a/src/Pure/ProofGeneral/preferences.ML	Fri Apr 08 15:02:11 2011 +0200
     5.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Fri Apr 08 15:48:14 2011 +0200
     5.3 @@ -115,19 +115,19 @@
     5.4  
     5.5  
     5.6  val display_preferences =
     5.7 - [bool_pref show_types_default
     5.8 + [bool_pref Printer.show_types_default
     5.9      "show-types"
    5.10      "Include types in display of Isabelle terms",
    5.11 -  bool_pref show_sorts_default
    5.12 +  bool_pref Printer.show_sorts_default
    5.13      "show-sorts"
    5.14      "Include sorts in display of Isabelle terms",
    5.15 -  bool_pref show_consts_default
    5.16 +  bool_pref Goal_Display.show_consts_default
    5.17      "show-consts"
    5.18      "Show types of consts in Isabelle goal display",
    5.19    bool_pref long_names
    5.20      "long-names"
    5.21      "Show fully qualified names in Isabelle terms",
    5.22 -  bool_pref show_brackets_default
    5.23 +  bool_pref Printer.show_brackets_default
    5.24      "show-brackets"
    5.25      "Show full bracketing in Isabelle terms",
    5.26    bool_pref Goal_Display.show_main_goal_default
    5.27 @@ -142,7 +142,7 @@
    5.28      "goals-limit"
    5.29      "Setting for maximum number of goals printed",
    5.30    print_depth_pref,
    5.31 -  bool_pref show_question_marks_default
    5.32 +  bool_pref Printer.show_question_marks_default
    5.33      "show-question-marks"
    5.34      "Show leading question mark of variable name"];
    5.35  
     6.1 --- a/src/Pure/Syntax/printer.ML	Fri Apr 08 15:02:11 2011 +0200
     6.2 +++ b/src/Pure/Syntax/printer.ML	Fri Apr 08 15:48:14 2011 +0200
     6.3 @@ -4,30 +4,30 @@
     6.4  Pretty printing of asts, terms, types and print (ast) translation.
     6.5  *)
     6.6  
     6.7 -signature PRINTER0 =
     6.8 +signature BASIC_PRINTER =
     6.9  sig
    6.10 -  val show_brackets_default: bool Unsynchronized.ref
    6.11 -  val show_brackets_raw: Config.raw
    6.12    val show_brackets: bool Config.T
    6.13 -  val show_types_default: bool Unsynchronized.ref
    6.14 -  val show_types_raw: Config.raw
    6.15    val show_types: bool Config.T
    6.16 -  val show_sorts_default: bool Unsynchronized.ref
    6.17 -  val show_sorts_raw: Config.raw
    6.18    val show_sorts: bool Config.T
    6.19    val show_free_types: bool Config.T
    6.20    val show_all_types: bool Config.T
    6.21 -  val show_structs_raw: Config.raw
    6.22    val show_structs: bool Config.T
    6.23 -  val show_question_marks_default: bool Unsynchronized.ref
    6.24 -  val show_question_marks_raw: Config.raw
    6.25    val show_question_marks: bool Config.T
    6.26    val pretty_priority: int Config.T
    6.27  end;
    6.28  
    6.29  signature PRINTER =
    6.30  sig
    6.31 -  include PRINTER0
    6.32 +  include BASIC_PRINTER
    6.33 +  val show_brackets_default: bool Unsynchronized.ref
    6.34 +  val show_brackets_raw: Config.raw
    6.35 +  val show_types_default: bool Unsynchronized.ref
    6.36 +  val show_types_raw: Config.raw
    6.37 +  val show_sorts_default: bool Unsynchronized.ref
    6.38 +  val show_sorts_raw: Config.raw
    6.39 +  val show_structs_raw: Config.raw
    6.40 +  val show_question_marks_default: bool Unsynchronized.ref
    6.41 +  val show_question_marks_raw: Config.raw
    6.42    type prtabs
    6.43    val empty_prtabs: prtabs
    6.44    val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
    6.45 @@ -267,3 +267,7 @@
    6.46    pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast;
    6.47  
    6.48  end;
    6.49 +
    6.50 +structure Basic_Printer: BASIC_PRINTER = Printer;
    6.51 +open Basic_Printer;
    6.52 +
     7.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 15:02:11 2011 +0200
     7.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 15:48:14 2011 +0200
     7.3 @@ -5,15 +5,9 @@
     7.4  (specified by mixfix declarations).
     7.5  *)
     7.6  
     7.7 -signature BASIC_SYNTAX =
     7.8 -sig
     7.9 -  include PRINTER0
    7.10 -end;
    7.11 -
    7.12  signature SYNTAX =
    7.13  sig
    7.14    include LEXICON0
    7.15 -  include PRINTER0
    7.16    val max_pri: int
    7.17    val root: string Config.T
    7.18    val positions_raw: Config.raw
    7.19 @@ -469,7 +463,6 @@
    7.20      print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    7.21      prtabs: Printer.prtabs} * stamp;
    7.22  
    7.23 -fun rep_syntax (Syntax (tabs, _)) = tabs;
    7.24  fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
    7.25  
    7.26  fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
    7.27 @@ -729,11 +722,8 @@
    7.28  
    7.29  (*export parts of internal Syntax structures*)
    7.30  val syntax_tokenize = tokenize;
    7.31 -open Lexicon Printer;
    7.32 +open Lexicon;
    7.33  val tokenize = syntax_tokenize;
    7.34  
    7.35  end;
    7.36  
    7.37 -structure Basic_Syntax: BASIC_SYNTAX = Syntax;
    7.38 -open Basic_Syntax;
    7.39 -
     8.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 15:02:11 2011 +0200
     8.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 15:48:14 2011 +0200
     8.3 @@ -361,7 +361,7 @@
     8.4        val checked = map snd (proper_results results');
     8.5        val len = length checked;
     8.6  
     8.7 -      val show_term = Syntax.string_of_term (Config.put Syntax.show_brackets true ctxt);
     8.8 +      val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
     8.9      in
    8.10        if len = 0 then
    8.11          report_result ctxt pos
     9.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Fri Apr 08 15:02:11 2011 +0200
     9.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Fri Apr 08 15:48:14 2011 +0200
     9.3 @@ -236,7 +236,7 @@
     9.4    end;
     9.5  in
     9.6  
     9.7 -val () = show_question_marks_default := false;
     9.8 +val () = Printer.show_question_marks_default := false;
     9.9  val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
    9.10  
    9.11  end;