more abstract Sendback operations, with explicit id/exec_id properties;
authorwenzelm
Thu Nov 22 13:21:02 2012 +0100 (2012-11-22 ago)
changeset 50163c62ce309dc26
parent 50162 e06eabc421e7
child 50164 77668b522ffe
more abstract Sendback operations, with explicit id/exec_id properties;
purge result messages (again), cf. db58490a68ac, 7b61a539721e;
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_reconstruct.ML
src/HOL/Tools/try0.ML
src/Pure/PIDE/command.scala
src/Pure/PIDE/sendback.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Tools/jEdit/src/isabelle_rendering.scala
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Nov 22 12:22:03 2012 +0100
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Nov 22 13:21:02 2012 +0100
     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 -    Markup.markup Isabelle_Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
     1.8 +    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 Nov 22 12:22:03 2012 +0100
     2.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Thu Nov 22 13:21:02 2012 +0100
     2.3 @@ -235,7 +235,7 @@
     2.4  
     2.5  ML {*
     2.6    fun make_benchmark n =
     2.7 -    writeln (Markup.markup Isabelle_Markup.sendback
     2.8 +    writeln (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 Nov 22 12:22:03 2012 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Nov 22 13:21:02 2012 +0100
     3.3 @@ -470,7 +470,7 @@
     3.4                pprint_nt (fn () => Pretty.blk (0,
     3.5                    pstrs "Hint: To check that the induction hypothesis is \
     3.6                          \general enough, try this command: " @
     3.7 -                  [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
     3.8 +                  [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0,
     3.9                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    3.10              else
    3.11                ()
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 22 12:22:03 2012 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Nov 22 13:21:02 2012 +0100
     4.3 @@ -754,8 +754,7 @@
     4.4            (true, "")
     4.5          end)
     4.6  
     4.7 -fun sendback sub =
     4.8 -  Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
     4.9 +fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub)
    4.10  
    4.11  val commit_timeout = seconds 30.0
    4.12  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Nov 22 12:22:03 2012 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Nov 22 13:21:02 2012 +0100
     5.3 @@ -233,15 +233,14 @@
     5.4    command_call (string_for_reconstructor reconstr) ss
     5.5  
     5.6  fun try_command_line banner time command =
     5.7 -  banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^
     5.8 -  show_time time ^ "."
     5.9 +  banner ^ ": " ^ Sendback.markup command ^ show_time time ^ "."
    5.10  
    5.11  fun minimize_line _ [] = ""
    5.12    | minimize_line minimize_command ss =
    5.13      case minimize_command ss of
    5.14        "" => ""
    5.15      | command =>
    5.16 -      "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
    5.17 +      "\nTo minimize: " ^ Sendback.markup command ^ "."
    5.18  
    5.19  fun split_used_facts facts =
    5.20    facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
    5.21 @@ -1055,7 +1054,7 @@
    5.22             else if preplay then
    5.23               " (" ^ string_from_ext_time ext_time ^ ")"
    5.24             else
    5.25 -             "") ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
    5.26 +             "") ^ ":\n" ^ Sendback.markup isar_text
    5.27        end
    5.28      val isar_proof =
    5.29        if debug then
     6.1 --- a/src/HOL/Tools/try0.ML	Thu Nov 22 12:22:03 2012 +0100
     6.2 +++ b/src/HOL/Tools/try0.ML	Thu Nov 22 13:21:02 2012 +0100
     6.3 @@ -138,7 +138,7 @@
     6.4               Auto_Try => "Auto Try Methods found a proof"
     6.5             | Try => "Try Methods found a proof"
     6.6             | Normal => "Try this") ^ ": " ^
     6.7 -          Markup.markup Isabelle_Markup.sendback
     6.8 +          Sendback.markup
     6.9                ((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
    6.10                  else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
    6.11            "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
     7.1 --- a/src/Pure/PIDE/command.scala	Thu Nov 22 12:22:03 2012 +0100
     7.2 +++ b/src/Pure/PIDE/command.scala	Thu Nov 22 13:21:02 2012 +0100
     7.3 @@ -66,14 +66,16 @@
     7.4          case XML.Elem(Markup(name, atts), body) =>
     7.5            atts match {
     7.6              case Isabelle_Markup.Serial(i) =>
     7.7 -              val st0 =
     7.8 -                copy(results =
     7.9 -                  results + (i -> XML.Elem(Markup(Isabelle_Markup.message(name), atts), body)))
    7.10 +              val props = Position.purge(atts)
    7.11 +              val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
    7.12 +              val message2 = XML.Elem(Markup(name, props), body)
    7.13 +
    7.14 +              val st0 = copy(results = results + (i -> message1))
    7.15                val st1 =
    7.16                  if (Protocol.is_tracing(message)) st0
    7.17                  else
    7.18                    (st0 /: Protocol.message_positions(command, message))(
    7.19 -                    (st, range) => st.add_markup(Text.Info(range, message)))
    7.20 +                    (st, range) => st.add_markup(Text.Info(range, message2)))
    7.21  
    7.22                st1
    7.23              case _ => System.err.println("Ignored message without serial number: " + message); this
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/PIDE/sendback.ML	Thu Nov 22 13:21:02 2012 +0100
     8.3 @@ -0,0 +1,28 @@
     8.4 +(*  Title:      Pure/PIDE/sendback.ML
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Clickable "sendback" areas within the source text (see also
     8.8 +Tools/jEdit/src/sendback.scala).
     8.9 +*)
    8.10 +
    8.11 +signature SENDBACK =
    8.12 +sig
    8.13 +  val make_markup: unit -> Markup.T
    8.14 +  val markup: string -> string
    8.15 +end;
    8.16 +
    8.17 +structure Sendback: SENDBACK =
    8.18 +struct
    8.19 +
    8.20 +fun make_markup () =
    8.21 +  let
    8.22 +    val props =
    8.23 +      (case Position.get_id (Position.thread_data ()) of
    8.24 +        SOME id => [(Isabelle_Markup.idN, id)]
    8.25 +      | NONE => []);
    8.26 +  in Markup.properties props Isabelle_Markup.sendback end;
    8.27 +
    8.28 +fun markup s = Markup.markup (make_markup ()) s;
    8.29 +
    8.30 +end;
    8.31 +
     9.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Nov 22 12:22:03 2012 +0100
     9.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Nov 22 13:21:02 2012 +0100
     9.3 @@ -8,7 +8,6 @@
     9.4  signature PROOF_GENERAL =
     9.5  sig
     9.6    val test_markupN: string
     9.7 -  val sendback: string -> Pretty.T list -> unit
     9.8    val init: bool -> unit
     9.9    structure ThyLoad: sig val add_path: string -> unit end
    9.10  end;
    9.11 @@ -113,9 +112,6 @@
    9.12  fun tell_file_retracted path =
    9.13    emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
    9.14  
    9.15 -fun sendback heading prts =
    9.16 -  Pretty.writeln (Pretty.big_list heading [Pretty.markup Isabelle_Markup.sendback prts]);
    9.17 -
    9.18  
    9.19  (* theory loader actions *)
    9.20  
    10.1 --- a/src/Pure/ROOT	Thu Nov 22 12:22:03 2012 +0100
    10.2 +++ b/src/Pure/ROOT	Thu Nov 22 13:21:02 2012 +0100
    10.3 @@ -147,6 +147,7 @@
    10.4      "PIDE/isabelle_markup.ML"
    10.5      "PIDE/markup.ML"
    10.6      "PIDE/protocol.ML"
    10.7 +    "PIDE/sendback.ML"
    10.8      "PIDE/xml.ML"
    10.9      "PIDE/yxml.ML"
   10.10      "Proof/extraction.ML"
    11.1 --- a/src/Pure/ROOT.ML	Thu Nov 22 12:22:03 2012 +0100
    11.2 +++ b/src/Pure/ROOT.ML	Thu Nov 22 13:21:02 2012 +0100
    11.3 @@ -64,6 +64,7 @@
    11.4  
    11.5  use "PIDE/xml.ML";
    11.6  use "PIDE/yxml.ML";
    11.7 +use "PIDE/sendback.ML";
    11.8  
    11.9  use "General/graph.ML";
   11.10  
    12.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Nov 22 12:22:03 2012 +0100
    12.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Nov 22 13:21:02 2012 +0100
    12.3 @@ -246,23 +246,11 @@
    12.4  
    12.5  
    12.6    def sendback(range: Text.Range): Option[Text.Info[Document.Exec_ID]] =
    12.7 -  {
    12.8 -    val results =
    12.9 -      snapshot.cumulate_markup[(Option[Document.Exec_ID], Option[Text.Range])](range,
   12.10 -        (None, None), Some(messages_include + Isabelle_Markup.SENDBACK),
   12.11 -          {
   12.12 -            case ((_, info), Text.Info(_, XML.Elem(Markup(name, Position.Id(id)), _)))
   12.13 -            if messages_include(name) => (Some(id), info)
   12.14 -
   12.15 -            case ((id, _), Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) =>
   12.16 -              (id, Some(snapshot.convert(info_range)))
   12.17 -          })
   12.18 -
   12.19 -    (for (Text.Info(_, (Some(id), Some(r))) <- results) yield Text.Info(r, id)) match {
   12.20 -      case res #:: _ => Some(res)
   12.21 -      case _ => None
   12.22 -    }
   12.23 -  }
   12.24 +    snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)),
   12.25 +        {
   12.26 +          case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, Position.Id(id)), _)) =>
   12.27 +            Text.Info(snapshot.convert(info_range), id)
   12.28 +        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   12.29  
   12.30  
   12.31    def tooltip_message(range: Text.Range): XML.Body =