# HG changeset patch
# User wenzelm
# Date 1468690527 -7200
# Node ID ae8fd6fe63a1539de81e367773bd04e2e479730d
# Parent  8ea738cffabe7e62a3cbafc039b92ce4d36503ea
tuned signature;

diff -r 8ea738cffabe -r ae8fd6fe63a1 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -60,7 +60,7 @@
 fun print_cert cert =
   Output.information
     ("To repeat this proof with a certificate use this command:\n" ^
-      Active.sendback_markup [Markup.padding_command]
+      Active.sendback_markup_command
         ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
 
 fun sos_tac ctxt NONE =
diff -r 8ea738cffabe -r ae8fd6fe63a1 src/HOL/Statespace/StateSpaceEx.thy
--- a/src/HOL/Statespace/StateSpaceEx.thy	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Statespace/StateSpaceEx.thy	Sat Jul 16 19:35:27 2016 +0200
@@ -234,7 +234,7 @@
 
 ML \<open>
   fun make_benchmark n =
-    writeln (Active.sendback_markup [Markup.padding_command]
+    writeln (Active.sendback_markup_command
       ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
         (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
 \<close>
diff -r 8ea738cffabe -r ae8fd6fe63a1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -441,7 +441,7 @@
               in
                 one_line_proof_text ctxt 0 one_line_params ^
                 "\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
-                Active.sendback_markup [Markup.padding_command]
+                Active.sendback_markup_command
                   (string_of_isar_proof ctxt subgoal subgoal_count isar_proof)
               end)
           end
diff -r 8ea738cffabe -r ae8fd6fe63a1 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -1319,7 +1319,7 @@
   else
     ()
 
-fun sendback sub = Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub)
+fun sendback sub = Active.sendback_markup_command (sledgehammerN ^ " " ^ sub)
 
 val commit_timeout = seconds 30.0
 
diff -r 8ea738cffabe -r ae8fd6fe63a1 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -180,7 +180,7 @@
 
 fun try_command_line banner play command =
   let val s = string_of_play_outcome play in
-    banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^
+    banner ^ ": " ^ Active.sendback_markup_command command ^
     (s |> s <> "" ? enclose " (" ")") ^ "."
   end
 
diff -r 8ea738cffabe -r ae8fd6fe63a1 src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/HOL/Tools/try0.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -143,7 +143,7 @@
              Auto_Try => "Auto Try0 found a proof"
            | Try => "Try0 found a proof"
            | Normal => "Try this") ^ ": " ^
-          Active.sendback_markup [Markup.padding_command]
+          Active.sendback_markup_command
               ((if Thm.nprems_of (#goal (Proof.goal st)) = 1 then "by"
                 else "apply") ^ " " ^ command) ^
           (case xs of
diff -r 8ea738cffabe -r ae8fd6fe63a1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -1555,8 +1555,7 @@
       [] => ""
     | proofs =>
         "Proof outline with cases:\n" ^
-        Active.sendback_markup [Markup.padding_command]
-          (space_implode "\nnext\n" proofs ^ "\nqed"))
+        Active.sendback_markup_command (space_implode "\nnext\n" proofs ^ "\nqed"))
   end;
 
 
diff -r 8ea738cffabe -r ae8fd6fe63a1 src/Pure/PIDE/active.ML
--- a/src/Pure/PIDE/active.ML	Sat Jul 16 18:56:43 2016 +0200
+++ b/src/Pure/PIDE/active.ML	Sat Jul 16 19:35:27 2016 +0200
@@ -9,7 +9,8 @@
   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: Properties.T -> string -> string
+  val sendback_markup_properties: Properties.T -> string -> string
+  val sendback_markup_command: string -> string
   val dialog: unit -> (string -> Markup.T) * string future
   val dialog_text: unit -> (string -> string) * string future
   val dialog_result: serial -> string -> unit
@@ -33,8 +34,11 @@
 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;
 
-fun sendback_markup props =
-  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props});
+fun sendback_markup_properties props s =
+  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props}) s;
+
+fun sendback_markup_command s =
+  sendback_markup_properties [Markup.padding_command] s;
 
 
 (* dialog via document content *)