# HG changeset patch # User wenzelm # Date 1374173602 -7200 # Node ID 6fb98a20c34904249bb2b92ed61e62722aa8b32f # Parent 38466f4f348338e461699bb570a31157071b98e8 explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it; diff -r 38466f4f3483 -r 6fb98a20c349 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- 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 diff -r 38466f4f3483 -r 6fb98a20c349 src/HOL/Statespace/StateSpaceEx.thy --- 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))))); *} diff -r 38466f4f3483 -r 6fb98a20c349 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 38466f4f3483 -r 6fb98a20c349 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 38466f4f3483 -r 6fb98a20c349 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- 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 diff -r 38466f4f3483 -r 6fb98a20c349 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 diff -r 38466f4f3483 -r 6fb98a20c349 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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; diff -r 38466f4f3483 -r 6fb98a20c349 src/HOL/Tools/try0.ML --- 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) ^ ")." diff -r 38466f4f3483 -r 6fb98a20c349 src/Pure/PIDE/active.ML --- 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 *) diff -r 38466f4f3483 -r 6fb98a20c349 src/Pure/PIDE/markup.ML --- 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)]); diff -r 38466f4f3483 -r 6fb98a20c349 src/Pure/PIDE/markup.scala --- 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) diff -r 38466f4f3483 -r 6fb98a20c349 src/Tools/jEdit/src/active.scala --- 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)