# HG changeset patch # User wenzelm # Date 1355143953 -3600 # Node ID 358b6020f8b69b1b717d6060a4a06f170b8c4e0a # Parent 2e22cdccdc38b5e4e79bd9501ef293f634e0398c generalized notion of active area, where sendback is just one application; some support for graphview via active area; diff -r 2e22cdccdc38 -r 358b6020f8b6 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- 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 diff -r 2e22cdccdc38 -r 358b6020f8b6 src/HOL/Statespace/StateSpaceEx.thy --- 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))))); *} diff -r 2e22cdccdc38 -r 358b6020f8b6 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 2e22cdccdc38 -r 358b6020f8b6 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 2e22cdccdc38 -r 358b6020f8b6 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 = diff -r 2e22cdccdc38 -r 358b6020f8b6 src/HOL/Tools/try0.ML --- 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" diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/General/graph_display.ML --- 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 = diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/Isar/outer_syntax.ML --- 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); diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/PIDE/active.ML --- /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; + diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/PIDE/markup.ML --- 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 *) diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/PIDE/markup.scala --- 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 */ diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/PIDE/protocol.scala --- 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) diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/PIDE/sendback.ML --- 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; - diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/ROOT --- 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" diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Pure/ROOT.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"; diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Tools/jEdit/etc/options --- 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" diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Tools/jEdit/src/active.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 => + } + } +} + diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Tools/jEdit/src/rendering.scala --- 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 { diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Tools/jEdit/src/rich_text_area.scala --- 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) } diff -r 2e22cdccdc38 -r 358b6020f8b6 src/Tools/jEdit/src/sendback.scala --- 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 => - } - } -} -