# HG changeset patch
# User wenzelm
# Date 1353943007 -3600
# Node ID 97959912840a71562867dac7952a4df208429c40
# Parent  67fb9a168d1051f36d9a4940ca693775daed0360
more general sendback properties;
support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';

diff -r 67fb9a168d10 -r 97959912840a src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Nov 26 16:16:47 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}) (Pretty.blk (0,
+                  [Pretty.mark (Sendback.make_markup {implicit = false, properties = []})
+                    (Pretty.blk (0,
                        pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
             else
               ()
diff -r 67fb9a168d10 -r 97959912840a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Nov 26 16:16:47 2012 +0100
@@ -66,8 +66,8 @@
 fun pretty_command (cmd as (name, Command {comment, ...})) =
   Pretty.block
     (Pretty.marks_str
-      ([Sendback.make_markup {implicit = true}, command_markup false cmd], name) ::
-      Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
+      ([Sendback.make_markup {implicit = true, properties = [Markup.padding_line]},
+        command_markup false cmd], name) :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
 
 
 (* parse command *)
diff -r 67fb9a168d10 -r 97959912840a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Nov 26 16:16:47 2012 +0100
@@ -96,6 +96,8 @@
   val proof_stateN: string val proof_state: int -> T
   val stateN: string val state: T
   val subgoalN: string val subgoal: T
+  val paddingN: string
+  val padding_line: string * string
   val sendbackN: string val sendback: T
   val intensifyN: string val intensify: T
   val taskN: string
@@ -333,7 +335,11 @@
 
 val (stateN, state) = markup_elem "state";
 val (subgoalN, subgoal) = markup_elem "subgoal";
+
+val paddingN = "padding";
+val padding_line = (paddingN, lineN);
 val (sendbackN, sendback) = markup_elem "sendback";
+
 val (intensifyN, intensify) = markup_elem "intensify";
 
 
diff -r 67fb9a168d10 -r 97959912840a src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Nov 26 16:16:47 2012 +0100
@@ -211,7 +211,11 @@
 
   val STATE = "state"
   val SUBGOAL = "subgoal"
+
+  val PADDING = "padding"
+  val PADDING_LINE = (PADDING, LINE)
   val SENDBACK = "sendback"
+
   val INTENSIFY = "intensify"
 
 
diff -r 67fb9a168d10 -r 97959912840a src/Pure/PIDE/sendback.ML
--- a/src/Pure/PIDE/sendback.ML	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Pure/PIDE/sendback.ML	Mon Nov 26 16:16:47 2012 +0100
@@ -7,7 +7,7 @@
 
 signature SENDBACK =
 sig
-  val make_markup: {implicit: bool} -> Markup.T
+  val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
   val markup_implicit: string -> string
   val markup: string -> string
 end;
@@ -15,18 +15,19 @@
 structure Sendback: SENDBACK =
 struct
 
-fun make_markup {implicit} =
-  if implicit then Markup.sendback
-  else
-    let
-      val props =
-        (case Position.get_id (Position.thread_data ()) of
-          SOME id => [(Markup.idN, id)]
-        | NONE => []);
-    in Markup.properties props Markup.sendback end;
+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}) s;
-fun markup s = Markup.markup (make_markup {implicit = false}) s;
+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 67fb9a168d10 -r 97959912840a src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Nov 26 16:16:47 2012 +0100
@@ -105,6 +105,13 @@
   }
 
 
+  /* get text */
+
+  def try_get_text(buffer: JEditBuffer, range: Text.Range): Option[String] =
+    try { Some(buffer.getText(range.start, range.length)) }
+    catch { case _: ArrayIndexOutOfBoundsException => None }
+
+
   /* point range */
 
   def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
diff -r 67fb9a168d10 -r 97959912840a src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Nov 26 16:16:47 2012 +0100
@@ -249,11 +249,11 @@
   }
 
 
-  def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
+  def sendback(range: Text.Range): Option[Text.Info[Properties.T]] =
     snapshot.select_markup(range, Some(Set(Markup.SENDBACK)),
         {
           case Text.Info(info_range, XML.Elem(Markup(Markup.SENDBACK, props), _)) =>
-            Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
+            Text.Info(snapshot.convert(info_range), props)
         }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
 
 
diff -r 67fb9a168d10 -r 97959912840a src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Nov 26 16:16:47 2012 +0100
@@ -134,7 +134,7 @@
 
   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[Option[Document.Exec_ID]]((r: Rendering) => r.sendback _)
+  private val sendback_area = new Active_Area[Properties.T]((r: Rendering) => r.sendback _)
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
@@ -157,7 +157,7 @@
           case None =>
         }
         sendback_area.text_info match {
-          case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id)
+          case Some((text, Text.Info(_, props))) => Sendback.activate(view, text, props)
           case None =>
         }
       }
diff -r 67fb9a168d10 -r 97959912840a src/Tools/jEdit/src/sendback.scala
--- a/src/Tools/jEdit/src/sendback.scala	Mon Nov 26 14:43:28 2012 +0100
+++ b/src/Tools/jEdit/src/sendback.scala	Mon Nov 26 16:16:47 2012 +0100
@@ -14,22 +14,21 @@
 
 object Sendback
 {
-  def activate(view: View, text: String, id: Option[Document.Exec_ID])
+  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) {
-            id match {
-              case None =>
-                doc_view.text_area.setSelectedText(text)
-              case Some(exec_id) =>
+            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 {
@@ -42,6 +41,22 @@
                     }
                   case None =>
                 }
+              case _ =>
+                JEdit_Lib.buffer_edit(buffer) {
+                  val text1 =
+                    if (props.exists(_ == Markup.PADDING_LINE) &&
+                        text_area.getSelectionCount == 0)
+                    {
+                      def pad(range: Text.Range): String =
+                        if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
+
+                      val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+                      val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
+                      pad(before_caret) + text + pad(caret)
+                    }
+                    else text
+                  text_area.setSelectedText(text1)
+                }
             }
           }
         }