# HG changeset patch
# User boehmes
# Date 1251739717 -7200
# Node ID 3e6f5365971ef557b7479b0a0bdac99a677c244a
# Parent  ba0cf920a39c3d4766508ab26289e2e9039cc8f0
Mirabelle: explicit command blacklist, preliminary documentation

diff -r ba0cf920a39c -r 3e6f5365971e src/HOL/Tools/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Mon Aug 31 17:32:29 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Mon Aug 31 19:28:37 2009 +0200
@@ -116,10 +116,12 @@
 
 end
 
+val blacklist = ["disable_pr", "enable_pr", "done", "."]
+
 fun step_hook tr pre post =
  (* FIXME: might require wrapping into "interruptible" *)
   if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
-     not (member (op =) ["disable_pr", "enable_pr"] (Toplevel.name_of tr))
+     not (member (op =) blacklist (Toplevel.name_of tr))
   then basic_hook tr (Toplevel.proof_of pre) (SOME post)
   else ()   (* FIXME: add theory_hook here *)