explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;

--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -130,7 +130,7 @@
 
 fun output_line cert =
   "To repeat this proof with a certifiate use this command:\n" ^
-    Active.sendback_markup ("by (sos_cert \"" ^ cert ^ "\")")
+    Active.sendback_markup [] ("by (sos_cert \"" ^ cert ^ "\")")
 
 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
 

--- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Jul 18 20:53:22 2013 +0200
@@ -235,7 +235,7 @@
 
 ML {*
   fun make_benchmark n =
-    writeln (Active.sendback_markup
+    writeln (Active.sendback_markup []
       ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
         (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
 *}

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -466,7 +466,8 @@
                   pstrs "Hint: To check that the induction hypothesis is \
                         \general enough, try this command: " @
                   [Pretty.mark
-                    (Active.make_markup Markup.sendbackN {implicit = false, properties = []})
+                    (Active.make_markup Markup.sendbackN
+                      {implicit = false, properties = [Markup.padding_command]})
                     (Pretty.blk (0,
                        pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
             else

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -955,7 +955,8 @@
       |> drop (length old_facts)
     end
 
-fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
+fun sendback sub =
+  Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub)
 
 val commit_timeout = seconds 30.0
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -13,7 +13,7 @@
 
   val string_of_reconstructor : reconstructor -> string
 
-  val one_line_proof_text : int -> one_line_params -> string
+  val one_line_proof_text : bool -> int -> one_line_params -> string
 
   val string_of_proof :
     Proof.context -> string -> string -> int -> int -> isar_proof -> string
@@ -71,21 +71,24 @@
   using_labels ls ^ apply_on_subgoal i n ^
   command_call (string_of_reconstructor reconstr) ss
 
-fun try_command_line banner time command =
-  banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
+fun try_command_line auto banner time command =
+  banner ^ ": " ^
+  Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^
+  show_time time ^ "."
 
-fun minimize_line _ [] = ""
-  | minimize_line minimize_command ss =
+fun minimize_line _ _ [] = ""
+  | minimize_line auto minimize_command ss =
     case minimize_command ss of
       "" => ""
     | command =>
-      "\nTo minimize: " ^ Active.sendback_markup command ^ "."
+      "\nTo minimize: " ^
+      Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^ "."
 
 fun split_used_facts facts =
   facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
         |> pairself (sort_distinct (string_ord o pairself fst))
 
-fun one_line_proof_text num_chained
+fun one_line_proof_text auto num_chained
         (preplay, banner, used_facts, minimize_command, subgoal,
          subgoal_count) =
   let
@@ -109,8 +112,8 @@
                      ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
                      \solve this.)"
           else
-            try_command_line banner ext_time)
-  in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
+            try_command_line auto banner ext_time)
+  in try_line ^ minimize_line auto minimize_command (map fst (extra @ chained)) end
 
 
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -973,7 +973,7 @@
                    subgoal, subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
-                proof_text ctxt isar_proofs isar_params num_chained
+                proof_text ctxt (mode = Auto_Try) isar_proofs isar_params num_chained
                            one_line_params
               end,
            (if verbose then
@@ -1177,7 +1177,7 @@
                                          preplay,
                  subgoal, subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
-            in one_line_proof_text num_chained one_line_params end,
+            in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
          if verbose then
            "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
          else
@@ -1222,7 +1222,7 @@
                  minimize_command override_params name, subgoal,
                  subgoal_count)
               val num_chained = length (#facts (Proof.goal state))
-            in one_line_proof_text num_chained one_line_params end,
+            in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
        message_tail = ""}
     | play =>
       let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -25,9 +25,9 @@
     Proof.context -> (string * stature) list vector -> 'a proof ->
     string list option
   val isar_proof_text :
-    Proof.context -> bool option -> isar_params -> one_line_params -> string
+    Proof.context -> bool -> bool option -> isar_params -> one_line_params -> string
   val proof_text :
-    Proof.context -> bool option -> isar_params -> int -> one_line_params
+    Proof.context -> bool -> bool option -> isar_params -> int -> one_line_params
     -> string
 end;
 
@@ -413,7 +413,7 @@
   * string Symtab.table * (string * stature) list vector
   * (string * term) list * int Symtab.table * string proof * thm
 
-fun isar_proof_text ctxt isar_proofs
+fun isar_proof_text ctxt auto isar_proofs
     (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
      isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
      fact_names, lifted, sym_tab, atp_proof, goal)
@@ -426,7 +426,7 @@
       |> (fn fixes =>
              ctxt |> Variable.set_body false
                   |> Proof_Context.add_fixes fixes)
-    val one_line_proof = one_line_proof_text 0 one_line_params
+    val one_line_proof = one_line_proof_text auto 0 one_line_params
     val type_enc =
       if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
       else partial_typesN
@@ -625,7 +625,8 @@
           in
             "\n\nStructured proof"
               ^ (commas msg |> not (null msg) ? enclose " (" ")")
-              ^ ":\n" ^ Active.sendback_markup isar_text
+              ^ ":\n" ^
+              Active.sendback_markup (if auto then [Markup.padding_command] else []) isar_text
           end
       end
     val isar_proof =
@@ -645,12 +646,12 @@
   | Trust_Playable _ => true
   | Failed_to_Play _ => true
 
-fun proof_text ctxt isar_proofs isar_params num_chained
+fun proof_text ctxt auto isar_proofs isar_params num_chained
                (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
       (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
-     isar_proof_text ctxt isar_proofs isar_params
+     isar_proof_text ctxt auto isar_proofs isar_params
    else
-     one_line_proof_text num_chained) one_line_params
+     one_line_proof_text auto num_chained) one_line_params
 
 end;

--- a/src/HOL/Tools/try0.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Tools/try0.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -137,7 +137,7 @@
              Auto_Try => "Auto Try Methods found a proof"
            | Try => "Try Methods found a proof"
            | Normal => "Try this") ^ ": " ^
-          Active.sendback_markup
+          Active.sendback_markup (if mode = Auto_Try then [Markup.padding_command] else [])
               ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
                 else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
           "\n(" ^ space_implode "; " (map time_string xs) ^ ")."

--- a/src/Pure/PIDE/active.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/Pure/PIDE/active.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -9,8 +9,7 @@
   val make_markup: string -> {implicit: bool, properties: Properties.T} -> Markup.T
   val markup_implicit: string -> string -> string
   val markup: string -> string -> string
-  val sendback_markup_implicit: string -> string
-  val sendback_markup: string -> string
+  val sendback_markup: Properties.T -> string -> string
   val dialog: unit -> (string -> Markup.T) * string future
   val dialog_text: unit -> (string -> string) * string future
   val dialog_result: serial -> string -> unit
@@ -34,11 +33,8 @@
 fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
 fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
 
-
-(* sendback area *)
-
-val sendback_markup_implicit = markup_implicit Markup.sendbackN;
-val sendback_markup = markup Markup.sendbackN;
+fun sendback_markup props =
+  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props});
 
 
 (* dialog via document content *)

--- a/src/Pure/PIDE/markup.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -139,6 +139,7 @@
   val sendbackN: string
   val paddingN: string
   val padding_line: Properties.entry
+  val padding_command: Properties.entry
   val dialogN: string val dialog: serial -> string -> T
   val functionN: string
   val assign_update: Properties.T
@@ -451,7 +452,8 @@
 
 val sendbackN = "sendback";
 val paddingN = "padding";
-val padding_line = (paddingN, lineN);
+val padding_line = (paddingN, "line");
+val padding_command = (paddingN, "command");
 
 val dialogN = "dialog";
 fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);

--- a/src/Pure/PIDE/markup.scala	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/Pure/PIDE/markup.scala	Thu Jul 18 20:53:22 2013 +0200
@@ -303,7 +303,8 @@
 
   val SENDBACK = "sendback"
   val PADDING = "padding"
-  val PADDING_LINE = (PADDING, LINE)
+  val PADDING_LINE = (PADDING, "line")
+  val PADDING_COMMAND = (PADDING, "command")
 
   val DIALOG = "dialog"
   val Result = new Properties.String(RESULT)

--- a/src/Tools/jEdit/src/active.scala	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala	Thu Jul 18 20:53:22 2013 +0200
@@ -26,15 +26,27 @@
           val buffer = model.buffer
           val snapshot = model.snapshot()
 
-          def try_replace_command(exec_id: Document_ID.Exec, s: String)
+          def try_replace_command(padding: Boolean, exec_id: Document_ID.Exec, s: String)
           {
             snapshot.state.execs.get(exec_id).map(_.command) match {
               case Some(command) =>
                 snapshot.node.command_start(command) match {
                   case Some(start) =>
                     JEdit_Lib.buffer_edit(buffer) {
-                      buffer.remove(start, command.proper_range.length)
-                      buffer.insert(start, s)
+                      val range = command.proper_range + start
+                      if (padding) {
+                        val pad =
+                          JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
+                            match {
+                              case None => ""
+                              case Some(s) => if (Symbol.is_blank(s)) "" else " "
+                            }
+                        buffer.insert(start + range.length, pad + s)
+                      }
+                      else {
+                        buffer.remove(start, range.length)
+                        buffer.insert(start, s)
+                      }
                     }
                   case None =>
                 }
@@ -70,7 +82,7 @@
               case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
                 props match {
                   case Position.Id(exec_id) =>
-                    try_replace_command(exec_id, text)
+                    try_replace_command(props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
                   case _ =>
                     if (props.exists(_ == Markup.PADDING_LINE))
                       Isabelle.insert_line_padding(text_area, text)