# HG changeset patch
# User wenzelm
# Date 1302270494 -7200
# Node ID dafae095d73337adb3a97225988784efd0e758dd
# Parent  2074b31650e65a9b81db84806f985648bd254049
discontinued special status of structure Printer;

diff -r 2074b31650e6 -r dafae095d733 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Apr 08 15:02:11 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Fri Apr 08 15:48:14 2011 +0200
@@ -132,12 +132,12 @@
 This \verb!no_vars! business can become a bit tedious.
 If you would rather never see question marks, simply put
 \begin{quote}
-@{ML "show_question_marks_default := false"}\verb!;!
+@{ML "Printer.show_question_marks_default := false"}\verb!;!
 \end{quote}
 at the beginning of your file \texttt{ROOT.ML}.
 The rest of this document is produced with this flag set to \texttt{false}.
 
-Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
+Hint: Setting @{ML Printer.show_question_marks_default} to \texttt{false} only
 suppresses question marks; variables that end in digits,
 e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
 e.g. @{text"x1.0"}, their internal index. This can be avoided by
diff -r 2074b31650e6 -r dafae095d733 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Apr 08 15:02:11 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Fri Apr 08 15:48:14 2011 +0200
@@ -173,12 +173,12 @@
 This \verb!no_vars! business can become a bit tedious.
 If you would rather never see question marks, simply put
 \begin{quote}
-\verb|show_question_marks_default := false|\verb!;!
+\verb|Printer.show_question_marks_default := false|\verb!;!
 \end{quote}
 at the beginning of your file \texttt{ROOT.ML}.
 The rest of this document is produced with this flag set to \texttt{false}.
 
-Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
+Hint: Setting \verb|Printer.show_question_marks_default| to \texttt{false} only
 suppresses question marks; variables that end in digits,
 e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isaliteral{2E}{\isachardot}}{\isadigit{0}}},
 e.g. \isa{x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}}, their internal index. This can be avoided by
diff -r 2074b31650e6 -r dafae095d733 src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 08 15:02:11 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 08 15:48:14 2011 +0200
@@ -244,7 +244,7 @@
       val (vs, cos) = the_spec thy dtco;
       val ty = Type (dtco, map TFree vs);
       val pretty_typ_bracket =
-        Syntax.pretty_typ (Config.put Syntax.pretty_priority (Syntax.max_pri + 1) ctxt);
+        Syntax.pretty_typ (Config.put pretty_priority (Syntax.max_pri + 1) ctxt);
       fun pretty_constr (co, tys) =
         Pretty.block (Pretty.breaks
           (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
diff -r 2074b31650e6 -r dafae095d733 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Apr 08 15:02:11 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 08 15:48:14 2011 +0200
@@ -382,14 +382,14 @@
     val config = coerce config_value;
   in (config, register_config config_value) end;
 
-val config_bool   = declare_config Config.Bool Config.bool false;
-val config_int    = declare_config Config.Int Config.int false;
-val config_real   = declare_config Config.Real Config.real false;
+val config_bool = declare_config Config.Bool Config.bool false;
+val config_int = declare_config Config.Int Config.int false;
+val config_real = declare_config Config.Real Config.real false;
 val config_string = declare_config Config.String Config.string false;
 
-val config_bool_global   = declare_config Config.Bool Config.bool true;
-val config_int_global    = declare_config Config.Int Config.int true;
-val config_real_global   = declare_config Config.Real Config.real true;
+val config_bool_global = declare_config Config.Bool Config.bool true;
+val config_int_global = declare_config Config.Int Config.int true;
+val config_real_global = declare_config Config.Real Config.real true;
 val config_string_global = declare_config Config.String Config.string true;
 
 end;
@@ -401,11 +401,11 @@
  (register_config Ast.trace_raw #>
   register_config Ast.stat_raw #>
   register_config Syntax.positions_raw #>
-  register_config Syntax.show_brackets_raw #>
-  register_config Syntax.show_sorts_raw #>
-  register_config Syntax.show_types_raw #>
-  register_config Syntax.show_structs_raw #>
-  register_config Syntax.show_question_marks_raw #>
+  register_config Printer.show_brackets_raw #>
+  register_config Printer.show_sorts_raw #>
+  register_config Printer.show_types_raw #>
+  register_config Printer.show_structs_raw #>
+  register_config Printer.show_question_marks_raw #>
   register_config Syntax.ambiguity_level_raw #>
   register_config Syntax_Trans.eta_contract_raw #>
   register_config ML_Context.trace_raw #>
diff -r 2074b31650e6 -r dafae095d733 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Fri Apr 08 15:02:11 2011 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Fri Apr 08 15:48:14 2011 +0200
@@ -115,19 +115,19 @@
 
 
 val display_preferences =
- [bool_pref show_types_default
+ [bool_pref Printer.show_types_default
     "show-types"
     "Include types in display of Isabelle terms",
-  bool_pref show_sorts_default
+  bool_pref Printer.show_sorts_default
     "show-sorts"
     "Include sorts in display of Isabelle terms",
-  bool_pref show_consts_default
+  bool_pref Goal_Display.show_consts_default
     "show-consts"
     "Show types of consts in Isabelle goal display",
   bool_pref long_names
     "long-names"
     "Show fully qualified names in Isabelle terms",
-  bool_pref show_brackets_default
+  bool_pref Printer.show_brackets_default
     "show-brackets"
     "Show full bracketing in Isabelle terms",
   bool_pref Goal_Display.show_main_goal_default
@@ -142,7 +142,7 @@
     "goals-limit"
     "Setting for maximum number of goals printed",
   print_depth_pref,
-  bool_pref show_question_marks_default
+  bool_pref Printer.show_question_marks_default
     "show-question-marks"
     "Show leading question mark of variable name"];
 
diff -r 2074b31650e6 -r dafae095d733 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Apr 08 15:02:11 2011 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Apr 08 15:48:14 2011 +0200
@@ -4,30 +4,30 @@
 Pretty printing of asts, terms, types and print (ast) translation.
 *)
 
-signature PRINTER0 =
+signature BASIC_PRINTER =
 sig
-  val show_brackets_default: bool Unsynchronized.ref
-  val show_brackets_raw: Config.raw
   val show_brackets: bool Config.T
-  val show_types_default: bool Unsynchronized.ref
-  val show_types_raw: Config.raw
   val show_types: bool Config.T
-  val show_sorts_default: bool Unsynchronized.ref
-  val show_sorts_raw: Config.raw
   val show_sorts: bool Config.T
   val show_free_types: bool Config.T
   val show_all_types: bool Config.T
-  val show_structs_raw: Config.raw
   val show_structs: bool Config.T
-  val show_question_marks_default: bool Unsynchronized.ref
-  val show_question_marks_raw: Config.raw
   val show_question_marks: bool Config.T
   val pretty_priority: int Config.T
 end;
 
 signature PRINTER =
 sig
-  include PRINTER0
+  include BASIC_PRINTER
+  val show_brackets_default: bool Unsynchronized.ref
+  val show_brackets_raw: Config.raw
+  val show_types_default: bool Unsynchronized.ref
+  val show_types_raw: Config.raw
+  val show_sorts_default: bool Unsynchronized.ref
+  val show_sorts_raw: Config.raw
+  val show_structs_raw: Config.raw
+  val show_question_marks_default: bool Unsynchronized.ref
+  val show_question_marks_raw: Config.raw
   type prtabs
   val empty_prtabs: prtabs
   val update_prtabs: string -> Syntax_Ext.xprod list -> prtabs -> prtabs
@@ -267,3 +267,7 @@
   pretty true false ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf extern ast;
 
 end;
+
+structure Basic_Printer: BASIC_PRINTER = Printer;
+open Basic_Printer;
+
diff -r 2074b31650e6 -r dafae095d733 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 15:02:11 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 15:48:14 2011 +0200
@@ -5,15 +5,9 @@
 (specified by mixfix declarations).
 *)
 
-signature BASIC_SYNTAX =
-sig
-  include PRINTER0
-end;
-
 signature SYNTAX =
 sig
   include LEXICON0
-  include PRINTER0
   val max_pri: int
   val root: string Config.T
   val positions_raw: Config.raw
@@ -469,7 +463,6 @@
     print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
     prtabs: Printer.prtabs} * stamp;
 
-fun rep_syntax (Syntax (tabs, _)) = tabs;
 fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2;
 
 fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
@@ -729,11 +722,8 @@
 
 (*export parts of internal Syntax structures*)
 val syntax_tokenize = tokenize;
-open Lexicon Printer;
+open Lexicon;
 val tokenize = syntax_tokenize;
 
 end;
 
-structure Basic_Syntax: BASIC_SYNTAX = Syntax;
-open Basic_Syntax;
-
diff -r 2074b31650e6 -r dafae095d733 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 15:02:11 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 15:48:14 2011 +0200
@@ -361,7 +361,7 @@
       val checked = map snd (proper_results results');
       val len = length checked;
 
-      val show_term = Syntax.string_of_term (Config.put Syntax.show_brackets true ctxt);
+      val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
     in
       if len = 0 then
         report_result ctxt pos
diff -r 2074b31650e6 -r dafae095d733 src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Fri Apr 08 15:02:11 2011 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Fri Apr 08 15:48:14 2011 +0200
@@ -236,7 +236,7 @@
   end;
 in
 
-val () = show_question_marks_default := false;
+val () = Printer.show_question_marks_default := false;
 val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
 
 end;