# HG changeset patch
# User wenzelm
# Date 1305388508 -7200
# Node ID e639d91d9073a5da9e7d6bcb7a2a2086f2c35e64
# Parent  4b660cdab9b71f597a9471fbfa492efe82ab20ab
more precise warnings: observe context visibility;

diff -r 4b660cdab9b7 -r e639d91d9073 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat May 14 16:27:47 2011 +0200
+++ b/src/Provers/classical.ML	Sat May 14 17:55:08 2011 +0200
@@ -306,14 +306,19 @@
     error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
   else Tactic.make_elim th;
 
-fun warn context msg rules th =
-  mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true);
+fun warn_thm context msg th =
+  if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false)
+  then warning (msg ^ string_of_thm context th)
+  else ();
 
-fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
-  warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
-  warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
-  warn context "Rule already declared as introduction (intro)\n" hazIs th orelse
-  warn context "Rule already declared as elimination (elim)\n" hazEs th;
+fun warn_rules context msg rules th =
+  mem_thm rules th andalso (warn_thm context msg th; true);
+
+fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
+  warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
+  warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
+  warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse
+  warn_rules context "Rule already declared as elimination (elim)\n" hazEs th;
 
 
 (*** Safe rules ***)
@@ -321,7 +326,7 @@
 fun addSI w context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
+  if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
   else
     let
       val th' = flat_rule th;
@@ -329,7 +334,7 @@
         List.partition Thm.no_prems [th'];
       val nI = length safeIs + 1;
       val nE = length safeEs;
-      val _ = warn_other context th cs;
+      val _ = warn_claset context th cs;
     in
       CS
        {safeIs  = th::safeIs,
@@ -348,7 +353,7 @@
 fun addSE w context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
+  if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
   else if has_fewer_prems 1 th then
     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
@@ -358,7 +363,7 @@
         List.partition (fn rl => nprems_of rl=1) [th'];
       val nI = length safeIs;
       val nE = length safeEs + 1;
-      val _ = warn_other context th cs;
+      val _ = warn_claset context th cs;
     in
       CS
        {safeEs  = th::safeEs,
@@ -382,13 +387,13 @@
 fun addI w context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
+  if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
   else
     let
       val th' = flat_rule th;
       val nI = length hazIs + 1;
       val nE = length hazEs;
-      val _ = warn_other context th cs;
+      val _ = warn_claset context th cs;
     in
       CS
        {hazIs = th :: hazIs,
@@ -409,7 +414,7 @@
 fun addE w context th
     (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
       safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
-  if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
+  if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
   else if has_fewer_prems 1 th then
     error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
   else
@@ -417,7 +422,7 @@
       val th' = classical_rule (flat_rule th);
       val nI = length hazIs;
       val nE = length hazEs + 1;
-      val _ = warn_other context th cs;
+      val _ = warn_claset context th cs;
     in
       CS
        {hazEs = th :: hazEs,
@@ -537,7 +542,7 @@
       mem_thm hazIs th orelse mem_thm hazEs th orelse
       mem_thm safeEs th' orelse mem_thm hazEs th'
     then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
-    else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs)
+    else (warn_thm context "Undeclared classical rule\n" th; cs)
   end;