--- a/Admin/makedist Wed Dec 09 16:46:04 2009 +0100
+++ b/Admin/makedist Wed Dec 09 21:33:50 2009 +0100
@@ -148,8 +148,6 @@
cp doc/isabelle*.eps lib/logo
-rm Isabelle Isabelle.exe
-
if [ -z "$RELEASE" ]; then
{
--- a/doc-src/Nitpick/nitpick.tex Wed Dec 09 16:46:04 2009 +0100
+++ b/doc-src/Nitpick/nitpick.tex Wed Dec 09 21:33:50 2009 +0100
@@ -1517,15 +1517,13 @@
\hbox{}\qquad Free variables: \nopagebreak \\
\hbox{}\qquad\qquad $t = N~a_3~1~\Lambda~\Lambda$ \\
\hbox{}\qquad\qquad $x = a_4$ \\[2\smallskipamount]
-Hint: Maybe you forgot a type constraint?
\postw
-It's hard to see why this is a counterexample. The hint is of no help here. To
-improve readability, we will restrict the theorem to \textit{nat}, so that we
-don't need to look up the value of the $\textit{op}~{<}$ constant to find out
-which element is smaller than the other. In addition, we will tell Nitpick to
-display the value of $\textit{insort}~t~x$ using the \textit{eval} option. This
-gives
+It's hard to see why this is a counterexample. To improve readability, we will
+restrict the theorem to \textit{nat}, so that we don't need to look up the value
+of the $\textit{op}~{<}$ constant to find out which element is smaller than the
+other. In addition, we will tell Nitpick to display the value of
+$\textit{insort}~t~x$ using the \textit{eval} option. This gives
\prew
\textbf{theorem} \textit{wf\_insort\_nat}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~(x\Colon\textit{nat}))$'' \\
--- a/lib/scripts/getsettings Wed Dec 09 16:46:04 2009 +0100
+++ b/lib/scripts/getsettings Wed Dec 09 21:33:50 2009 +0100
@@ -51,6 +51,7 @@
if [ "$OSTYPE" = cygwin ]; then
CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
function jvmpath() { cygpath -w -p "$@"; }
+ CYGWIN_ROOT="$(jvmpath "/")"
else
function jvmpath() { echo "$@"; }
fi
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Dec 09 16:46:04 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Dec 09 21:33:50 2009 +0100
@@ -164,17 +164,15 @@
(* ('a * bool option) list -> bool *)
fun none_true asgns = forall (not_equal (SOME true) o snd) asgns
-val weaselly_sorts =
- [@{sort default}, @{sort zero}, @{sort one}, @{sort plus}, @{sort minus},
- @{sort uminus}, @{sort times}, @{sort inverse}, @{sort abs}, @{sort sgn},
- @{sort ord}, @{sort eq}, @{sort number}]
-(* theory -> typ -> bool *)
-fun is_tfree_with_weaselly_sort thy (TFree (_, S)) =
- exists (curry (Sign.subsort thy) S) weaselly_sorts
- | is_tfree_with_weaselly_sort _ _ = false
-(* theory term -> bool *)
-val has_weaselly_sorts =
- exists_type o exists_subtype o is_tfree_with_weaselly_sort
+val syntactic_sorts =
+ @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,eq}"} @
+ @{sort number}
+(* typ -> bool *)
+fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
+ subset (op =) (S, syntactic_sorts)
+ | has_tfree_syntactic_sort _ = false
+(* term -> bool *)
+val has_syntactic_sorts = exists_type (exists_subtype has_tfree_syntactic_sort)
(* (unit -> string) -> Pretty.T *)
fun plazy f = Pretty.blk (0, pstrs (f ()))
@@ -184,8 +182,16 @@
orig_t =
let
val timer = Timer.startRealTimer ()
- val thy = Proof.theory_of state
+ val user_thy = Proof.theory_of state
+ val nitpick_thy = ThyInfo.get_theory "Nitpick"
+ val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy))
+ val thy = if nitpick_thy_missing then
+ Theory.begin_theory "Nitpick_Internal" [nitpick_thy, user_thy]
+ |> Theory.checkpoint
+ else
+ user_thy
val ctxt = Proof.context_of state
+ |> nitpick_thy_missing ? Context.raw_transfer thy
val {cards_assigns, maxes_assigns, iters_assigns, bisim_depths, boxes,
monos, wfs, sat_solver, blocking, falsify, debug, verbose, overlord,
user_axioms, assms, merge_type_vars, destroy_constrs, specialize,
@@ -575,7 +581,7 @@
| NONE => print "No confirmation by \"auto\".")
else
();
- if has_weaselly_sorts thy orig_t then
+ if has_syntactic_sorts orig_t then
print "Hint: Maybe you forgot a type constraint?"
else
();
@@ -801,7 +807,7 @@
(* int -> int -> scope list -> int * int * int -> Kodkod.outcome *)
fun run_batches _ _ [] (max_potential, max_genuine, donno) =
if donno > 0 andalso max_genuine > 0 then
- (print_m (fn () => excipit "ran into difficulties"); "unknown")
+ (print_m (fn () => excipit "ran out of juice"); "unknown")
else if max_genuine = original_max_genuine then
if max_potential = original_max_potential then
(print_m (K ("Nitpick found no " ^ word_model ^ ".")); "none")
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Dec 09 16:46:04 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Dec 09 21:33:50 2009 +0100
@@ -250,8 +250,8 @@
val nat_subscript = subscript o signed_string_of_int
(* Time.time option -> ('a -> 'b) -> 'a -> 'b *)
-fun time_limit NONE f = f
- | time_limit (SOME delay) f = TimeLimit.timeLimit delay f
+fun time_limit NONE = I
+ | time_limit (SOME delay) = TimeLimit.timeLimit delay
(* Time.time option -> tactic -> tactic *)
fun DETERM_TIMEOUT delay tac st =
--- a/src/Pure/General/swing_thread.scala Wed Dec 09 16:46:04 2009 +0100
+++ b/src/Pure/General/swing_thread.scala Wed Dec 09 21:33:50 2009 +0100
@@ -10,6 +10,8 @@
import javax.swing.{SwingUtilities, Timer}
import java.awt.event.{ActionListener, ActionEvent}
+import scala.actors.{Future, Futures}
+
object Swing_Thread
{
@@ -21,13 +23,17 @@
/* main dispatch queue */
- def now[A](body: => A): A = {
+ def now[A](body: => A): A =
+ {
var result: Option[A] = None
if (SwingUtilities.isEventDispatchThread()) { result = Some(body) }
else SwingUtilities.invokeAndWait(new Runnable { def run = { result = Some(body) } })
result.get
}
+ def future[A](body: => A): Future[A] =
+ Futures.future(now(body))
+
def later(body: => Unit) {
if (SwingUtilities.isEventDispatchThread()) body
else SwingUtilities.invokeLater(new Runnable { def run = body })
--- a/src/Pure/System/cygwin.scala Wed Dec 09 16:46:04 2009 +0100
+++ b/src/Pure/System/cygwin.scala Wed Dec 09 21:33:50 2009 +0100
@@ -81,11 +81,16 @@
// new-style setup (Cygwin 1.7)
private val CYGWIN_SETUP1 = "Software\\Cygwin\\setup"
- private val CYGWIN_SETUP2 = "Software\\Wow6432Node\\Cygwin\\setup" // !?
+ private val CYGWIN_SETUP2 = "Software\\Wow6432Node\\Cygwin\\setup"
def config(): (String, String) =
{
- query_registry(CYGWIN_SETUP1, "rootdir") match {
+ val cygwin_root = java.lang.System.getenv("CYGWIN_ROOT")
+
+ (if (cygwin_root != null && cygwin_root != "") Some(cygwin_root) else None) orElse
+ query_registry(CYGWIN_SETUP1, "rootdir") orElse
+ query_registry(CYGWIN_SETUP2, "rootdir") match
+ {
case Some(root) => (root, "/cygdrive")
case None =>
val root =
--- a/src/Pure/System/isabelle_system.scala Wed Dec 09 16:46:04 2009 +0100
+++ b/src/Pure/System/isabelle_system.scala Wed Dec 09 21:33:50 2009 +0100
@@ -341,11 +341,11 @@
private def create_font(name: String) =
Font.createFont(Font.TRUETYPE_FONT, platform_file(name))
- def register_fonts(): Boolean =
- {
+ def register_fonts() {
val ge = GraphicsEnvironment.getLocalGraphicsEnvironment()
val ok1 = ge.registerFont(create_font("~~/lib/fonts/IsabelleText.ttf"))
val ok2 = ge.registerFont(create_font("~~/lib/fonts/IsabelleTextBold.ttf"))
- ok1 && ok2
+ if (!(ok1 && ok2) && !ge.getAvailableFontFamilyNames.contains(font_family))
+ error("Font family " + font_family + " unavailable")
}
}