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';
     1 (*  Title:      Pure/PIDE/sendback.ML
     2     Author:     Makarius
     3 
     4 Clickable "sendback" areas within the source text (see also
     5 Tools/jEdit/src/sendback.scala).
     6 *)
     7 
     8 signature SENDBACK =
     9 sig
    10   val make_markup: {implicit: bool, properties: Properties.T} -> Markup.T
    11   val markup_implicit: string -> string
    12   val markup: string -> string
    13 end;
    14 
    15 structure Sendback: SENDBACK =
    16 struct
    17 
    18 fun make_markup {implicit, properties} =
    19   Markup.sendback
    20   |> not implicit ? (fn markup =>
    21       let
    22         val props =
    23           (case Position.get_id (Position.thread_data ()) of
    24             SOME id => [(Markup.idN, id)]
    25           | NONE => []);
    26       in Markup.properties props markup end)
    27   |> Markup.properties properties;
    28 
    29 fun markup_implicit s = Markup.markup (make_markup {implicit = true, properties = []}) s;
    30 fun markup s = Markup.markup (make_markup {implicit = false, properties = []}) s;
    31 
    32 end;
    33