src/Provers/classical.ML
changeset 42807 e639d91d9073
parent 42799 4e33894aec6d
child 42810 2425068fe13a
     1.1 --- a/src/Provers/classical.ML	Sat May 14 16:27:47 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat May 14 17:55:08 2011 +0200
     1.3 @@ -306,14 +306,19 @@
     1.4      error ("Ill-formed destruction rule\n" ^ string_of_thm context th)
     1.5    else Tactic.make_elim th;
     1.6  
     1.7 -fun warn context msg rules th =
     1.8 -  mem_thm rules th andalso (warning (msg ^ string_of_thm context th); true);
     1.9 +fun warn_thm context msg th =
    1.10 +  if (case context of SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt | _ => false)
    1.11 +  then warning (msg ^ string_of_thm context th)
    1.12 +  else ();
    1.13  
    1.14 -fun warn_other context th (CS{safeIs, safeEs, hazIs, hazEs, ...}) =
    1.15 -  warn context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
    1.16 -  warn context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
    1.17 -  warn context "Rule already declared as introduction (intro)\n" hazIs th orelse
    1.18 -  warn context "Rule already declared as elimination (elim)\n" hazEs th;
    1.19 +fun warn_rules context msg rules th =
    1.20 +  mem_thm rules th andalso (warn_thm context msg th; true);
    1.21 +
    1.22 +fun warn_claset context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) =
    1.23 +  warn_rules context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse
    1.24 +  warn_rules context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse
    1.25 +  warn_rules context "Rule already declared as introduction (intro)\n" hazIs th orelse
    1.26 +  warn_rules context "Rule already declared as elimination (elim)\n" hazEs th;
    1.27  
    1.28  
    1.29  (*** Safe rules ***)
    1.30 @@ -321,7 +326,7 @@
    1.31  fun addSI w context th
    1.32      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.33        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.34 -  if warn context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
    1.35 +  if warn_rules context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs
    1.36    else
    1.37      let
    1.38        val th' = flat_rule th;
    1.39 @@ -329,7 +334,7 @@
    1.40          List.partition Thm.no_prems [th'];
    1.41        val nI = length safeIs + 1;
    1.42        val nE = length safeEs;
    1.43 -      val _ = warn_other context th cs;
    1.44 +      val _ = warn_claset context th cs;
    1.45      in
    1.46        CS
    1.47         {safeIs  = th::safeIs,
    1.48 @@ -348,7 +353,7 @@
    1.49  fun addSE w context th
    1.50      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.51        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.52 -  if warn context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
    1.53 +  if warn_rules context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs
    1.54    else if has_fewer_prems 1 th then
    1.55      error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
    1.56    else
    1.57 @@ -358,7 +363,7 @@
    1.58          List.partition (fn rl => nprems_of rl=1) [th'];
    1.59        val nI = length safeIs;
    1.60        val nE = length safeEs + 1;
    1.61 -      val _ = warn_other context th cs;
    1.62 +      val _ = warn_claset context th cs;
    1.63      in
    1.64        CS
    1.65         {safeEs  = th::safeEs,
    1.66 @@ -382,13 +387,13 @@
    1.67  fun addI w context th
    1.68      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.69        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.70 -  if warn context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
    1.71 +  if warn_rules context "Ignoring duplicate introduction (intro)\n" hazIs th then cs
    1.72    else
    1.73      let
    1.74        val th' = flat_rule th;
    1.75        val nI = length hazIs + 1;
    1.76        val nE = length hazEs;
    1.77 -      val _ = warn_other context th cs;
    1.78 +      val _ = warn_claset context th cs;
    1.79      in
    1.80        CS
    1.81         {hazIs = th :: hazIs,
    1.82 @@ -409,7 +414,7 @@
    1.83  fun addE w context th
    1.84      (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers,
    1.85        safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
    1.86 -  if warn context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
    1.87 +  if warn_rules context "Ignoring duplicate elimination (elim)\n" hazEs th then cs
    1.88    else if has_fewer_prems 1 th then
    1.89      error ("Ill-formed elimination rule\n" ^ string_of_thm context th)
    1.90    else
    1.91 @@ -417,7 +422,7 @@
    1.92        val th' = classical_rule (flat_rule th);
    1.93        val nI = length hazIs;
    1.94        val nE = length hazEs + 1;
    1.95 -      val _ = warn_other context th cs;
    1.96 +      val _ = warn_claset context th cs;
    1.97      in
    1.98        CS
    1.99         {hazEs = th :: hazEs,
   1.100 @@ -537,7 +542,7 @@
   1.101        mem_thm hazIs th orelse mem_thm hazEs th orelse
   1.102        mem_thm safeEs th' orelse mem_thm hazEs th'
   1.103      then delSI th (delSE th (delI context th (delE th (delSE th' (delE th' cs)))))
   1.104 -    else (warning ("Undeclared classical rule\n" ^ string_of_thm context th); cs)
   1.105 +    else (warn_thm context "Undeclared classical rule\n" th; cs)
   1.106    end;
   1.107  
   1.108