# HG changeset patch
# User blanchet
# Date 1282208579 -7200
# Node ID db482afec7f0bce0664d613c7e2286120495929b
# Parent  f881b865dcf4e63509919a2f79466ffaeec12497
no spurious trailing "\n" at the end of Sledgehammer's output

diff -r f881b865dcf4 -r db482afec7f0 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 18 20:53:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 19 11:02:59 2010 +0200
@@ -348,7 +348,7 @@
         proof_text isar_proof
             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
             (full_types, minimize_command, proof, axiom_names, th, subgoal)
-      | SOME failure => (string_for_failure failure ^ "\n", [])
+      | SOME failure => (string_for_failure failure, [])
   in
     {outcome = outcome, message = message, pool = pool,
      used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
diff -r f881b865dcf4 -r db482afec7f0 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Aug 18 20:53:55 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 19 11:02:59 2010 +0200
@@ -10,7 +10,6 @@
 sig
   type minimize_command = string list -> string
 
-  val metis_line: bool -> int -> int -> string list -> string
   val metis_proof_text:
     bool * minimize_command * string * string vector * thm * int
     -> string * string list
@@ -598,14 +597,14 @@
   metis_using ls ^ metis_apply i n ^ metis_call full_types ss
 fun metis_line full_types i n ss =
   "Try this command: " ^
-  Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ ".\n"
+  Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "."
 fun minimize_line _ [] = ""
   | minimize_line minimize_command facts =
     case minimize_command facts of
       "" => ""
     | command =>
-      "To minimize the number of lemmas, try this: " ^
-      Markup.markup Markup.sendback command ^ ".\n"
+      "\nTo minimize the number of lemmas, try this: " ^
+      Markup.markup Markup.sendback command ^ "."
 
 val unprefix_chained = perhaps (try (unprefix chained_prefix))