# HG changeset patch
# User blanchet
# Date 1378975253 -7200
# Node ID f9682fdfd47b83d884e466dd180009254226aae4
# Parent  5d3ec1198a6432b71914d8acc57a72e9a4e46227
minor fixes

diff -r 5d3ec1198a64 -r f9682fdfd47b src/HOL/Tools/Sledgehammer/MaSh/src/compareStats.py
--- 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
diff -r 5d3ec1198a64 -r f9682fdfd47b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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 ***)