--- a/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py Thu Sep 12 10:35:33 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py Thu Sep 12 10:40:53 2013 +0200
@@ -1,4 +1,4 @@
-#!/usr/bin/python
+#!/usr/bin/env python
# Title: HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
# Author: Daniel Kuehlwein, ICIS, Radboud University Nijmegen
# Copyright 2012
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Sep 12 10:35:33 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Sep 12 10:40:53 2013 +0200
@@ -218,9 +218,15 @@
Date.fmt ".%Y%m%d_%H%M%S__" (Date.fromTimeLocal (Time.now ())) ^
serial_string ()
+(* Avoid scientific notation *)
+fun safe_str_of_real r =
+ if r < 0.00001 then "0.00001"
+ else if r >= 1000000.0 then "1000000"
+ else Markup.print_real r
+
fun encode_feature (name, weight) =
encode_str name ^
- (if Real.== (weight, 1.0) then "" else "=" ^ Markup.print_real weight)
+ (if Real.== (weight, 1.0) then "" else "=" ^ safe_str_of_real weight)
val encode_features = map encode_feature #> space_implode " "
@@ -445,7 +451,8 @@
end
-fun mash_unlearn ctxt ({overlord, ...} : params) = clear_state ctxt overlord
+fun mash_unlearn ctxt ({overlord, ...} : params) =
+ (clear_state ctxt overlord; Output.urgent_message "Reset MaSh")
(*** Isabelle helpers ***)