# HG changeset patch
# User wenzelm
# Date 1374248112 -7200
# Node ID 0e4bacf21e771db3480ab8bd36f6d2cd5ca351ad
# Parent  13e6014ed42bb40a5e8dde053277fdc854b37d3a
turned pattern unify flag into configuration option (global only);

diff -r 13e6014ed42b -r 0e4bacf21e77 src/Doc/Tutorial/Rules/Basic.thy
--- a/src/Doc/Tutorial/Rules/Basic.thy	Fri Jul 19 16:36:13 2013 +0200
+++ b/src/Doc/Tutorial/Rules/Basic.thy	Fri Jul 19 17:35:12 2013 +0200
@@ -187,7 +187,7 @@
 
 text{*unification failure trace *}
 
-ML "trace_unify_fail := true"
+declare [[unify_trace_failure = 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 "trace_unify_fail := false"
+declare [[unify_trace_failure = false]]
 
 
 text{*Quantifiers*}
diff -r 13e6014ed42b -r 0e4bacf21e77 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jul 19 16:36:13 2013 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Jul 19 17:35:12 2013 +0200
@@ -573,6 +573,7 @@
   register_config Goal_Display.show_consts_raw #>
   register_config Display.show_hyps_raw #>
   register_config Display.show_tags_raw #>
+  register_config Pattern.unify_trace_failure_raw #>
   register_config Unify.trace_bound_raw #>
   register_config Unify.search_bound_raw #>
   register_config Unify.trace_simp_raw #>
diff -r 13e6014ed42b -r 0e4bacf21e77 src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Fri Jul 19 16:36:13 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Fri Jul 19 17:35:12 2013 +0200
@@ -107,7 +107,7 @@
 val _ =
   ProofGeneral.preference_bool ProofGeneral.category_tracing
     NONE
-    Pattern.trace_unify_fail
+    Pattern.unify_trace_failure_default
     "trace-unification"
     "Output error diagnostics during unification";
 
diff -r 13e6014ed42b -r 0e4bacf21e77 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Jul 19 16:36:13 2013 +0200
+++ b/src/Pure/pattern.ML	Fri Jul 19 17:35:12 2013 +0200
@@ -12,7 +12,9 @@
 
 signature PATTERN =
 sig
-  val trace_unify_fail: bool Unsynchronized.ref
+  val unify_trace_failure_default: bool Unsynchronized.ref
+  val unify_trace_failure_raw: Config.raw
+  val unify_trace_failure: bool Config.T
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val first_order_match: theory -> term * term
     -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -38,7 +40,10 @@
 exception Unif;
 exception Pattern;
 
-val trace_unify_fail = Unsynchronized.ref false;
+val unify_trace_failure_default = Unsynchronized.ref false;
+val unify_trace_failure_raw =
+  Config.declare_global "unify_trace_failure" (fn _ => Config.Bool (! unify_trace_failure_default));
+val unify_trace_failure = Config.bool unify_trace_failure_raw;
 
 fun string_of_term thy env binders t =
   Syntax.string_of_term_global thy
@@ -48,28 +53,30 @@
 fun bnames binders is = space_implode " " (map (bname binders) is);
 
 fun typ_clash thy (tye,T,U) =
-  if !trace_unify_fail
+  if Config.get_global thy unify_trace_failure
   then let val t = Syntax.string_of_typ_global thy (Envir.norm_type tye T)
            and u = Syntax.string_of_typ_global thy (Envir.norm_type tye U)
        in tracing("The following types do not unify:\n" ^ t ^ "\n" ^ u) end
   else ()
 
-fun clash a b =
-  if !trace_unify_fail then tracing("Clash: " ^ a ^ " =/= " ^ b) else ()
+fun clash thy a b =
+  if Config.get_global thy unify_trace_failure then tracing("Clash: " ^ a ^ " =/= " ^ b) else ()
 
 fun boundVar binders i =
   "bound variable " ^ bname binders i ^ " (depth " ^ string_of_int i ^ ")";
 
-fun clashBB binders i j =
-  if !trace_unify_fail then clash (boundVar binders i) (boundVar binders j)
+fun clashBB thy binders i j =
+  if Config.get_global thy unify_trace_failure
+  then clash thy (boundVar binders i) (boundVar binders j)
   else ()
 
-fun clashB binders i s =
-  if !trace_unify_fail then clash (boundVar binders i) s
+fun clashB thy binders i s =
+  if Config.get_global thy unify_trace_failure
+  then clash thy (boundVar binders i) s
   else ()
 
 fun proj_fail thy (env,binders,F,_,is,t) =
-  if !trace_unify_fail
+  if Config.get_global thy unify_trace_failure
   then let val f = Term.string_of_vname F
            val xs = bnames binders is
            val u = string_of_term thy env binders t
@@ -81,7 +88,7 @@
   else ()
 
 fun ocheck_fail thy (F,t,binders,env) =
-  if !trace_unify_fail
+  if Config.get_global thy unify_trace_failure
   then let val f = Term.string_of_vname F
            val u = string_of_term thy env binders t
        in tracing("Variable " ^ f ^ " occurs in term\n" ^ u ^
@@ -251,20 +258,20 @@
       | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB thy (env,binders,i,j,ss,ts)
       | ((Abs(_),_),_)                => raise Pattern
       | (_,(Abs(_),_))                => raise Pattern
-      | ((Const(c,_),_),(Free(f,_),_)) => (clash c f; raise Unif)
-      | ((Const(c,_),_),(Bound i,_))   => (clashB binders i c; raise Unif)
-      | ((Free(f,_),_),(Const(c,_),_)) => (clash f c; raise Unif)
-      | ((Free(f,_),_),(Bound i,_))    => (clashB binders i f; raise Unif)
-      | ((Bound i,_),(Const(c,_),_))   => (clashB binders i c; raise Unif)
-      | ((Bound i,_),(Free(f,_),_))    => (clashB binders i f; raise Unif)
+      | ((Const(c,_),_),(Free(f,_),_)) => (clash thy c f; raise Unif)
+      | ((Const(c,_),_),(Bound i,_))   => (clashB thy binders i c; raise Unif)
+      | ((Free(f,_),_),(Const(c,_),_)) => (clash thy f c; raise Unif)
+      | ((Free(f,_),_),(Bound i,_))    => (clashB thy binders i f; raise Unif)
+      | ((Bound i,_),(Const(c,_),_))   => (clashB thy binders i c; raise Unif)
+      | ((Bound i,_),(Free(f,_),_))    => (clashB thy binders i f; raise Unif)
 
 
 and rigidrigid thy (env,binders,(a,Ta),(b,Tb),ss,ts) =
-      if a<>b then (clash a b; raise Unif)
+      if a<>b then (clash thy a b; raise Unif)
       else env |> unify_types thy (Ta,Tb) |> fold (unif thy binders) (ss~~ts)
 
 and rigidrigidB thy (env,binders,i,j,ss,ts) =
-     if i <> j then (clashBB binders i j; raise Unif)
+     if i <> j then (clashBB thy binders i j; raise Unif)
      else fold (unif thy binders) (ss~~ts) env
 
 and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
@@ -480,4 +487,3 @@
 
 end;
 
-val trace_unify_fail = Pattern.trace_unify_fail;
diff -r 13e6014ed42b -r 0e4bacf21e77 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jul 19 16:36:13 2013 +0200
+++ b/src/Pure/thm.ML	Fri Jul 19 17:35:12 2013 +0200
@@ -1735,7 +1735,7 @@
             (state, (stpairs, Bs, Bi, C), true);
         fun res [] = Seq.empty
           | res ((eres_flg, rule)::brules) =
-              if !Pattern.trace_unify_fail orelse
+              if Config.get_global (theory_of_thm state) Pattern.unify_trace_failure orelse
                  could_bires (Hs, B, eres_flg, rule)
               then Seq.make (*delay processing remainder till needed*)
                   (fn()=> SOME(compose (eres_flg, lift rule, nprems_of rule),