src/Pure/PIDE/sendback.ML
author wenzelm
Mon Nov 26 16:16:47 2012 +0100 (2012-11-26 ago)
changeset 50215 97959912840a
parent 50212 4fb06c22c5ec
permissions -rw-r--r--
more general sendback properties;
support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
wenzelm@50163
     1
(*  Title:      Pure/PIDE/sendback.ML
wenzelm@50163
     2
    Author:     Makarius
wenzelm@50163
     3
wenzelm@50163
     4
Clickable "sendback" areas within the source text (see also
wenzelm@50163
     5
Tools/jEdit/src/sendback.scala).
wenzelm@50163
     6
*)
wenzelm@50163
     7
wenzelm@50163
     8
signature SENDBACK =
wenzelm@50163
     9
sig
wenzelm@50215
    10
  val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
wenzelm@50212
    11
  val markup_implicit: string -> string
wenzelm@50163
    12
  val markup: string -> string
wenzelm@50163
    13
end;
wenzelm@50163
    14
wenzelm@50163
    15
structure Sendback: SENDBACK =
wenzelm@50163
    16
struct
wenzelm@50163
    17
wenzelm@50215
    18
fun make_markup {implicit, properties} =
wenzelm@50215
    19
  Markup.sendback
wenzelm@50215
    20
  |> not implicit ? (fn markup =>
wenzelm@50215
    21
      let
wenzelm@50215
    22
        val props =
wenzelm@50215
    23
          (case Position.get_id (Position.thread_data ()) of
wenzelm@50215
    24
            SOME id => [(Markup.idN, id)]
wenzelm@50215
    25
          | NONE => []);
wenzelm@50215
    26
      in Markup.properties props markup end)
wenzelm@50215
    27
  |> Markup.properties properties;
wenzelm@50163
    28
wenzelm@50215
    29
fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
wenzelm@50215
    30
fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
wenzelm@50164
    31
wenzelm@50163
    32
end;
wenzelm@50163
    33