--- a/src/Doc/IsarRef/Spec.thy Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Doc/IsarRef/Spec.thy Wed Sep 11 16:16:45 2013 +0200
@@ -251,7 +251,7 @@
Here is an artificial example of bundling various configuration
options: *}
-bundle trace = [[simp_trace, blast_trace, linarith_trace, metis_trace, smt_trace]]
+bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
lemma "x = x"
including trace by metis
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy Wed Sep 11 15:49:39 2013 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy Wed Sep 11 16:16:45 2013 +0200
@@ -1,5 +1,5 @@
-(* Title: HOL/ex/Adhoc_Overloading_Examples.thy
- Author: Christian Sternagel
+(* Title: HOL/ex/Adhoc_Overloading_Examples.thy
+ Author: Christian Sternagel
*)
header {* Ad Hoc Overloading *}
--- a/src/Provers/blast.ML Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Provers/blast.ML Wed Sep 11 16:16:45 2013 +0200
@@ -78,8 +78,8 @@
(* options *)
val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
-val (trace, setup_trace) = Attrib.config_bool @{binding blast_trace} (K false);
-val (stats, setup_stats) = Attrib.config_bool @{binding blast_stats} (K false);
+val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false);
+val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false);
datatype term =
@@ -1298,8 +1298,6 @@
val setup =
setup_depth_limit #>
- setup_trace #>
- setup_stats #>
Method.setup @{binding blast}
(Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
(fn NONE => SIMPLE_METHOD' o blast_tac
--- a/src/Pure/General/name_space.ML Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Pure/General/name_space.ML Wed Sep 11 16:16:45 2013 +0200
@@ -30,6 +30,7 @@
val extern: Proof.context -> T -> string -> xstring
val extern_ord: Proof.context -> T -> string * string -> order
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
+ val pretty: Proof.context -> T -> string -> Pretty.T
val hide: bool -> string -> T -> T
val merge: T * T -> T
type naming
@@ -194,6 +195,8 @@
fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
+fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
+
(* modify internals *)
--- a/src/Pure/Isar/class.ML Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Pure/Isar/class.ML Wed Sep 11 16:16:45 2013 +0200
@@ -182,14 +182,14 @@
fun prt_param (c, ty) =
Pretty.block
- [Pretty.mark_str (Name_Space.markup_extern ctxt const_space c), Pretty.str " ::",
+ [Name_Space.pretty ctxt const_space c, Pretty.str " ::",
Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
fun prt_entry class =
Pretty.block
([Pretty.command "class", Pretty.brk 1,
- Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
- Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
+ Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk,
+ Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
(case try (Axclass.get_info thy) class of
NONE => []
| SOME {params, ...} =>
--- a/src/Tools/adhoc_overloading.ML Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML Wed Sep 11 16:16:45 2013 +0200
@@ -1,5 +1,5 @@
-(* Author: Alexander Krauss, TU Muenchen
- Author: Christian Sternagel, University of Innsbruck
+(* Author: Alexander Krauss, TU Muenchen
+ Author: Christian Sternagel, University of Innsbruck
Adhoc overloading of constants based on their types.
*)
@@ -21,6 +21,7 @@
val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
+
(* errors *)
fun err_duplicate_variant oconst =
@@ -32,19 +33,27 @@
fun err_not_overloaded oconst =
error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
-fun err_unresolved_overloading ctxt (c, T) t instances =
- let val ctxt' = Config.put show_variants true ctxt
+fun err_unresolved_overloading ctxt0 (c, T) t instances =
+ let
+ val ctxt = Config.put show_variants true ctxt0
+ val const_space = Proof_Context.const_space ctxt
+ val prt_const =
+ Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_typ ctxt T)]
in
- cat_lines (
- "Unresolved overloading of constant" ::
- quote c ^ " :: " ^ quote (Syntax.string_of_typ ctxt' T) ::
- "in term " ::
- quote (Syntax.string_of_term ctxt' t) ::
- (if null instances then "no instances" else "multiple instances:") ::
- map (Markup.markup Markup.item o Syntax.string_of_term ctxt') instances)
- |> error
+ error (Pretty.string_of (Pretty.chunks [
+ Pretty.block [
+ Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1,
+ prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1,
+ Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]],
+ Pretty.block (
+ (if null instances then [Pretty.str "no instances"]
+ else Pretty.fbreaks (
+ Pretty.str "multiple instances:" ::
+ map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))]))
end;
+
(* generic data *)
fun variants_eq ((v1, T1), (v2, T2)) =
@@ -133,6 +142,7 @@
val generic_remove_variant = generic_variant false;
end;
+
(* check / uncheck *)
fun unifiable_with thy T1 T2 =
@@ -178,6 +188,7 @@
| (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT));
in map check_unresolved end;
+
(* setup *)
val _ = Context.>>
@@ -185,6 +196,7 @@
#> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
#> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck);
+
(* commands *)
fun generic_adhoc_overloading_cmd add =
--- a/src/Tools/subtyping.ML Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Tools/subtyping.ML Wed Sep 11 16:16:45 2013 +0200
@@ -1046,9 +1046,9 @@
val tmaps =
sort (Name_Space.extern_ord ctxt type_space o pairself #1)
(Symtab.dest (tmaps_of ctxt));
- fun show_map (x, (t, _)) =
+ fun show_map (c, (t, _)) =
Pretty.block
- [Pretty.mark_str (Name_Space.markup_extern ctxt type_space x), Pretty.str ":",
+ [Name_Space.pretty ctxt type_space c, Pretty.str ":",
Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)];
in
[Pretty.big_list "coercions between base types:" (map show_coercion simple),