# HG changeset patch
# User blanchet
# Date 1471170369 -7200
# Node ID 9ad6a63cc8bdc95b3cd36e1a03a69f9b003b50bb
# Parent  e58bcea9492a59bbc4684eb8c42634f762c4419d
optimization in MaSh parsing

diff -r e58bcea9492a -r 9ad6a63cc8bd src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -289,11 +289,13 @@
               "Filtering " ^ string_of_int (length all_facts) ^ " facts (MaSh algorithm: " ^
               str_of_mash_algorithm (the_mash_algorithm ()) ^ ")"));
           in
+timeit (fn () =>
             all_facts
             |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
             |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
             |> spy ? tap (fn factss => spying spy (fn () =>
               (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
+) (*###*)
           end
 
         fun launch_provers () =
diff -r e58bcea9492a -r 9ad6a63cc8bd src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 14 12:26:09 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Aug 14 12:26:09 2016 +0200
@@ -533,10 +533,13 @@
   | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
 
 val encode_str = String.translate meta_char
-val decode_str = String.explode #> unmeta_chars []
+val encode_strs = map encode_str #> space_implode " "
 
-val encode_strs = map encode_str #> space_implode " "
-val decode_strs = space_explode " " #> map decode_str
+fun decode_str s =
+  if String.isSubstring "%" s then unmeta_chars [] (String.explode s) else s;
+
+fun decode_strs s =
+  space_explode " " s |> String.isSubstring "%" s ? map decode_str;
 
 datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop