generalized notion of active area, where sendback is just one application;
some support for graphview via active area;
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Mon Dec 10 13:52:33 2012 +0100
@@ -130,7 +130,7 @@
fun output_line cert =
"To repeat this proof with a certifiate use this command:\n" ^
- 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
--- a/src/HOL/Statespace/StateSpaceEx.thy Mon Dec 10 10:41:29 2012 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy Mon Dec 10 13:52:33 2012 +0100
@@ -235,7 +235,7 @@
ML {*
fun make_benchmark n =
- writeln (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)))));
*}
--- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Dec 10 13:52:33 2012 +0100
@@ -470,7 +470,8 @@
pprint_nt (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
\general enough, try this command: " @
- [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
+ [Pretty.mark
+ (Active.make_markup Markup.sendbackN {implicit = false, properties = []})
(Pretty.blk (0,
pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon Dec 10 13:52:33 2012 +0100
@@ -829,7 +829,7 @@
(true, "")
end)
-fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub)
+fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
val commit_timeout = seconds 30.0
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 10 13:52:33 2012 +0100
@@ -220,14 +220,14 @@
command_call (string_for_reconstructor reconstr) ss
fun try_command_line banner time command =
- banner ^ ": " ^ Sendback.markup command ^ show_time time ^ "."
+ banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
"" => ""
| command =>
- "\nTo minimize: " ^ Sendback.markup command ^ "."
+ "\nTo minimize: " ^ Active.sendback_markup command ^ "."
fun split_used_facts facts =
facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
@@ -728,7 +728,7 @@
in
"\n\nStructured proof "
^ (commas msg |> not (null msg) ? enclose "(" ")")
- ^ ":\n" ^ Sendback.markup isar_text
+ ^ ":\n" ^ Active.sendback_markup isar_text
end
end
val isar_proof =
--- a/src/HOL/Tools/try0.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/HOL/Tools/try0.ML Mon Dec 10 13:52:33 2012 +0100
@@ -138,7 +138,7 @@
Auto_Try => "Auto Try Methods found a proof"
| Try => "Try Methods found a proof"
| Normal => "Try this") ^ ": " ^
- Sendback.markup
+ Active.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"
--- a/src/Pure/General/graph_display.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Pure/General/graph_display.ML Mon Dec 10 13:52:33 2012 +0100
@@ -57,9 +57,11 @@
fun display_graph graph =
if print_mode_active graphview_reportN then
- (Output.report
- (YXML.string_of (XML.Elem ((Markup.graphviewN, []), encode_graphview graph)));
- writeln "(see graphview)")
+ let
+ val markup = Active.make_markup Markup.graphviewN {implicit = false, properties = []};
+ val ((bg1, bg2), en) = YXML.output_markup_elem markup;
+ val graph_yxml = YXML.string_of_body (encode_graphview graph);
+ in writeln ("See " ^ bg1 ^ graph_yxml ^ bg2 ^ "graphview" ^ en) end
else
let
val browser =
--- a/src/Pure/Isar/outer_syntax.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Mon Dec 10 13:52:33 2012 +0100
@@ -66,7 +66,7 @@
fun pretty_command (cmd as (name, Command {comment, ...})) =
Pretty.block
(Pretty.marks_str
- ([Sendback.make_markup {implicit = true, properties = [Markup.padding_line]},
+ ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/active.ML Mon Dec 10 13:52:33 2012 +0100
@@ -0,0 +1,37 @@
+(* Title: Pure/PIDE/active.ML
+ Author: Makarius
+
+Active areas within the document (see also Tools/jEdit/src/active.scala).
+*)
+
+signature ACTIVE =
+sig
+ 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
+end;
+
+structure Active: ACTIVE =
+struct
+
+fun make_markup name {implicit, properties} =
+ (name, [])
+ |> not implicit ? (fn markup =>
+ let
+ val props =
+ (case Position.get_id (Position.thread_data ()) of
+ SOME id => [(Markup.idN, id)]
+ | NONE => []);
+ in Markup.properties props markup end)
+ |> Markup.properties properties;
+
+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;
+
+val sendback_markup_implicit = markup_implicit Markup.sendbackN;
+val sendback_markup = markup Markup.sendbackN;
+
+end;
+
--- a/src/Pure/PIDE/markup.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Mon Dec 10 13:52:33 2012 +0100
@@ -98,7 +98,8 @@
val subgoalN: string val subgoal: T
val paddingN: string
val padding_line: string * string
- val sendbackN: string val sendback: T
+ val sendbackN: string
+ val graphviewN: string
val intensifyN: string val intensify: T
val taskN: string
val acceptedN: string val accepted: T
@@ -120,7 +121,6 @@
val reportN: string val report: T
val no_reportN: string val no_report: T
val badN: string val bad: T
- val graphviewN: string
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
@@ -337,9 +337,14 @@
val (stateN, state) = markup_elem "state";
val (subgoalN, subgoal) = markup_elem "subgoal";
+
+(* active areads *)
+
+val sendbackN = "sendback";
+val graphviewN = "graphview";
+
val paddingN = "padding";
val padding_line = (paddingN, lineN);
-val (sendbackN, sendback) = markup_elem "sendback";
val (intensifyN, intensify) = markup_elem "intensify";
@@ -376,8 +381,6 @@
val (badN, bad) = markup_elem "bad";
-val graphviewN = "graphview";
-
(* protocol message functions *)
--- a/src/Pure/PIDE/markup.scala Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Mon Dec 10 13:52:33 2012 +0100
@@ -212,9 +212,14 @@
val STATE = "state"
val SUBGOAL = "subgoal"
+
+ /* active areas */
+
+ val SENDBACK = "sendback"
+ val GRAPHVIEW = "graphview"
+
val PADDING = "padding"
val PADDING_LINE = (PADDING, LINE)
- val SENDBACK = "sendback"
val INTENSIFY = "intensify"
@@ -280,8 +285,6 @@
val BAD = "bad"
- val GRAPHVIEW = "graphview"
-
/* protocol message functions */
--- a/src/Pure/PIDE/protocol.scala Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Dec 10 13:52:33 2012 +0100
@@ -118,10 +118,12 @@
/* result messages */
+ private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
+
def clean_message(body: XML.Body): XML.Body =
body filter {
- case XML.Elem(Markup(Markup.REPORT, _), _) => false
- case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false
+ case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name)
+ case XML.Elem(Markup(name, _), _) => !clean(name)
case _ => true
} map {
case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
@@ -131,6 +133,8 @@
def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
body flatMap {
+ case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
+ List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
--- a/src/Pure/PIDE/sendback.ML Mon Dec 10 10:41:29 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* 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: {implicit: bool, properties: Properties.T} -> Markup.T
- val markup_implicit: string -> string
- val markup: string -> string
-end;
-
-structure Sendback: SENDBACK =
-struct
-
-fun make_markup {implicit, properties} =
- Markup.sendback
- |> not implicit ? (fn markup =>
- let
- val props =
- (case Position.get_id (Position.thread_data ()) of
- SOME id => [(Markup.idN, id)]
- | NONE => []);
- in Markup.properties props markup end)
- |> Markup.properties properties;
-
-fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
-fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
-
-end;
-
--- a/src/Pure/ROOT Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Pure/ROOT Mon Dec 10 13:52:33 2012 +0100
@@ -144,11 +144,11 @@
"ML/ml_statistics_polyml-5.5.0.ML"
"ML/ml_syntax.ML"
"ML/ml_thms.ML"
+ "PIDE/active.ML"
"PIDE/command.ML"
"PIDE/document.ML"
"PIDE/markup.ML"
"PIDE/protocol.ML"
- "PIDE/sendback.ML"
"PIDE/xml.ML"
"PIDE/yxml.ML"
"Proof/extraction.ML"
--- a/src/Pure/ROOT.ML Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Pure/ROOT.ML Mon Dec 10 13:52:33 2012 +0100
@@ -63,7 +63,7 @@
use "PIDE/xml.ML";
use "PIDE/yxml.ML";
-use "PIDE/sendback.ML";
+use "PIDE/active.ML";
use "General/graph.ML";
--- a/src/Tools/jEdit/etc/options Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Tools/jEdit/etc/options Mon Dec 10 13:52:33 2012 +0100
@@ -41,8 +41,8 @@
option quoted_color : string = "8B8B8B19"
option highlight_color : string = "50505032"
option hyperlink_color : string = "000000FF"
-option sendback_color : string = "DCDCDCFF"
-option sendback_active_color : string = "9DC75DFF"
+option active_color : string = "DCDCDCFF"
+option active_hover_color : string = "9DC75DFF"
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"
--- a/src/Tools/jEdit/lib/Tools/jedit Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Mon Dec 10 13:52:33 2012 +0100
@@ -8,6 +8,7 @@
## sources
declare -a SOURCES=(
+ "src/active.scala"
"src/dockable.scala"
"src/document_model.scala"
"src/document_view.scala"
@@ -35,7 +36,6 @@
"src/rendering.scala"
"src/rich_text_area.scala"
"src/scala_console.scala"
- "src/sendback.scala"
"src/symbols_dockable.scala"
"src/syslog_dockable.scala"
"src/text_overview.scala"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/active.scala Mon Dec 10 13:52:33 2012 +0100
@@ -0,0 +1,63 @@
+/* Title: Tools/jEdit/src/active.scala
+ Author: Makarius
+
+Active areas within the document.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.View
+
+
+object Active
+{
+ def action(view: View, text: String, elem: XML.Elem)
+ {
+ Swing_Thread.require()
+
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ doc_view.rich_text_area.robust_body() {
+ val text_area = doc_view.text_area
+ val model = doc_view.model
+ val buffer = model.buffer
+ val snapshot = model.snapshot()
+
+ if (!snapshot.is_outdated) {
+ elem match {
+ case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
+ props match {
+ case Position.Id(exec_id) =>
+ 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, text)
+ }
+ case None =>
+ }
+ case None =>
+ }
+ case _ =>
+ if (props.exists(_ == Markup.PADDING_LINE))
+ Isabelle.insert_line_padding(text_area, text)
+ else text_area.setSelectedText(text)
+ }
+
+ case XML.Elem(Markup(Markup.GRAPHVIEW, props), body) =>
+ java.lang.System.err.println("graphview " + props) // FIXME
+
+ case _ =>
+ }
+ }
+ }
+ case None =>
+ }
+ }
+}
+
--- a/src/Tools/jEdit/src/rendering.scala Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Mon Dec 10 13:52:33 2012 +0100
@@ -135,8 +135,8 @@
val quoted_color = color_value("quoted_color")
val highlight_color = color_value("highlight_color")
val hyperlink_color = color_value("hyperlink_color")
- val sendback_color = color_value("sendback_color")
- val sendback_active_color = color_value("sendback_active_color")
+ val active_color = color_value("active_color")
+ val active_hover_color = color_value("active_hover_color")
val keyword1_color = color_value("keyword1_color")
val keyword2_color = color_value("keyword2_color")
@@ -249,11 +249,13 @@
}
- def sendback(range: Text.Range): Option[Text.Info[Properties.T]] =
- snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
+ private val active_include = Set(Markup.SENDBACK, Markup.GRAPHVIEW)
+
+ def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
+ snapshot.select_markup(range, Some(active_include),
{
- case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
- Text.Info(snapshot.convert(info_range), props)
+ case Text.Info(info_range, elem @ XML.Elem(markup, _))
+ if active_include(markup.name) => Text.Info(snapshot.convert(info_range), elem)
}) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
@@ -405,8 +407,8 @@
private val background1_include =
Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
- Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
- Markup.SENDBACK
+ Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
+ active_include
def background1(range: Text.Range): Stream[Text.Info[Color]] =
{
@@ -424,8 +426,8 @@
(None, Some(bad_color))
case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
(None, Some(intensify_color))
- case (_, Text.Info(_, XML.Elem(Markup(Markup.SENDBACK, _), _))) =>
- (None, Some(sendback_color))
+ case (_, Text.Info(_, XML.Elem(Markup(name, _), _))) if active_include(name) =>
+ (None, Some(active_color))
})
color <-
(result match {
--- a/src/Tools/jEdit/src/rich_text_area.scala Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Mon Dec 10 13:52:33 2012 +0100
@@ -135,10 +135,10 @@
private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
- private val sendback_area = new Active_Area[Properties.T]((r: Rendering) => r.sendback _)
+ private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
private val active_areas =
- List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
+ List((highlight_area, true), (hyperlink_area, true), (active_area, false))
def active_reset(): Unit = active_areas.foreach(_._1.reset)
private val focus_listener = new FocusAdapter {
@@ -157,8 +157,8 @@
case Some(Text.Info(_, link)) => link.follow(view)
case None =>
}
- sendback_area.text_info match {
- case Some((text, Text.Info(_, props))) => Sendback.activate(view, text, props)
+ active_area.text_info match {
+ case Some((text, Text.Info(_, markup))) => Active.action(view, text, markup)
case None =>
}
}
@@ -252,13 +252,13 @@
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
- // sendback range -- potentially from other snapshot
+ // active area -- potentially from other snapshot
for {
- info <- sendback_area.info
+ info <- active_area.info
Text.Info(range, _) <- info.try_restrict(line_range)
r <- JEdit_Lib.gfx_range(text_area, range)
} {
- gfx.setColor(rendering.sendback_active_color)
+ gfx.setColor(rendering.active_hover_color)
gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
}
--- a/src/Tools/jEdit/src/sendback.scala Mon Dec 10 10:41:29 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-/* Title: Tools/jEdit/src/sendback.scala
- Author: Makarius
-
-Clickable "sendback" areas within the source text.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.View
-
-
-object Sendback
-{
- def activate(view: View, text: String, props: Properties.T)
- {
- Swing_Thread.require()
-
- Document_View(view.getTextArea) match {
- case Some(doc_view) =>
- doc_view.rich_text_area.robust_body() {
- val text_area = doc_view.text_area
- val model = doc_view.model
- val buffer = model.buffer
- val snapshot = model.snapshot()
-
- if (!snapshot.is_outdated) {
- props match {
- case Position.Id(exec_id) =>
- 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, text)
- }
- case None =>
- }
- case None =>
- }
- case _ =>
- if (props.exists(_ == Markup.PADDING_LINE))
- Isabelle.insert_line_padding(text_area, text)
- else text_area.setSelectedText(text)
- }
- }
- }
- case None =>
- }
- }
-}
-