--- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Aug 27 12:57:55 2010 +0200
+++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Aug 27 14:07:09 2010 +0200
@@ -5,11 +5,11 @@
val tests = ["Brackin", "Instructions", "SML", "Verilog"];
-Unsynchronized.set timing;
+timing := true;
-warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
+warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
use_thys tests;
-warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
+warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
List.app Thy_Info.remove_thy tests;
use_thys tests;
--- a/Admin/Benchmarks/HOL-record/ROOT.ML Fri Aug 27 12:57:55 2010 +0200
+++ b/Admin/Benchmarks/HOL-record/ROOT.ML Fri Aug 27 14:07:09 2010 +0200
@@ -5,10 +5,10 @@
val tests = ["RecordBenchmark"];
-Unsynchronized.set timing;
+timing := true;
-warning "\nset quick_and_dirty\n"; Unsynchronized.set quick_and_dirty;
+warning "\nset quick_and_dirty\n"; quick_and_dirty := true;
use_thys tests;
-warning "\nreset quick_and_dirty\n"; Unsynchronized.reset quick_and_dirty;
+warning "\nreset quick_and_dirty\n"; quick_and_dirty := false;
use_thys tests;
--- a/Admin/Benchmarks/HOL-record/RecordBenchmark.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/Admin/Benchmarks/HOL-record/RecordBenchmark.thy Fri Aug 27 14:07:09 2010 +0200
@@ -8,7 +8,7 @@
imports Main
begin
-ML {* Unsynchronized.set Record.timing *}
+ML {* Record.timing := true *}
record many_A =
A000::nat
--- a/doc-src/Codegen/Thy/Setup.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy Fri Aug 27 14:07:09 2010 +0200
@@ -27,6 +27,6 @@
setup {* Code_Target.set_default_code_width 74 *}
-ML_command {* Unsynchronized.reset unique_names *}
+ML_command {* unique_names := false *}
end
--- a/doc-src/IsarOverview/Isar/ROOT.ML Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/IsarOverview/Isar/ROOT.ML Fri Aug 27 14:07:09 2010 +0200
@@ -1,3 +1,3 @@
-Unsynchronized.set quick_and_dirty;
+quick_and_dirty := true;
use_thys ["Logic", "Induction"];
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri Aug 27 14:07:09 2010 +0200
@@ -132,7 +132,7 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{quote}
-@{ML "Unsynchronized.reset show_question_marks"}\verb!;!
+@{ML "show_question_marks := 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}.
@@ -144,7 +144,7 @@
turning the last digit into a subscript: write \verb!x\<^isub>1! and
obtain the much nicer @{text"x\<^isub>1"}. *}
-(*<*)ML "Unsynchronized.reset show_question_marks"(*>*)
+(*<*)ML "show_question_marks := false"(*>*)
subsection {*Qualified names*}
@@ -155,7 +155,7 @@
short names (no qualifiers) by setting \verb!short_names!, typically
in \texttt{ROOT.ML}:
\begin{quote}
-@{ML "Unsynchronized.set short_names"}\verb!;!
+@{ML "short_names := true"}\verb!;!
\end{quote}
*}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri Aug 27 14:07:09 2010 +0200
@@ -173,7 +173,7 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{quote}
-\verb|Unsynchronized.reset show_question_marks|\verb!;!
+\verb|show_question_marks := 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}.
@@ -211,7 +211,7 @@
short names (no qualifiers) by setting \verb!short_names!, typically
in \texttt{ROOT.ML}:
\begin{quote}
-\verb|Unsynchronized.set short_names|\verb!;!
+\verb|short_names := true|\verb!;!
\end{quote}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/Misc/Itrev.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy Fri Aug 27 14:07:09 2010 +0200
@@ -2,7 +2,7 @@
theory Itrev
imports Main
begin
-ML"Unsynchronized.reset unique_names"
+ML"unique_names := false"
(*>*)
section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
\index{induction heuristics|)}
*}
(*<*)
-ML"Unsynchronized.set unique_names"
+ML"unique_names := true"
end
(*>*)
--- a/doc-src/TutorialI/Rules/Basic.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy Fri Aug 27 14:07:09 2010 +0200
@@ -187,7 +187,7 @@
text{*unification failure trace *}
-ML "Unsynchronized.set trace_unify_fail"
+ML "trace_unify_fail := true"
lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"
txt{*
@@ -212,7 +212,7 @@
*}
oops
-ML "Unsynchronized.reset trace_unify_fail"
+ML "trace_unify_fail := false"
text{*Quantifiers*}
--- a/doc-src/TutorialI/Sets/Examples.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy Fri Aug 27 14:07:09 2010 +0200
@@ -1,7 +1,6 @@
-(* ID: $Id$ *)
theory Examples imports Main Binomial begin
-ML "Unsynchronized.reset eta_contract"
+ML "eta_contract := false"
ML "Pretty.margin_default := 64"
text{*membership, intersection *}
--- a/src/CCL/ROOT.ML Fri Aug 27 12:57:55 2010 +0200
+++ b/src/CCL/ROOT.ML Fri Aug 27 14:07:09 2010 +0200
@@ -8,6 +8,6 @@
evaluation to weak head-normal form.
*)
-Unsynchronized.set eta_contract;
+eta_contract := true;
use_thys ["Wfd", "Fix"];
--- a/src/HOL/Prolog/prolog.ML Fri Aug 27 12:57:55 2010 +0200
+++ b/src/HOL/Prolog/prolog.ML Fri Aug 27 14:07:09 2010 +0200
@@ -2,7 +2,7 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-Unsynchronized.set Proof.show_main_goal;
+Proof.show_main_goal := true;
structure Prolog =
struct
--- a/src/HOL/ex/SAT_Examples.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/src/HOL/ex/SAT_Examples.thy Fri Aug 27 14:07:09 2010 +0200
@@ -10,8 +10,8 @@
(* ML {* sat.solver := "zchaff_with_proofs"; *} *)
(* ML {* sat.solver := "minisat_with_proofs"; *} *)
-ML {* Unsynchronized.set sat.trace_sat; *}
-ML {* Unsynchronized.set quick_and_dirty; *}
+ML {* sat.trace_sat := true; *}
+ML {* quick_and_dirty := true; *}
lemma "True"
by sat
@@ -77,8 +77,8 @@
lemma "(ALL x. P x) | ~ All P"
by sat
-ML {* Unsynchronized.reset sat.trace_sat; *}
-ML {* Unsynchronized.reset quick_and_dirty; *}
+ML {* sat.trace_sat := false; *}
+ML {* quick_and_dirty := false; *}
method_setup rawsat =
{* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}
@@ -525,8 +525,8 @@
(* ML {*
sat.solver := "zchaff_with_proofs";
-Unsynchronized.reset sat.trace_sat;
-Unsynchronized.reset quick_and_dirty;
+sat.trace_sat := false;
+quick_and_dirty := false;
*} *)
ML {*
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Aug 27 12:57:55 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Aug 27 14:07:09 2010 +0200
@@ -232,7 +232,8 @@
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
| init true =
- (! initialized orelse
+ (if ! initialized then ()
+ else
(Output.no_warnings_CRITICAL init_outer_syntax ();
Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
Output.add_mode proof_generalN Output.default_output Output.default_escape;
@@ -241,8 +242,8 @@
ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
setup_thy_loader ();
setup_present_hook ();
- Unsynchronized.set initialized);
- sync_thy_loader ();
+ initialized := true);
+ sync_thy_loader ();
Unsynchronized.change print_mode (update (op =) proof_generalN);
Secure.PG_setup ();
Isar.toplevel_loop TextIO.stdIn
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Aug 27 12:57:55 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Aug 27 14:07:09 2010 +0200
@@ -1021,7 +1021,8 @@
fun init_pgip false = panic "No Proof General interface support for Isabelle/classic mode."
| init_pgip true =
- (! initialized orelse
+ (if ! initialized then ()
+ else
(setup_preferences_tweak ();
Output.add_mode proof_generalN Output.default_output Output.default_escape;
Markup.add_mode proof_generalN YXML.output_markup;
@@ -1031,8 +1032,8 @@
setup_present_hook ();
init_pgip_session_id ();
welcome ();
- Unsynchronized.set initialized);
- sync_thy_loader ();
+ initialized := true);
+ sync_thy_loader ();
Unsynchronized.change print_mode (update (op =) proof_generalN);
pgip_toplevel tty_src);
--- a/src/ZF/ZF.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/src/ZF/ZF.thy Fri Aug 27 14:07:09 2010 +0200
@@ -10,7 +10,7 @@
uses "~~/src/Tools/misc_legacy.ML"
begin
-ML {* Unsynchronized.reset eta_contract *}
+ML {* eta_contract := false *}
typedecl i
arities i :: "term"