--- 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
--- 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
--- 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)) ::
--- 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 #>
--- 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"];
--- 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;
+
--- 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;
-
--- 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
--- 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;