more general sendback properties;
authorwenzelm
Mon Nov 26 16:16:47 2012 +0100 (2012-11-26 ago)
changeset 5021597959912840a
parent 50214 67fb9a168d10
child 50216 de77cde57376
more general sendback properties;
support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
src/HOL/Tools/Nitpick/nitpick.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/sendback.ML
src/Tools/jEdit/src/jedit_lib.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/Tools/Nitpick/nitpick.ML	Mon Nov 26 14:43:28 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 16:16:47 2012 +0100
     1.3 @@ -470,7 +470,8 @@
     1.4                pprint_nt (fn () => Pretty.blk (0,
     1.5                    pstrs "Hint: To check that the induction hypothesis is \
     1.6                          \general enough, try this command: " @
     1.7 -                  [Pretty.mark (Sendback.make_markup {implicit = false}) (Pretty.blk (0,
     1.8 +                  [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
     1.9 +                    (Pretty.blk (0,
    1.10                         pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
    1.11              else
    1.12                ()
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 14:43:28 2012 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 16:16:47 2012 +0100
     2.3 @@ -66,8 +66,8 @@
     2.4  fun pretty_command (cmd as (name, Command {comment, ...})) =
     2.5    Pretty.block
     2.6      (Pretty.marks_str
     2.7 -      ([Sendback.make_markup {implicit = true}, command_markup false cmd], name) ::
     2.8 -      Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
     2.9 +      ([Sendback.make_markup {implicit = true, properties = [Markup.padding_line]},
    2.10 +        command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
    2.11  
    2.12  
    2.13  (* parse command *)
     3.1 --- a/src/Pure/PIDE/markup.ML	Mon Nov 26 14:43:28 2012 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Mon Nov 26 16:16:47 2012 +0100
     3.3 @@ -96,6 +96,8 @@
     3.4    val proof_stateN: string val proof_state: int -> T
     3.5    val stateN: string val state: T
     3.6    val subgoalN: string val subgoal: T
     3.7 +  val paddingN: string
     3.8 +  val padding_line: string * string
     3.9    val sendbackN: string val sendback: T
    3.10    val intensifyN: string val intensify: T
    3.11    val taskN: string
    3.12 @@ -333,7 +335,11 @@
    3.13  
    3.14  val (stateN, state) = markup_elem "state";
    3.15  val (subgoalN, subgoal) = markup_elem "subgoal";
    3.16 +
    3.17 +val paddingN = "padding";
    3.18 +val padding_line = (paddingN, lineN);
    3.19  val (sendbackN, sendback) = markup_elem "sendback";
    3.20 +
    3.21  val (intensifyN, intensify) = markup_elem "intensify";
    3.22  
    3.23  
     4.1 --- a/src/Pure/PIDE/markup.scala	Mon Nov 26 14:43:28 2012 +0100
     4.2 +++ b/src/Pure/PIDE/markup.scala	Mon Nov 26 16:16:47 2012 +0100
     4.3 @@ -211,7 +211,11 @@
     4.4  
     4.5    val STATE = "state"
     4.6    val SUBGOAL = "subgoal"
     4.7 +
     4.8 +  val PADDING = "padding"
     4.9 +  val PADDING_LINE = (PADDING, LINE)
    4.10    val SENDBACK = "sendback"
    4.11 +
    4.12    val INTENSIFY = "intensify"
    4.13  
    4.14  
     5.1 --- a/src/Pure/PIDE/sendback.ML	Mon Nov 26 14:43:28 2012 +0100
     5.2 +++ b/src/Pure/PIDE/sendback.ML	Mon Nov 26 16:16:47 2012 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  signature SENDBACK =
     5.6  sig
     5.7 -  val make_markup: {implicit: bool} -> Markup.T
     5.8 +  val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
     5.9    val markup_implicit: string -> string
    5.10    val markup: string -> string
    5.11  end;
    5.12 @@ -15,18 +15,19 @@
    5.13  structure Sendback: SENDBACK =
    5.14  struct
    5.15  
    5.16 -fun make_markup {implicit} =
    5.17 -  if implicit then Markup.sendback
    5.18 -  else
    5.19 -    let
    5.20 -      val props =
    5.21 -        (case Position.get_id (Position.thread_data ()) of
    5.22 -          SOME id => [(Markup.idN, id)]
    5.23 -        | NONE => []);
    5.24 -    in Markup.properties props Markup.sendback end;
    5.25 +fun make_markup {implicit, properties} =
    5.26 +  Markup.sendback
    5.27 +  |> not implicit ? (fn markup =>
    5.28 +      let
    5.29 +        val props =
    5.30 +          (case Position.get_id (Position.thread_data ()) of
    5.31 +            SOME id => [(Markup.idN, id)]
    5.32 +          | NONE => []);
    5.33 +      in Markup.properties props markup end)
    5.34 +  |> Markup.properties properties;
    5.35  
    5.36 -fun markup_implicit s = Markup.markup (make_markup {implicit = true}) s;
    5.37 -fun markup s = Markup.markup (make_markup {implicit = false}) s;
    5.38 +fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
    5.39 +fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
    5.40  
    5.41  end;
    5.42  
     6.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 26 14:43:28 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 26 16:16:47 2012 +0100
     6.3 @@ -105,6 +105,13 @@
     6.4    }
     6.5  
     6.6  
     6.7 +  /* get text */
     6.8 +
     6.9 +  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
    6.10 +    try { Some(buffer.getText(range.start, range.length)) }
    6.11 +    catch { case _: ArrayIndexOutOfBoundsException => None }
    6.12 +
    6.13 +
    6.14    /* point range */
    6.15  
    6.16    def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
     7.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Nov 26 14:43:28 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Nov 26 16:16:47 2012 +0100
     7.3 @@ -249,11 +249,11 @@
     7.4    }
     7.5  
     7.6  
     7.7 -  def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
     7.8 +  def sendback(range: Text.Range): Option[Text.Info[Properties.T]] =
     7.9      snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
    7.10          {
    7.11            case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
    7.12 -            Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
    7.13 +            Text.Info(snapshot.convert(info_range), props)
    7.14          }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
    7.15  
    7.16  
     8.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 14:43:28 2012 +0100
     8.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 16:16:47 2012 +0100
     8.3 @@ -134,7 +134,7 @@
     8.4  
     8.5    private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _)
     8.6    private val hyperlink_area = new Active_Area[Hyperlink]((r: Rendering) => r.hyperlink _)
     8.7 -  private val sendback_area = new Active_Area[Option[Document.Exec_ID]]((r: Rendering) => r.sendback _)
     8.8 +  private val sendback_area = new Active_Area[Properties.T]((r: Rendering) => r.sendback _)
     8.9  
    8.10    private val active_areas =
    8.11      List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
    8.12 @@ -157,7 +157,7 @@
    8.13            case None =>
    8.14          }
    8.15          sendback_area.text_info match {
    8.16 -          case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id)
    8.17 +          case Some((text, Text.Info(_, props))) => Sendback.activate(view, text, props)
    8.18            case None =>
    8.19          }
    8.20        }
     9.1 --- a/src/Tools/jEdit/src/sendback.scala	Mon Nov 26 14:43:28 2012 +0100
     9.2 +++ b/src/Tools/jEdit/src/sendback.scala	Mon Nov 26 16:16:47 2012 +0100
     9.3 @@ -14,22 +14,21 @@
     9.4  
     9.5  object Sendback
     9.6  {
     9.7 -  def activate(view: View, text: String, id: Option[Document.Exec_ID])
     9.8 +  def activate(view: View, text: String, props: Properties.T)
     9.9    {
    9.10      Swing_Thread.require()
    9.11  
    9.12      Document_View(view.getTextArea) match {
    9.13        case Some(doc_view) =>
    9.14          doc_view.rich_text_area.robust_body() {
    9.15 +          val text_area = doc_view.text_area
    9.16            val model = doc_view.model
    9.17            val buffer = model.buffer
    9.18            val snapshot = model.snapshot()
    9.19  
    9.20            if (!snapshot.is_outdated) {
    9.21 -            id match {
    9.22 -              case None =>
    9.23 -                doc_view.text_area.setSelectedText(text)
    9.24 -              case Some(exec_id) =>
    9.25 +            props match {
    9.26 +              case Position.Id(exec_id) =>
    9.27                  snapshot.state.execs.get(exec_id).map(_.command) match {
    9.28                    case Some(command) =>
    9.29                      snapshot.node.command_start(command) match {
    9.30 @@ -42,6 +41,22 @@
    9.31                      }
    9.32                    case None =>
    9.33                  }
    9.34 +              case _ =>
    9.35 +                JEdit_Lib.buffer_edit(buffer) {
    9.36 +                  val text1 =
    9.37 +                    if (props.exists(_ == Markup.PADDING_LINE) &&
    9.38 +                        text_area.getSelectionCount == 0)
    9.39 +                    {
    9.40 +                      def pad(range: Text.Range): String =
    9.41 +                        if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
    9.42 +
    9.43 +                      val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
    9.44 +                      val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
    9.45 +                      pad(before_caret) + text + pad(caret)
    9.46 +                    }
    9.47 +                    else text
    9.48 +                  text_area.setSelectedText(text1)
    9.49 +                }
    9.50              }
    9.51            }
    9.52          }