explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
authorwenzelm
Thu Jul 18 20:53:22 2013 +0200 (2013-07-18 ago)
changeset 526976fb98a20c349
parent 52696 38466f4f3483
child 52698 df1531af559f
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
src/HOL/Statespace/StateSpaceEx.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/try0.ML
src/Pure/PIDE/active.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/active.scala
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Jul 18 13:12:54 2013 +0200
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Jul 18 20:53:22 2013 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  fun output_line cert =
     1.6    "To repeat this proof with a certifiate use this command:\n" ^
     1.7 -    Active.sendback_markup ("by (sos_cert \"" ^ cert ^ "\")")
     1.8 +    Active.sendback_markup [] ("by (sos_cert \"" ^ cert ^ "\")")
     1.9  
    1.10  val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
    1.11  
     2.1 --- a/src/HOL/Statespace/StateSpaceEx.thy	Thu Jul 18 13:12:54 2013 +0200
     2.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Jul 18 20:53:22 2013 +0200
     2.3 @@ -235,7 +235,7 @@
     2.4  
     2.5  ML {*
     2.6    fun make_benchmark n =
     2.7 -    writeln (Active.sendback_markup
     2.8 +    writeln (Active.sendback_markup []
     2.9        ("statespace benchmark" ^ string_of_int n ^ " =\n" ^
    2.10          (cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
    2.11  *}
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jul 18 13:12:54 2013 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jul 18 20:53:22 2013 +0200
     3.3 @@ -466,7 +466,8 @@
     3.4                    pstrs "Hint: To check that the induction hypothesis is \
     3.5                          \general enough, try this command: " @
     3.6                    [Pretty.mark
     3.7 -                    (Active.make_markup Markup.sendbackN {implicit = false, properties = []})
     3.8 +                    (Active.make_markup Markup.sendbackN
     3.9 +                      {implicit = false, properties = [Markup.padding_command]})
    3.10                      (Pretty.blk (0,
    3.11                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    3.12              else
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 18 13:12:54 2013 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 18 20:53:22 2013 +0200
     4.3 @@ -955,7 +955,8 @@
     4.4        |> drop (length old_facts)
     4.5      end
     4.6  
     4.7 -fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
     4.8 +fun sendback sub =
     4.9 +  Active.sendback_markup [Markup.padding_command] (sledgehammerN ^ " " ^ sub)
    4.10  
    4.11  val commit_timeout = seconds 30.0
    4.12  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 18 13:12:54 2013 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Jul 18 20:53:22 2013 +0200
     5.3 @@ -13,7 +13,7 @@
     5.4  
     5.5    val string_of_reconstructor : reconstructor -> string
     5.6  
     5.7 -  val one_line_proof_text : int -> one_line_params -> string
     5.8 +  val one_line_proof_text : bool -> int -> one_line_params -> string
     5.9  
    5.10    val string_of_proof :
    5.11      Proof.context -> string -> string -> int -> int -> isar_proof -> string
    5.12 @@ -71,21 +71,24 @@
    5.13    using_labels ls ^ apply_on_subgoal i n ^
    5.14    command_call (string_of_reconstructor reconstr) ss
    5.15  
    5.16 -fun try_command_line banner time command =
    5.17 -  banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
    5.18 +fun try_command_line auto banner time command =
    5.19 +  banner ^ ": " ^
    5.20 +  Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^
    5.21 +  show_time time ^ "."
    5.22  
    5.23 -fun minimize_line _ [] = ""
    5.24 -  | minimize_line minimize_command ss =
    5.25 +fun minimize_line _ _ [] = ""
    5.26 +  | minimize_line auto minimize_command ss =
    5.27      case minimize_command ss of
    5.28        "" => ""
    5.29      | command =>
    5.30 -      "\nTo minimize: " ^ Active.sendback_markup command ^ "."
    5.31 +      "\nTo minimize: " ^
    5.32 +      Active.sendback_markup (if auto then [Markup.padding_command] else []) command ^ "."
    5.33  
    5.34  fun split_used_facts facts =
    5.35    facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
    5.36          |> pairself (sort_distinct (string_ord o pairself fst))
    5.37  
    5.38 -fun one_line_proof_text num_chained
    5.39 +fun one_line_proof_text auto num_chained
    5.40          (preplay, banner, used_facts, minimize_command, subgoal,
    5.41           subgoal_count) =
    5.42    let
    5.43 @@ -109,8 +112,8 @@
    5.44                       ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
    5.45                       \solve this.)"
    5.46            else
    5.47 -            try_command_line banner ext_time)
    5.48 -  in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
    5.49 +            try_command_line auto banner ext_time)
    5.50 +  in try_line ^ minimize_line auto minimize_command (map fst (extra @ chained)) end
    5.51  
    5.52  
    5.53  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 18 13:12:54 2013 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 18 20:53:22 2013 +0200
     6.3 @@ -973,7 +973,7 @@
     6.4                     subgoal, subgoal_count)
     6.5                  val num_chained = length (#facts (Proof.goal state))
     6.6                in
     6.7 -                proof_text ctxt isar_proofs isar_params num_chained
     6.8 +                proof_text ctxt (mode = Auto_Try) isar_proofs isar_params num_chained
     6.9                             one_line_params
    6.10                end,
    6.11             (if verbose then
    6.12 @@ -1177,7 +1177,7 @@
    6.13                                           preplay,
    6.14                   subgoal, subgoal_count)
    6.15                val num_chained = length (#facts (Proof.goal state))
    6.16 -            in one_line_proof_text num_chained one_line_params end,
    6.17 +            in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
    6.18           if verbose then
    6.19             "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "."
    6.20           else
    6.21 @@ -1222,7 +1222,7 @@
    6.22                   minimize_command override_params name, subgoal,
    6.23                   subgoal_count)
    6.24                val num_chained = length (#facts (Proof.goal state))
    6.25 -            in one_line_proof_text num_chained one_line_params end,
    6.26 +            in one_line_proof_text (mode = Auto_Try) num_chained one_line_params end,
    6.27         message_tail = ""}
    6.28      | play =>
    6.29        let
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jul 18 13:12:54 2013 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jul 18 20:53:22 2013 +0200
     7.3 @@ -25,9 +25,9 @@
     7.4      Proof.context -> (string * stature) list vector -> 'a proof ->
     7.5      string list option
     7.6    val isar_proof_text :
     7.7 -    Proof.context -> bool option -> isar_params -> one_line_params -> string
     7.8 +    Proof.context -> bool -> bool option -> isar_params -> one_line_params -> string
     7.9    val proof_text :
    7.10 -    Proof.context -> bool option -> isar_params -> int -> one_line_params
    7.11 +    Proof.context -> bool -> bool option -> isar_params -> int -> one_line_params
    7.12      -> string
    7.13  end;
    7.14  
    7.15 @@ -413,7 +413,7 @@
    7.16    * string Symtab.table * (string * stature) list vector
    7.17    * (string * term) list * int Symtab.table * string proof * thm
    7.18  
    7.19 -fun isar_proof_text ctxt isar_proofs
    7.20 +fun isar_proof_text ctxt auto isar_proofs
    7.21      (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
    7.22       isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
    7.23       fact_names, lifted, sym_tab, atp_proof, goal)
    7.24 @@ -426,7 +426,7 @@
    7.25        |> (fn fixes =>
    7.26               ctxt |> Variable.set_body false
    7.27                    |> Proof_Context.add_fixes fixes)
    7.28 -    val one_line_proof = one_line_proof_text 0 one_line_params
    7.29 +    val one_line_proof = one_line_proof_text auto 0 one_line_params
    7.30      val type_enc =
    7.31        if is_typed_helper_used_in_atp_proof atp_proof then full_typesN
    7.32        else partial_typesN
    7.33 @@ -625,7 +625,8 @@
    7.34            in
    7.35              "\n\nStructured proof"
    7.36                ^ (commas msg |> not (null msg) ? enclose " (" ")")
    7.37 -              ^ ":\n" ^ Active.sendback_markup isar_text
    7.38 +              ^ ":\n" ^
    7.39 +              Active.sendback_markup (if auto then [Markup.padding_command] else []) isar_text
    7.40            end
    7.41        end
    7.42      val isar_proof =
    7.43 @@ -645,12 +646,12 @@
    7.44    | Trust_Playable _ => true
    7.45    | Failed_to_Play _ => true
    7.46  
    7.47 -fun proof_text ctxt isar_proofs isar_params num_chained
    7.48 +fun proof_text ctxt auto isar_proofs isar_params num_chained
    7.49                 (one_line_params as (preplay, _, _, _, _, _)) =
    7.50    (if isar_proofs = SOME true orelse
    7.51        (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
    7.52 -     isar_proof_text ctxt isar_proofs isar_params
    7.53 +     isar_proof_text ctxt auto isar_proofs isar_params
    7.54     else
    7.55 -     one_line_proof_text num_chained) one_line_params
    7.56 +     one_line_proof_text auto num_chained) one_line_params
    7.57  
    7.58  end;
     8.1 --- a/src/HOL/Tools/try0.ML	Thu Jul 18 13:12:54 2013 +0200
     8.2 +++ b/src/HOL/Tools/try0.ML	Thu Jul 18 20:53:22 2013 +0200
     8.3 @@ -137,7 +137,7 @@
     8.4               Auto_Try => "Auto Try Methods found a proof"
     8.5             | Try => "Try Methods found a proof"
     8.6             | Normal => "Try this") ^ ": " ^
     8.7 -          Active.sendback_markup
     8.8 +          Active.sendback_markup (if mode = Auto_Try then [Markup.padding_command] else [])
     8.9                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
    8.10                  else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
    8.11            "\n(" ^ space_implode "; " (map time_string xs) ^ ")."
     9.1 --- a/src/Pure/PIDE/active.ML	Thu Jul 18 13:12:54 2013 +0200
     9.2 +++ b/src/Pure/PIDE/active.ML	Thu Jul 18 20:53:22 2013 +0200
     9.3 @@ -9,8 +9,7 @@
     9.4    val make_markup: string -> {implicit: bool, properties: Properties.T} -> Markup.T
     9.5    val markup_implicit: string -> string -> string
     9.6    val markup: string -> string -> string
     9.7 -  val sendback_markup_implicit: string -> string
     9.8 -  val sendback_markup: string -> string
     9.9 +  val sendback_markup: Properties.T -> string -> string
    9.10    val dialog: unit -> (string -> Markup.T) * string future
    9.11    val dialog_text: unit -> (string -> string) * string future
    9.12    val dialog_result: serial -> string -> unit
    9.13 @@ -34,11 +33,8 @@
    9.14  fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
    9.15  fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
    9.16  
    9.17 -
    9.18 -(* sendback area *)
    9.19 -
    9.20 -val sendback_markup_implicit = markup_implicit Markup.sendbackN;
    9.21 -val sendback_markup = markup Markup.sendbackN;
    9.22 +fun sendback_markup props =
    9.23 +  Markup.markup (make_markup Markup.sendbackN {implicit = false, properties = props});
    9.24  
    9.25  
    9.26  (* dialog via document content *)
    10.1 --- a/src/Pure/PIDE/markup.ML	Thu Jul 18 13:12:54 2013 +0200
    10.2 +++ b/src/Pure/PIDE/markup.ML	Thu Jul 18 20:53:22 2013 +0200
    10.3 @@ -139,6 +139,7 @@
    10.4    val sendbackN: string
    10.5    val paddingN: string
    10.6    val padding_line: Properties.entry
    10.7 +  val padding_command: Properties.entry
    10.8    val dialogN: string val dialog: serial -> string -> T
    10.9    val functionN: string
   10.10    val assign_update: Properties.T
   10.11 @@ -451,7 +452,8 @@
   10.12  
   10.13  val sendbackN = "sendback";
   10.14  val paddingN = "padding";
   10.15 -val padding_line = (paddingN, lineN);
   10.16 +val padding_line = (paddingN, "line");
   10.17 +val padding_command = (paddingN, "command");
   10.18  
   10.19  val dialogN = "dialog";
   10.20  fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
    11.1 --- a/src/Pure/PIDE/markup.scala	Thu Jul 18 13:12:54 2013 +0200
    11.2 +++ b/src/Pure/PIDE/markup.scala	Thu Jul 18 20:53:22 2013 +0200
    11.3 @@ -303,7 +303,8 @@
    11.4  
    11.5    val SENDBACK = "sendback"
    11.6    val PADDING = "padding"
    11.7 -  val PADDING_LINE = (PADDING, LINE)
    11.8 +  val PADDING_LINE = (PADDING, "line")
    11.9 +  val PADDING_COMMAND = (PADDING, "command")
   11.10  
   11.11    val DIALOG = "dialog"
   11.12    val Result = new Properties.String(RESULT)
    12.1 --- a/src/Tools/jEdit/src/active.scala	Thu Jul 18 13:12:54 2013 +0200
    12.2 +++ b/src/Tools/jEdit/src/active.scala	Thu Jul 18 20:53:22 2013 +0200
    12.3 @@ -26,15 +26,27 @@
    12.4            val buffer = model.buffer
    12.5            val snapshot = model.snapshot()
    12.6  
    12.7 -          def try_replace_command(exec_id: Document_ID.Exec, s: String)
    12.8 +          def try_replace_command(padding: Boolean, exec_id: Document_ID.Exec, s: String)
    12.9            {
   12.10              snapshot.state.execs.get(exec_id).map(_.command) match {
   12.11                case Some(command) =>
   12.12                  snapshot.node.command_start(command) match {
   12.13                    case Some(start) =>
   12.14                      JEdit_Lib.buffer_edit(buffer) {
   12.15 -                      buffer.remove(start, command.proper_range.length)
   12.16 -                      buffer.insert(start, s)
   12.17 +                      val range = command.proper_range + start
   12.18 +                      if (padding) {
   12.19 +                        val pad =
   12.20 +                          JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
   12.21 +                            match {
   12.22 +                              case None => ""
   12.23 +                              case Some(s) => if (Symbol.is_blank(s)) "" else " "
   12.24 +                            }
   12.25 +                        buffer.insert(start + range.length, pad + s)
   12.26 +                      }
   12.27 +                      else {
   12.28 +                        buffer.remove(start, range.length)
   12.29 +                        buffer.insert(start, s)
   12.30 +                      }
   12.31                      }
   12.32                    case None =>
   12.33                  }
   12.34 @@ -70,7 +82,7 @@
   12.35                case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
   12.36                  props match {
   12.37                    case Position.Id(exec_id) =>
   12.38 -                    try_replace_command(exec_id, text)
   12.39 +                    try_replace_command(props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
   12.40                    case _ =>
   12.41                      if (props.exists(_ == Markup.PADDING_LINE))
   12.42                        Isabelle.insert_line_padding(text_area, text)