generalized notion of active area, where sendback is just one application;
authorwenzelm
Mon Dec 10 13:52:33 2012 +0100 (2012-12-10 ago)
changeset 50450358b6020f8b6
parent 50447 2e22cdccdc38
child 50451 2af559170d07
generalized notion of active area, where sendback is just one application;
some support for graphview via active area;
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/General/graph_display.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/active.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/sendback.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Tools/jEdit/etc/options
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
src/Tools/jEdit/src/sendback.scala
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Dec 10 10:41:29 2012 +0100
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Dec 10 13:52:33 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 -    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	Mon Dec 10 10:41:29 2012 +0100
     2.2 +++ b/src/HOL/Statespace/StateSpaceEx.thy	Mon Dec 10 13:52:33 2012 +0100
     2.3 @@ -235,7 +235,7 @@
     2.4  
     2.5  ML {*
     2.6    fun make_benchmark n =
     2.7 -    writeln (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	Mon Dec 10 10:41:29 2012 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Dec 10 13:52:33 2012 +0100
     3.3 @@ -470,7 +470,8 @@
     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 (Sendback.make_markup {implicit = false, properties = []})
     3.8 +                  [Pretty.mark
     3.9 +                    (Active.make_markup Markup.sendbackN {implicit = false, properties = []})
    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	Mon Dec 10 10:41:29 2012 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 10 13:52:33 2012 +0100
     4.3 @@ -829,7 +829,7 @@
     4.4            (true, "")
     4.5          end)
     4.6  
     4.7 -fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub)
     4.8 +fun sendback sub = Active.sendback_markup (sledgehammerN ^ " " ^ sub)
     4.9  
    4.10  val commit_timeout = seconds 30.0
    4.11  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 10 10:41:29 2012 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Mon Dec 10 13:52:33 2012 +0100
     5.3 @@ -220,14 +220,14 @@
     5.4    command_call (string_for_reconstructor reconstr) ss
     5.5  
     5.6  fun try_command_line banner time command =
     5.7 -  banner ^ ": " ^ Sendback.markup command ^ show_time time ^ "."
     5.8 +  banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "."
     5.9  
    5.10  fun minimize_line _ [] = ""
    5.11    | minimize_line minimize_command ss =
    5.12      case minimize_command ss of
    5.13        "" => ""
    5.14      | command =>
    5.15 -      "\nTo minimize: " ^ Sendback.markup command ^ "."
    5.16 +      "\nTo minimize: " ^ Active.sendback_markup command ^ "."
    5.17  
    5.18  fun split_used_facts facts =
    5.19    facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
    5.20 @@ -728,7 +728,7 @@
    5.21            in
    5.22              "\n\nStructured proof "
    5.23                ^ (commas msg |> not (null msg) ? enclose "(" ")")
    5.24 -              ^ ":\n" ^ Sendback.markup isar_text
    5.25 +              ^ ":\n" ^ Active.sendback_markup isar_text
    5.26            end
    5.27        end
    5.28      val isar_proof =
     6.1 --- a/src/HOL/Tools/try0.ML	Mon Dec 10 10:41:29 2012 +0100
     6.2 +++ b/src/HOL/Tools/try0.ML	Mon Dec 10 13:52:33 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 -          Sendback.markup
     6.8 +          Active.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/General/graph_display.ML	Mon Dec 10 10:41:29 2012 +0100
     7.2 +++ b/src/Pure/General/graph_display.ML	Mon Dec 10 13:52:33 2012 +0100
     7.3 @@ -57,9 +57,11 @@
     7.4  
     7.5  fun display_graph graph =
     7.6    if print_mode_active graphview_reportN then
     7.7 -    (Output.report
     7.8 -      (YXML.string_of (XML.Elem ((Markup.graphviewN, []), encode_graphview graph)));
     7.9 -      writeln "(see graphview)")
    7.10 +    let
    7.11 +      val markup = Active.make_markup Markup.graphviewN {implicit = false, properties = []};
    7.12 +      val ((bg1, bg2), en) = YXML.output_markup_elem markup;
    7.13 +      val graph_yxml = YXML.string_of_body (encode_graphview graph);
    7.14 +    in writeln ("See " ^ bg1 ^ graph_yxml ^ bg2 ^ "graphview" ^ en) end
    7.15    else
    7.16      let
    7.17        val browser =
     8.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Dec 10 10:41:29 2012 +0100
     8.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Dec 10 13:52:33 2012 +0100
     8.3 @@ -66,7 +66,7 @@
     8.4  fun pretty_command (cmd as (name, Command {comment, ...})) =
     8.5    Pretty.block
     8.6      (Pretty.marks_str
     8.7 -      ([Sendback.make_markup {implicit = true, properties = [Markup.padding_line]},
     8.8 +      ([Active.make_markup Markup.sendbackN {implicit = true, properties = [Markup.padding_line]},
     8.9          command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
    8.10  
    8.11  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/PIDE/active.ML	Mon Dec 10 13:52:33 2012 +0100
     9.3 @@ -0,0 +1,37 @@
     9.4 +(*  Title:      Pure/PIDE/active.ML
     9.5 +    Author:     Makarius
     9.6 +
     9.7 +Active areas within the document (see also Tools/jEdit/src/active.scala).
     9.8 +*)
     9.9 +
    9.10 +signature ACTIVE =
    9.11 +sig
    9.12 +  val make_markup: string -> {implicit: bool, properties: Properties.T} -> Markup.T
    9.13 +  val markup_implicit: string -> string -> string
    9.14 +  val markup: string -> string -> string
    9.15 +  val sendback_markup_implicit: string -> string
    9.16 +  val sendback_markup: string -> string
    9.17 +end;
    9.18 +
    9.19 +structure Active: ACTIVE =
    9.20 +struct
    9.21 +
    9.22 +fun make_markup name {implicit, properties} =
    9.23 +  (name, [])
    9.24 +  |> not implicit ? (fn markup =>
    9.25 +      let
    9.26 +        val props =
    9.27 +          (case Position.get_id (Position.thread_data ()) of
    9.28 +            SOME id => [(Markup.idN, id)]
    9.29 +          | NONE => []);
    9.30 +      in Markup.properties props markup end)
    9.31 +  |> Markup.properties properties;
    9.32 +
    9.33 +fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s;
    9.34 +fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s;
    9.35 +
    9.36 +val sendback_markup_implicit = markup_implicit Markup.sendbackN;
    9.37 +val sendback_markup = markup Markup.sendbackN;
    9.38 +
    9.39 +end;
    9.40 +
    10.1 --- a/src/Pure/PIDE/markup.ML	Mon Dec 10 10:41:29 2012 +0100
    10.2 +++ b/src/Pure/PIDE/markup.ML	Mon Dec 10 13:52:33 2012 +0100
    10.3 @@ -98,7 +98,8 @@
    10.4    val subgoalN: string val subgoal: T
    10.5    val paddingN: string
    10.6    val padding_line: string * string
    10.7 -  val sendbackN: string val sendback: T
    10.8 +  val sendbackN: string
    10.9 +  val graphviewN: string
   10.10    val intensifyN: string val intensify: T
   10.11    val taskN: string
   10.12    val acceptedN: string val accepted: T
   10.13 @@ -120,7 +121,6 @@
   10.14    val reportN: string val report: T
   10.15    val no_reportN: string val no_report: T
   10.16    val badN: string val bad: T
   10.17 -  val graphviewN: string
   10.18    val functionN: string
   10.19    val assign_execs: Properties.T
   10.20    val removed_versions: Properties.T
   10.21 @@ -337,9 +337,14 @@
   10.22  val (stateN, state) = markup_elem "state";
   10.23  val (subgoalN, subgoal) = markup_elem "subgoal";
   10.24  
   10.25 +
   10.26 +(* active areads *)
   10.27 +
   10.28 +val sendbackN = "sendback";
   10.29 +val graphviewN = "graphview";
   10.30 +
   10.31  val paddingN = "padding";
   10.32  val padding_line = (paddingN, lineN);
   10.33 -val (sendbackN, sendback) = markup_elem "sendback";
   10.34  
   10.35  val (intensifyN, intensify) = markup_elem "intensify";
   10.36  
   10.37 @@ -376,8 +381,6 @@
   10.38  
   10.39  val (badN, bad) = markup_elem "bad";
   10.40  
   10.41 -val graphviewN = "graphview";
   10.42 -
   10.43  
   10.44  (* protocol message functions *)
   10.45  
    11.1 --- a/src/Pure/PIDE/markup.scala	Mon Dec 10 10:41:29 2012 +0100
    11.2 +++ b/src/Pure/PIDE/markup.scala	Mon Dec 10 13:52:33 2012 +0100
    11.3 @@ -212,9 +212,14 @@
    11.4    val STATE = "state"
    11.5    val SUBGOAL = "subgoal"
    11.6  
    11.7 +
    11.8 +  /* active areas */
    11.9 +
   11.10 +  val SENDBACK = "sendback"
   11.11 +  val GRAPHVIEW = "graphview"
   11.12 +
   11.13    val PADDING = "padding"
   11.14    val PADDING_LINE = (PADDING, LINE)
   11.15 -  val SENDBACK = "sendback"
   11.16  
   11.17    val INTENSIFY = "intensify"
   11.18  
   11.19 @@ -280,8 +285,6 @@
   11.20  
   11.21    val BAD = "bad"
   11.22  
   11.23 -  val GRAPHVIEW = "graphview"
   11.24 -
   11.25  
   11.26    /* protocol message functions */
   11.27  
    12.1 --- a/src/Pure/PIDE/protocol.scala	Mon Dec 10 10:41:29 2012 +0100
    12.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Dec 10 13:52:33 2012 +0100
    12.3 @@ -118,10 +118,12 @@
    12.4  
    12.5    /* result messages */
    12.6  
    12.7 +  private val clean = Set(Markup.REPORT, Markup.NO_REPORT)
    12.8 +
    12.9    def clean_message(body: XML.Body): XML.Body =
   12.10      body filter {
   12.11 -      case XML.Elem(Markup(Markup.REPORT, _), _) => false
   12.12 -      case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false
   12.13 +      case XML.Wrapped_Elem(Markup(name, _), _, _) => !clean(name)
   12.14 +      case XML.Elem(Markup(name, _), _) => !clean(name)
   12.15        case _ => true
   12.16      } map {
   12.17        case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
   12.18 @@ -131,6 +133,8 @@
   12.19  
   12.20    def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
   12.21      body flatMap {
   12.22 +      case XML.Wrapped_Elem(Markup(Markup.REPORT, ps), body, ts) =>
   12.23 +        List(XML.Wrapped_Elem(Markup(Markup.REPORT, props ::: ps), body, ts))
   12.24        case XML.Elem(Markup(Markup.REPORT, ps), ts) =>
   12.25          List(XML.Elem(Markup(Markup.REPORT, props ::: ps), ts))
   12.26        case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
    13.1 --- a/src/Pure/PIDE/sendback.ML	Mon Dec 10 10:41:29 2012 +0100
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,33 +0,0 @@
    13.4 -(*  Title:      Pure/PIDE/sendback.ML
    13.5 -    Author:     Makarius
    13.6 -
    13.7 -Clickable "sendback" areas within the source text (see also
    13.8 -Tools/jEdit/src/sendback.scala).
    13.9 -*)
   13.10 -
   13.11 -signature SENDBACK =
   13.12 -sig
   13.13 -  val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
   13.14 -  val markup_implicit: string -> string
   13.15 -  val markup: string -> string
   13.16 -end;
   13.17 -
   13.18 -structure Sendback: SENDBACK =
   13.19 -struct
   13.20 -
   13.21 -fun make_markup {implicit, properties} =
   13.22 -  Markup.sendback
   13.23 -  |> not implicit ? (fn markup =>
   13.24 -      let
   13.25 -        val props =
   13.26 -          (case Position.get_id (Position.thread_data ()) of
   13.27 -            SOME id => [(Markup.idN, id)]
   13.28 -          | NONE => []);
   13.29 -      in Markup.properties props markup end)
   13.30 -  |> Markup.properties properties;
   13.31 -
   13.32 -fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
   13.33 -fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
   13.34 -
   13.35 -end;
   13.36 -
    14.1 --- a/src/Pure/ROOT	Mon Dec 10 10:41:29 2012 +0100
    14.2 +++ b/src/Pure/ROOT	Mon Dec 10 13:52:33 2012 +0100
    14.3 @@ -144,11 +144,11 @@
    14.4      "ML/ml_statistics_polyml-5.5.0.ML"
    14.5      "ML/ml_syntax.ML"
    14.6      "ML/ml_thms.ML"
    14.7 +    "PIDE/active.ML"
    14.8      "PIDE/command.ML"
    14.9      "PIDE/document.ML"
   14.10      "PIDE/markup.ML"
   14.11      "PIDE/protocol.ML"
   14.12 -    "PIDE/sendback.ML"
   14.13      "PIDE/xml.ML"
   14.14      "PIDE/yxml.ML"
   14.15      "Proof/extraction.ML"
    15.1 --- a/src/Pure/ROOT.ML	Mon Dec 10 10:41:29 2012 +0100
    15.2 +++ b/src/Pure/ROOT.ML	Mon Dec 10 13:52:33 2012 +0100
    15.3 @@ -63,7 +63,7 @@
    15.4  
    15.5  use "PIDE/xml.ML";
    15.6  use "PIDE/yxml.ML";
    15.7 -use "PIDE/sendback.ML";
    15.8 +use "PIDE/active.ML";
    15.9  
   15.10  use "General/graph.ML";
   15.11  
    16.1 --- a/src/Tools/jEdit/etc/options	Mon Dec 10 10:41:29 2012 +0100
    16.2 +++ b/src/Tools/jEdit/etc/options	Mon Dec 10 13:52:33 2012 +0100
    16.3 @@ -41,8 +41,8 @@
    16.4  option quoted_color : string = "8B8B8B19"
    16.5  option highlight_color : string = "50505032"
    16.6  option hyperlink_color : string = "000000FF"
    16.7 -option sendback_color : string = "DCDCDCFF"
    16.8 -option sendback_active_color : string = "9DC75DFF"
    16.9 +option active_color : string = "DCDCDCFF"
   16.10 +option active_hover_color : string = "9DC75DFF"
   16.11  option keyword1_color : string = "006699FF"
   16.12  option keyword2_color : string = "009966FF"
   16.13  
    17.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Dec 10 10:41:29 2012 +0100
    17.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Dec 10 13:52:33 2012 +0100
    17.3 @@ -8,6 +8,7 @@
    17.4  ## sources
    17.5  
    17.6  declare -a SOURCES=(
    17.7 +  "src/active.scala"
    17.8    "src/dockable.scala"
    17.9    "src/document_model.scala"
   17.10    "src/document_view.scala"
   17.11 @@ -35,7 +36,6 @@
   17.12    "src/rendering.scala"
   17.13    "src/rich_text_area.scala"
   17.14    "src/scala_console.scala"
   17.15 -  "src/sendback.scala"
   17.16    "src/symbols_dockable.scala"
   17.17    "src/syslog_dockable.scala"
   17.18    "src/text_overview.scala"
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/Tools/jEdit/src/active.scala	Mon Dec 10 13:52:33 2012 +0100
    18.3 @@ -0,0 +1,63 @@
    18.4 +/*  Title:      Tools/jEdit/src/active.scala
    18.5 +    Author:     Makarius
    18.6 +
    18.7 +Active areas within the document.
    18.8 +*/
    18.9 +
   18.10 +package isabelle.jedit
   18.11 +
   18.12 +
   18.13 +import isabelle._
   18.14 +
   18.15 +import org.gjt.sp.jedit.View
   18.16 +
   18.17 +
   18.18 +object Active
   18.19 +{
   18.20 +  def action(view: View, text: String, elem: XML.Elem)
   18.21 +  {
   18.22 +    Swing_Thread.require()
   18.23 +
   18.24 +    Document_View(view.getTextArea) match {
   18.25 +      case Some(doc_view) =>
   18.26 +        doc_view.rich_text_area.robust_body() {
   18.27 +          val text_area = doc_view.text_area
   18.28 +          val model = doc_view.model
   18.29 +          val buffer = model.buffer
   18.30 +          val snapshot = model.snapshot()
   18.31 +
   18.32 +          if (!snapshot.is_outdated) {
   18.33 +            elem match {
   18.34 +              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
   18.35 +                props match {
   18.36 +                  case Position.Id(exec_id) =>
   18.37 +                    snapshot.state.execs.get(exec_id).map(_.command) match {
   18.38 +                      case Some(command) =>
   18.39 +                        snapshot.node.command_start(command) match {
   18.40 +                          case Some(start) =>
   18.41 +                            JEdit_Lib.buffer_edit(buffer) {
   18.42 +                              buffer.remove(start, command.proper_range.length)
   18.43 +                              buffer.insert(start, text)
   18.44 +                            }
   18.45 +                          case None =>
   18.46 +                        }
   18.47 +                      case None =>
   18.48 +                    }
   18.49 +                  case _ =>
   18.50 +                    if (props.exists(_ == Markup.PADDING_LINE))
   18.51 +                      Isabelle.insert_line_padding(text_area, text)
   18.52 +                    else text_area.setSelectedText(text)
   18.53 +                }
   18.54 +
   18.55 +              case XML.Elem(Markup(Markup.GRAPHVIEW, props), body) =>
   18.56 +                java.lang.System.err.println("graphview " + props)  // FIXME
   18.57 +
   18.58 +              case _ =>
   18.59 +            }
   18.60 +          }
   18.61 +        }
   18.62 +      case None =>
   18.63 +    }
   18.64 +  }
   18.65 +}
   18.66 +
    19.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Dec 10 10:41:29 2012 +0100
    19.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Dec 10 13:52:33 2012 +0100
    19.3 @@ -135,8 +135,8 @@
    19.4    val quoted_color = color_value("quoted_color")
    19.5    val highlight_color = color_value("highlight_color")
    19.6    val hyperlink_color = color_value("hyperlink_color")
    19.7 -  val sendback_color = color_value("sendback_color")
    19.8 -  val sendback_active_color = color_value("sendback_active_color")
    19.9 +  val active_color = color_value("active_color")
   19.10 +  val active_hover_color = color_value("active_hover_color")
   19.11    val keyword1_color = color_value("keyword1_color")
   19.12    val keyword2_color = color_value("keyword2_color")
   19.13  
   19.14 @@ -249,11 +249,13 @@
   19.15    }
   19.16  
   19.17  
   19.18 -  def sendback(range: Text.Range): Option[Text.Info[Properties.T]] =
   19.19 -    snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
   19.20 +  private val active_include = Set(Markup.SENDBACK, Markup.GRAPHVIEW)
   19.21 +
   19.22 +  def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
   19.23 +    snapshot.select_markup(range, Some(active_include),
   19.24          {
   19.25 -          case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
   19.26 -            Text.Info(snapshot.convert(info_range), props)
   19.27 +          case Text.Info(info_range, elem @ XML.Elem(markup, _))
   19.28 +          if active_include(markup.name) => Text.Info(snapshot.convert(info_range), elem)
   19.29          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   19.30  
   19.31  
   19.32 @@ -405,8 +407,8 @@
   19.33  
   19.34    private val background1_include =
   19.35      Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
   19.36 -      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY +
   19.37 -      Markup.SENDBACK
   19.38 +      Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
   19.39 +      active_include
   19.40  
   19.41    def background1(range: Text.Range): Stream[Text.Info[Color]] =
   19.42    {
   19.43 @@ -424,8 +426,8 @@
   19.44                  (None, Some(bad_color))
   19.45                case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
   19.46                  (None, Some(intensify_color))
   19.47 -              case (_, Text.Info(_, XML.Elem(Markup(Markup.SENDBACK, _), _))) =>
   19.48 -                (None, Some(sendback_color))
   19.49 +              case (_, Text.Info(_, XML.Elem(Markup(name, _), _))) if active_include(name) =>
   19.50 +                (None, Some(active_color))
   19.51              })
   19.52          color <-
   19.53            (result match {
    20.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Dec 10 10:41:29 2012 +0100
    20.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Dec 10 13:52:33 2012 +0100
    20.3 @@ -135,10 +135,10 @@
    20.4  
    20.5    private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
    20.6    private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
    20.7 -  private val sendback_area = new Active_Area[Properties.T]((r: Rendering) => r.sendback _)
    20.8 +  private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _)
    20.9  
   20.10    private val active_areas =
   20.11 -    List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
   20.12 +    List((highlight_area, true), (hyperlink_area, true), (active_area, false))
   20.13    def active_reset(): Unit = active_areas.foreach(_._1.reset)
   20.14  
   20.15    private val focus_listener = new FocusAdapter {
   20.16 @@ -157,8 +157,8 @@
   20.17            case Some(Text.Info(_, link)) => link.follow(view)
   20.18            case None =>
   20.19          }
   20.20 -        sendback_area.text_info match {
   20.21 -          case Some((text, Text.Info(_, props))) => Sendback.activate(view, text, props)
   20.22 +        active_area.text_info match {
   20.23 +          case Some((text, Text.Info(_, markup))) => Active.action(view, text, markup)
   20.24            case None =>
   20.25          }
   20.26        }
   20.27 @@ -252,13 +252,13 @@
   20.28                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   20.29              }
   20.30  
   20.31 -            // sendback range -- potentially from other snapshot
   20.32 +            // active area -- potentially from other snapshot
   20.33              for {
   20.34 -              info <- sendback_area.info
   20.35 +              info <- active_area.info
   20.36                Text.Info(range, _) <- info.try_restrict(line_range)
   20.37                r <- JEdit_Lib.gfx_range(text_area, range)
   20.38              } {
   20.39 -              gfx.setColor(rendering.sendback_active_color)
   20.40 +              gfx.setColor(rendering.active_hover_color)
   20.41                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   20.42              }
   20.43  
    21.1 --- a/src/Tools/jEdit/src/sendback.scala	Mon Dec 10 10:41:29 2012 +0100
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,55 +0,0 @@
    21.4 -/*  Title:      Tools/jEdit/src/sendback.scala
    21.5 -    Author:     Makarius
    21.6 -
    21.7 -Clickable "sendback" areas within the source text.
    21.8 -*/
    21.9 -
   21.10 -package isabelle.jedit
   21.11 -
   21.12 -
   21.13 -import isabelle._
   21.14 -
   21.15 -import org.gjt.sp.jedit.View
   21.16 -
   21.17 -
   21.18 -object Sendback
   21.19 -{
   21.20 -  def activate(view: View, text: String, props: Properties.T)
   21.21 -  {
   21.22 -    Swing_Thread.require()
   21.23 -
   21.24 -    Document_View(view.getTextArea) match {
   21.25 -      case Some(doc_view) =>
   21.26 -        doc_view.rich_text_area.robust_body() {
   21.27 -          val text_area = doc_view.text_area
   21.28 -          val model = doc_view.model
   21.29 -          val buffer = model.buffer
   21.30 -          val snapshot = model.snapshot()
   21.31 -
   21.32 -          if (!snapshot.is_outdated) {
   21.33 -            props match {
   21.34 -              case Position.Id(exec_id) =>
   21.35 -                snapshot.state.execs.get(exec_id).map(_.command) match {
   21.36 -                  case Some(command) =>
   21.37 -                    snapshot.node.command_start(command) match {
   21.38 -                      case Some(start) =>
   21.39 -                        JEdit_Lib.buffer_edit(buffer) {
   21.40 -                          buffer.remove(start, command.proper_range.length)
   21.41 -                          buffer.insert(start, text)
   21.42 -                        }
   21.43 -                      case None =>
   21.44 -                    }
   21.45 -                  case None =>
   21.46 -                }
   21.47 -              case _ =>
   21.48 -                if (props.exists(_ == Markup.PADDING_LINE))
   21.49 -                  Isabelle.insert_line_padding(text_area, text)
   21.50 -                else text_area.setSelectedText(text)
   21.51 -            }
   21.52 -          }
   21.53 -        }
   21.54 -      case None =>
   21.55 -    }
   21.56 -  }
   21.57 -}
   21.58 -