--- a/Admin/isatest/settings/cygwin-poly-e Thu Sep 02 17:01:49 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e Thu Sep 02 17:02:00 2010 +0200
@@ -24,6 +24,4 @@
ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
-# Disable while Jasmin is on vacation
-unset KODKODI
-#init_component "$HOME/contrib_devel/kodkodi"
+init_component "$HOME/contrib_devel/kodkodi"
--- a/NEWS Thu Sep 02 17:01:49 2010 +0200
+++ b/NEWS Thu Sep 02 17:02:00 2010 +0200
@@ -23,7 +23,7 @@
at the cost of clarity of file dependencies. Recall that Isabelle/ML
files exclusively use the .ML extension. Minor INCOMPATIBILTY.
-* Various options that affect document antiquotations are now properly
+* Various options that affect pretty printing etc. are now properly
handled within the context via configuration options, instead of
unsynchronized references. There are both ML Config.T entities and
Isar declaration attributes to access these.
@@ -36,15 +36,11 @@
Thy_Output.source thy_output_source
Thy_Output.break thy_output_break
+ show_question_marks show_question_marks
+
Note that the corresponding "..._default" references may be only
changed globally at the ROOT session setup, but *not* within a theory.
-* ML structure Unsynchronized never opened, not even in Isar
-interaction mode as before. Old Unsynchronized.set etc. have been
-discontinued -- use plain := instead. This should be *rare* anyway,
-since modern tools always work via official context data, notably
-configuration options.
-
*** Pure ***
@@ -217,6 +213,15 @@
*** ML ***
+* Configuration option show_question_marks only affects regular pretty
+printing of types and terms, not raw Term.string_of_vname.
+
+* ML structure Unsynchronized never opened, not even in Isar
+interaction mode as before. Old Unsynchronized.set etc. have been
+discontinued -- use plain := instead. This should be *rare* anyway,
+since modern tools always work via official context data, notably
+configuration options.
+
* ML antiquotations @{theory} and @{theory_ref} refer to named
theories from the ancestry of the current context, not any accidental
theory loader state as before. Potential INCOMPATIBILITY, subtle
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Sep 02 17:01:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Thu Sep 02 17:02:00 2010 +0200
@@ -108,7 +108,7 @@
@{index_ML Proof.show_main_goal: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML show_hyps: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML show_tags: "bool Unsynchronized.ref"} & default @{ML false} \\
- @{index_ML show_question_marks: "bool Unsynchronized.ref"} & default @{ML true} \\
+ @{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\
\end{mldecls}
These global ML variables control the detail of information that is
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Sep 02 17:01:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Thu Sep 02 17:02:00 2010 +0200
@@ -130,7 +130,7 @@
\indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\
\indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\
- \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Unsynchronized.ref| & default \verb|true| \\
+ \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
\end{mldecls}
These global ML variables control the detail of information that is
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Sep 02 17:01:49 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Sep 02 17:02:00 2010 +0200
@@ -132,19 +132,19 @@
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 := false"}\verb!;!
+@{ML "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! to \texttt{false} only
+Hint: Setting \verb!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
turning the last digit into a subscript: write \verb!x\<^isub>1! and
obtain the much nicer @{text"x\<^isub>1"}. *}
-(*<*)ML "show_question_marks := false"(*>*)
+(*<*)declare [[show_question_marks = false]](*>*)
subsection {*Qualified names*}
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Sep 02 17:01:49 2010 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Thu Sep 02 17:02:00 2010 +0200
@@ -164,7 +164,7 @@
\begin{isamarkuptext}%
If you print anything, especially theorems, containing
schematic variables they are prefixed with a question mark:
-\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}P{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isasymand}\ Q}. Most of the time
+\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. Most of the time
you would rather not see the question marks. There is an attribute
\verb!no_vars! that you can attach to the theorem that turns its
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
@@ -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 := false|\verb!;!
+\verb|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! to \texttt{false} only
+Hint: Setting \verb!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{{\isachardot}{\isadigit{0}}},
e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their internal index. This can be avoided by
@@ -187,19 +187,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
\isamarkupsubsection{Qualified names%
}
\isamarkuptrue%
--- a/src/HOL/HOL.thy Thu Sep 02 17:01:49 2010 +0200
+++ b/src/HOL/HOL.thy Thu Sep 02 17:02:00 2010 +0200
@@ -32,6 +32,7 @@
("Tools/recfun_codegen.ML")
"Tools/async_manager.ML"
"Tools/try.ML"
+ ("Tools/cnf_funcs.ML")
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -1645,7 +1646,6 @@
"(\<not> \<not>(P)) = P"
by blast+
-
subsection {* Basic ML bindings *}
ML {*
@@ -1699,6 +1699,7 @@
val trans = @{thm trans}
*}
+use "Tools/cnf_funcs.ML"
subsection {* Code generator setup *}
--- a/src/HOL/Hilbert_Choice.thy Thu Sep 02 17:01:49 2010 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Sep 02 17:02:00 2010 +0200
@@ -7,7 +7,8 @@
theory Hilbert_Choice
imports Nat Wellfounded Plain
-uses ("Tools/meson.ML") ("Tools/choice_specification.ML")
+uses ("Tools/meson.ML")
+ ("Tools/choice_specification.ML")
begin
subsection {* Hilbert's epsilon *}
--- a/src/HOL/SAT.thy Thu Sep 02 17:01:49 2010 +0200
+++ b/src/HOL/SAT.thy Thu Sep 02 17:02:00 2010 +0200
@@ -10,7 +10,6 @@
theory SAT
imports Refute
uses
- "Tools/cnf_funcs.ML"
"Tools/sat_funcs.ML"
begin
--- a/src/HOL/Sledgehammer.thy Thu Sep 02 17:01:49 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Thu Sep 02 17:02:00 2010 +0200
@@ -26,6 +26,9 @@
("Tools/Sledgehammer/sledgehammer_isar.ML")
begin
+lemma TruepropI: "P \<equiv> Q \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
+by simp
+
definition skolem_id :: "'a \<Rightarrow> 'a" where
[no_atp]: "skolem_id = (\<lambda>x. x)"
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML Thu Sep 02 17:02:00 2010 +0200
@@ -10,7 +10,8 @@
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
- val cnf_axiom: theory -> thm -> thm list
+ val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
+ val cnf_axiom : theory -> thm -> thm list
end;
structure Clausifier : CLAUSIFIER =
@@ -228,19 +229,26 @@
|> Meson.make_nnf ctxt
in (th3, ctxt) end
+fun to_definitional_cnf_with_quantifiers thy th =
+ let
+ val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
+ val eqth = eqth RS @{thm eq_reflection}
+ val eqth = eqth RS @{thm TruepropI}
+ in Thm.equal_elim eqth th end
+
(* Convert a theorem to CNF, with Skolem functions as additional premises. *)
fun cnf_axiom thy th =
let
val ctxt0 = Variable.global_thm_context th
- val (nnfth, ctxt) = to_nnf th ctxt0
- val sko_ths = map (skolem_theorem_of_def thy)
- (assume_skolem_funs nnfth)
- val (cnfs, ctxt) = Meson.make_cnf sko_ths nnfth ctxt
+ val (nnf_th, ctxt) = to_nnf th ctxt0
+ val def_th = to_definitional_cnf_with_quantifiers thy nnf_th
+ val sko_ths = map (skolem_theorem_of_def thy) (assume_skolem_funs def_th)
+ val (cnf_ths, ctxt) = Meson.make_cnf sko_ths def_th ctxt
in
- cnfs |> map introduce_combinators_in_theorem
- |> Variable.export ctxt ctxt0
- |> Meson.finish_cnf
- |> map Thm.close_derivation
+ cnf_ths |> map introduce_combinators_in_theorem
+ |> Variable.export ctxt ctxt0
+ |> Meson.finish_cnf
+ |> map Thm.close_derivation
end
handle THM _ => []
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML Thu Sep 02 17:02:00 2010 +0200
@@ -795,13 +795,15 @@
fun generic_metis_tac mode ctxt ths i st0 =
let
+ val thy = ProofContext.theory_of ctxt
val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
if exists_type type_has_top_sort (prop_of st0) then
(warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
else
- Meson.MESON (maps neg_clausify)
+ Meson.MESON (K all_tac) (* TODO: Try (cnf.cnfx_rewrite_tac ctxt) *)
+ (maps neg_clausify)
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
ctxt i st0
end
--- a/src/HOL/Tools/cnf_funcs.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Sep 02 17:02:00 2010 +0200
@@ -430,7 +430,7 @@
in
make_cnf_disj_conj_r OF [thm1, thm2] (* (x' | (y1 & y2)) = ((x' | y1)' & (x' | y2)') *)
end
- | make_cnfx_disj_thm (Const (@{const_name Ex}, _) $ x') y' =
+ | make_cnfx_disj_thm (@{term "Ex::(bool => bool) => bool"} $ x') y' =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_l (* ((Ex x') | y') = (Ex (x' | y')) *)
val var = new_free ()
@@ -441,7 +441,7 @@
in
iff_trans OF [thm1, thm5] (* ((Ex x') | y') = (Ex v. body') *)
end
- | make_cnfx_disj_thm x' (Const (@{const_name Ex}, _) $ y') =
+ | make_cnfx_disj_thm x' (@{term "Ex::(bool => bool) => bool"} $ y') =
let
val thm1 = inst_thm thy [x', y'] make_cnfx_disj_ex_r (* (x' | (Ex y')) = (Ex (x' | y')) *)
val var = new_free ()
--- a/src/HOL/Tools/meson.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/HOL/Tools/meson.ML Thu Sep 02 17:02:00 2010 +0200
@@ -25,7 +25,9 @@
val depth_prolog_tac: thm list -> tactic
val gocls: thm list -> thm list
val skolemize_prems_tac: Proof.context -> thm list -> int -> tactic
- val MESON: (thm list -> thm list) -> (thm list -> tactic) -> Proof.context -> int -> tactic
+ val MESON:
+ (int -> tactic) -> (thm list -> thm list) -> (thm list -> tactic)
+ -> Proof.context -> int -> tactic
val best_meson_tac: (thm -> int) -> Proof.context -> int -> tactic
val safe_best_meson_tac: Proof.context -> int -> tactic
val depth_meson_tac: Proof.context -> int -> tactic
@@ -315,8 +317,8 @@
(nf prem) returns a LIST of theorems, we can backtrack to get all combinations.*)
fun resop nf [prem] = resolve_tac (nf prem) 1;
-(*Any need to extend this list with
- "HOL.type_class","HOL.eq_class","Pure.term"?*)
+(* Any need to extend this list with "HOL.type_class", "HOL.eq_class",
+ and "Pure.term"? *)
val has_meta_conn = exists_Const (member (op =) ["==", "==>", "=simp=>", "all", "prop"] o #1);
fun apply_skolem_theorem (th, rls) =
@@ -573,7 +575,8 @@
(*Make clauses from a list of theorems, previously Skolemized and put into nnf.
The resulting clauses are HOL disjunctions.*)
-fun make_clauses_unsorted ths = fold_rev add_clauses ths [];
+fun make_clauses_unsorted ths = fold_rev add_clauses ths []
+handle exn => error (ML_Compiler.exn_message exn) (*###*)
val make_clauses = sort_clauses o make_clauses_unsorted;
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
@@ -598,20 +601,22 @@
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
Function mkcl converts theorems to clauses.*)
-fun MESON mkcl cltac ctxt i st =
+fun MESON preskolem_tac mkcl cltac ctxt i st =
SELECT_GOAL
(EVERY [Object_Logic.atomize_prems_tac 1,
rtac ccontr 1,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
- EVERY1 [skolemize_prems_tac ctxt negs,
+ EVERY1 [preskolem_tac,
+ skolemize_prems_tac ctxt negs,
Subgoal.FOCUS (cltac o mkcl o #prems) ctxt']) ctxt 1]) i st
handle THM _ => no_tac st; (*probably from make_meta_clause, not first-order*)
+
(** Best-first search versions **)
(*ths is a list of additional clauses (HOL disjunctions) to use.*)
fun best_meson_tac sizef =
- MESON make_clauses
+ MESON (K all_tac) make_clauses
(fn cls =>
THEN_BEST_FIRST (resolve_tac (gocls cls) 1)
(has_fewer_prems 1, sizef)
@@ -625,7 +630,7 @@
(** Depth-first search version **)
val depth_meson_tac =
- MESON make_clauses
+ MESON (K all_tac) make_clauses
(fn cls => EVERY [resolve_tac (gocls cls) 1, depth_prolog_tac (make_horns cls)]);
@@ -645,7 +650,7 @@
fun iter_deepen_prolog_tac horns =
ITER_DEEPEN iter_deepen_limit (has_fewer_prems 1) (prolog_step_tac' horns);
-fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON make_clauses
+fun iter_deepen_meson_tac ctxt ths = ctxt |> MESON (K all_tac) make_clauses
(fn cls =>
(case (gocls (cls @ ths)) of
[] => no_tac (*no goal clauses*)
--- a/src/Pure/Isar/attrib.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Sep 02 17:02:00 2010 +0200
@@ -392,7 +392,8 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (register_config Unify.trace_bound_value #>
+ (register_config show_question_marks_value #>
+ register_config Unify.trace_bound_value #>
register_config Unify.search_bound_value #>
register_config Unify.trace_simp_value #>
register_config Unify.trace_types_value #>
--- a/src/Pure/Isar/proof_context.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Sep 02 17:02:00 2010 +0200
@@ -413,8 +413,7 @@
SOME (x, i) =>
(case try Name.dest_skolem x of
NONE => Pretty.mark Markup.var (Pretty.str s)
- | SOME x' => Pretty.mark Markup.skolem
- (Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
+ | SOME x' => Pretty.mark Markup.skolem (Pretty.str (Term.string_of_vname (x', i))))
| NONE => Pretty.mark Markup.var (Pretty.str s));
fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
@@ -536,14 +535,16 @@
fun certify_consts ctxt = Consts.certify (Syntax.pp ctxt) (tsig_of ctxt)
(not (abbrev_mode ctxt)) (consts_of ctxt);
-fun reject_schematic (Var (xi, _)) =
- error ("Unbound schematic variable: " ^ Term.string_of_vname xi)
- | reject_schematic (Abs (_, _, t)) = reject_schematic t
- | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
- | reject_schematic _ = ();
+fun expand_binds ctxt =
+ let
+ val Mode {pattern, schematic, ...} = get_mode ctxt;
-fun expand_binds ctxt =
- let val Mode {pattern, schematic, ...} = get_mode ctxt in
+ fun reject_schematic (t as Var _) =
+ error ("Unbound schematic variable: " ^ Syntax.string_of_term ctxt t)
+ | reject_schematic (Abs (_, _, t)) = reject_schematic t
+ | reject_schematic (t $ u) = (reject_schematic t; reject_schematic u)
+ | reject_schematic _ = ();
+ in
if pattern then I
else Variable.expand_binds ctxt #> (if schematic then I else tap reject_schematic)
end;
@@ -576,9 +577,9 @@
val _ =
pattern orelse schematic orelse
T |> Term.exists_subtype
- (fn TVar (xi, _) =>
+ (fn T as TVar (xi, _) =>
not (Type_Infer.is_param xi) andalso
- error ("Illegal schematic type variable: " ^ Term.string_of_vname xi)
+ error ("Illegal schematic type variable: " ^ Syntax.string_of_typ ctxt T)
| _ => false)
in T end;
--- a/src/Pure/ProofGeneral/preferences.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Thu Sep 02 17:02:00 2010 +0200
@@ -141,7 +141,7 @@
"prems-limit"
"Setting for maximum number of premises printed",
print_depth_pref,
- bool_pref show_question_marks
+ bool_pref show_question_marks_default
"show-question-marks"
"Show leading question mark of variable name"];
--- a/src/Pure/Syntax/printer.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Thu Sep 02 17:02:00 2010 +0200
@@ -12,6 +12,9 @@
val show_no_free_types: bool Unsynchronized.ref
val show_all_types: bool Unsynchronized.ref
val show_structs: bool Unsynchronized.ref
+ val show_question_marks_default: bool Unsynchronized.ref
+ val show_question_marks_value: Config.value Config.T
+ val show_question_marks: bool Config.T
val pp_show_brackets: Pretty.pp -> Pretty.pp
end;
@@ -52,6 +55,11 @@
val show_all_types = Unsynchronized.ref false;
val show_structs = Unsynchronized.ref false;
+val show_question_marks_default = Unsynchronized.ref true;
+val show_question_marks_value =
+ Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
+val show_question_marks = Config.bool show_question_marks_value;
+
fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
@@ -72,15 +80,18 @@
(* simple_ast_of *)
-fun simple_ast_of (Const (c, _)) = Ast.Constant c
- | simple_ast_of (Free (x, _)) = Ast.Variable x
- | simple_ast_of (Var (xi, _)) = Ast.Variable (Term.string_of_vname xi)
- | simple_ast_of (t as _ $ _) =
- let val (f, args) = strip_comb t in
- Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
- end
- | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
- | simple_ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
+fun simple_ast_of ctxt =
+ let
+ val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
+ fun ast_of (Const (c, _)) = Ast.Constant c
+ | ast_of (Free (x, _)) = Ast.Variable x
+ | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
+ | ast_of (t as _ $ _) =
+ let val (f, args) = strip_comb t
+ in Ast.mk_appl (ast_of f) (map ast_of args) end
+ | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
+ | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
+ in ast_of end;
@@ -88,14 +99,14 @@
fun ast_of_termT ctxt trf tm =
let
- fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
- | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
+ fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
+ | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
| ast_of (Const (a, _)) = trans a []
| ast_of (t as _ $ _) =
(case strip_comb t of
(Const (a, _), args) => trans a args
| (f, args) => Ast.Appl (map ast_of (f :: args)))
- | ast_of t = simple_ast_of t
+ | ast_of t = simple_ast_of ctxt t
and trans a args =
ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
@@ -168,7 +179,7 @@
if show_all_types
then Ast.mk_appl (constrain const T) (map ast_of ts)
else trans c T ts
- | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
+ | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
and trans a T args =
ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
@@ -176,9 +187,9 @@
and constrain t T =
if show_types andalso T <> dummyT then
- Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of t,
+ Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of ctxt t,
ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
- else simple_ast_of t;
+ else simple_ast_of ctxt t;
in
tm
|> Syn_Trans.prop_tr'
--- a/src/Pure/Thy/thy_output.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Thu Sep 02 17:02:00 2010 +0200
@@ -447,7 +447,7 @@
val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean);
-val _ = add_option "show_question_marks" (add_wrapper o setmp_CRITICAL show_question_marks o boolean);
+val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
--- a/src/Pure/term.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/Pure/term.ML Thu Sep 02 17:02:00 2010 +0200
@@ -114,7 +114,6 @@
val exists_type: (typ -> bool) -> term -> bool
val exists_subterm: (term -> bool) -> term -> bool
val exists_Const: (string * typ -> bool) -> term -> bool
- val show_question_marks: bool Unsynchronized.ref
end;
signature TERM =
@@ -983,11 +982,8 @@
(* display variables *)
-val show_question_marks = Unsynchronized.ref true;
-
fun string_of_vname (x, i) =
let
- val question_mark = if ! show_question_marks then "?" else "";
val idx = string_of_int i;
val dot =
(case rev (Symbol.explode x) of
@@ -996,9 +992,9 @@
| c :: _ => Symbol.is_digit c
| _ => true);
in
- if dot then question_mark ^ x ^ "." ^ idx
- else if i <> 0 then question_mark ^ x ^ idx
- else question_mark ^ x
+ if dot then "?" ^ x ^ "." ^ idx
+ else if i <> 0 then "?" ^ x ^ idx
+ else "?" ^ x
end;
fun string_of_vname' (x, ~1) = x
--- a/src/Tools/WWW_Find/find_theorems.ML Thu Sep 02 17:01:49 2010 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML Thu Sep 02 17:02:00 2010 +0200
@@ -143,9 +143,9 @@
fun html_thm ctxt (n, (thmref, thm)) =
let
- val string_of_thm =
+ val output_thm =
Output.output o Pretty.string_of_margin 100 o
- setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
+ Display.pretty_thm (Config.put show_question_marks false ctxt);
in
tag' "tr" (class ("row" ^ Int.toString (n mod 2)))
[
@@ -153,7 +153,7 @@
[span' (sorry_class thm)
[raw_text (Facts.string_of_ref thmref)]
],
- tag' "td" (class "thm") [pre noid (string_of_thm thm)]
+ tag' "td" (class "thm") [pre noid (output_thm thm)]
]
end;
@@ -236,7 +236,7 @@
end;
in
-val () = show_question_marks := false;
+val () = show_question_marks_default := false;
val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
end;