# HG changeset patch # User wenzelm # Date 1353586862 -3600 # Node ID c62ce309dc268ead549db668519b32b0548bae16 # Parent e06eabc421e7ee248bb138836b3e309c1af38fb3 more abstract Sendback operations, with explicit id/exec_id properties; purge result messages (again), cf. db58490a68ac, 7b61a539721e; diff -r e06eabc421e7 -r c62ce309dc26 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Thu Nov 22 13:21:02 2012 +0100 @@ -130,7 +130,7 @@ fun output_line cert = "To repeat this proof with a certifiate use this command:\n" ^ - Markup.markup Isabelle_Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")") + Sendback.markup ("by (sos_cert \"" ^ cert ^ "\")") val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert diff -r e06eabc421e7 -r c62ce309dc26 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Thu Nov 22 12:22:03 2012 +0100 +++ b/src/HOL/Statespace/StateSpaceEx.thy Thu Nov 22 13:21:02 2012 +0100 @@ -235,7 +235,7 @@ ML {* fun make_benchmark n = - writeln (Markup.markup Isabelle_Markup.sendback + writeln (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 e06eabc421e7 -r c62ce309dc26 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 22 13:21:02 2012 +0100 @@ -470,7 +470,7 @@ pprint_nt (fn () => Pretty.blk (0, pstrs "Hint: To check that the induction hypothesis is \ \general enough, try this command: " @ - [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0, + [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0, pstrs ("nitpick [non_std, show_all]")))] @ pstrs ".")) else () diff -r e06eabc421e7 -r c62ce309dc26 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 22 13:21:02 2012 +0100 @@ -754,8 +754,7 @@ (true, "") end) -fun sendback sub = - Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub) +fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub) val commit_timeout = seconds 30.0 diff -r e06eabc421e7 -r c62ce309dc26 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Nov 22 13:21:02 2012 +0100 @@ -233,15 +233,14 @@ command_call (string_for_reconstructor reconstr) ss fun try_command_line banner time command = - banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ - show_time time ^ "." + banner ^ ": " ^ Sendback.markup command ^ show_time time ^ "." fun minimize_line _ [] = "" | minimize_line minimize_command ss = case minimize_command ss of "" => "" | command => - "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "." + "\nTo minimize: " ^ Sendback.markup command ^ "." fun split_used_facts facts = facts |> List.partition (fn (_, (sc, _)) => sc = Chained) @@ -1055,7 +1054,7 @@ else if preplay then " (" ^ string_from_ext_time ext_time ^ ")" else - "") ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text + "") ^ ":\n" ^ Sendback.markup isar_text end val isar_proof = if debug then diff -r e06eabc421e7 -r c62ce309dc26 src/HOL/Tools/try0.ML --- a/src/HOL/Tools/try0.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/HOL/Tools/try0.ML Thu Nov 22 13:21:02 2012 +0100 @@ -138,7 +138,7 @@ Auto_Try => "Auto Try Methods found a proof" | Try => "Try Methods found a proof" | Normal => "Try this") ^ ": " ^ - Markup.markup Isabelle_Markup.sendback + Sendback.markup ((if nprems_of (#goal (Proof.goal st)) = 1 then "by" else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^ "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n" diff -r e06eabc421e7 -r c62ce309dc26 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Thu Nov 22 12:22:03 2012 +0100 +++ b/src/Pure/PIDE/command.scala Thu Nov 22 13:21:02 2012 +0100 @@ -66,14 +66,16 @@ case XML.Elem(Markup(name, atts), body) => atts match { case Isabelle_Markup.Serial(i) => - val st0 = - copy(results = - results + (i -> XML.Elem(Markup(Isabelle_Markup.message(name), atts), body))) + val props = Position.purge(atts) + val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), props), body) + val message2 = XML.Elem(Markup(name, props), body) + + val st0 = copy(results = results + (i -> message1)) val st1 = if (Protocol.is_tracing(message)) st0 else (st0 /: Protocol.message_positions(command, message))( - (st, range) => st.add_markup(Text.Info(range, message))) + (st, range) => st.add_markup(Text.Info(range, message2))) st1 case _ => System.err.println("Ignored message without serial number: " + message); this diff -r e06eabc421e7 -r c62ce309dc26 src/Pure/PIDE/sendback.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/sendback.ML Thu Nov 22 13:21:02 2012 +0100 @@ -0,0 +1,28 @@ +(* Title: Pure/PIDE/sendback.ML + Author: Makarius + +Clickable "sendback" areas within the source text (see also +Tools/jEdit/src/sendback.scala). +*) + +signature SENDBACK = +sig + val make_markup: unit -> Markup.T + val markup: string -> string +end; + +structure Sendback: SENDBACK = +struct + +fun make_markup () = + let + val props = + (case Position.get_id (Position.thread_data ()) of + SOME id => [(Isabelle_Markup.idN, id)] + | NONE => []); + in Markup.properties props Isabelle_Markup.sendback end; + +fun markup s = Markup.markup (make_markup ()) s; + +end; + diff -r e06eabc421e7 -r c62ce309dc26 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Nov 22 13:21:02 2012 +0100 @@ -8,7 +8,6 @@ signature PROOF_GENERAL = sig val test_markupN: string - val sendback: string -> Pretty.T list -> unit val init: bool -> unit structure ThyLoad: sig val add_path: string -> unit end end; @@ -113,9 +112,6 @@ fun tell_file_retracted path = emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path)); -fun sendback heading prts = - Pretty.writeln (Pretty.big_list heading [Pretty.markup Isabelle_Markup.sendback prts]); - (* theory loader actions *) diff -r e06eabc421e7 -r c62ce309dc26 src/Pure/ROOT --- a/src/Pure/ROOT Thu Nov 22 12:22:03 2012 +0100 +++ b/src/Pure/ROOT Thu Nov 22 13:21:02 2012 +0100 @@ -147,6 +147,7 @@ "PIDE/isabelle_markup.ML" "PIDE/markup.ML" "PIDE/protocol.ML" + "PIDE/sendback.ML" "PIDE/xml.ML" "PIDE/yxml.ML" "Proof/extraction.ML" diff -r e06eabc421e7 -r c62ce309dc26 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Nov 22 12:22:03 2012 +0100 +++ b/src/Pure/ROOT.ML Thu Nov 22 13:21:02 2012 +0100 @@ -64,6 +64,7 @@ use "PIDE/xml.ML"; use "PIDE/yxml.ML"; +use "PIDE/sendback.ML"; use "General/graph.ML"; diff -r e06eabc421e7 -r c62ce309dc26 src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Nov 22 12:22:03 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Thu Nov 22 13:21:02 2012 +0100 @@ -246,23 +246,11 @@ def sendback(range: Text.Range): Option[Text.Info[Document.Exec_ID]] = - { - val results = - snapshot.cumulate_markup[(Option[Document.Exec_ID], Option[Text.Range])](range, - (None, None), Some(messages_include + Isabelle_Markup.SENDBACK), - { - case ((_, info), Text.Info(_, XML.Elem(Markup(name, Position.Id(id)), _))) - if messages_include(name) => (Some(id), info) - - case ((id, _), Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) => - (id, Some(snapshot.convert(info_range))) - }) - - (for (Text.Info(_, (Some(id), Some(r))) <- results) yield Text.Info(r, id)) match { - case res #:: _ => Some(res) - case _ => None - } - } + snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)), + { + case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, Position.Id(id)), _)) => + Text.Info(snapshot.convert(info_range), id) + }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None } def tooltip_message(range: Text.Range): XML.Body =