src/Pure/PIDE/sendback.ML
author wenzelm
Thu, 22 Nov 2012 22:21:54 +0100
changeset 50172 1a28109edc6d
parent 50164 77668b522ffe
child 50201 c26369c9eda6
permissions -rw-r--r--
defer interpretation of markup via implicit print mode;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50163
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/PIDE/sendback.ML
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     3
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     4
Clickable "sendback" areas within the source text (see also
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     5
Tools/jEdit/src/sendback.scala).
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     6
*)
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     7
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     8
signature SENDBACK =
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
     9
sig
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    10
  val make_markup: unit -> Markup.T
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    11
  val markup: string -> string
50164
77668b522ffe some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents: 50163
diff changeset
    12
  val markup_implicit: string -> string
50163
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    13
end;
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    14
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    15
structure Sendback: SENDBACK =
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    16
struct
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    17
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    18
fun make_markup () =
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    19
  let
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    20
    val props =
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    21
      (case Position.get_id (Position.thread_data ()) of
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    22
        SOME id => [(Isabelle_Markup.idN, id)]
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    23
      | NONE => []);
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    24
  in Markup.properties props Isabelle_Markup.sendback end;
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    25
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    26
fun markup s = Markup.markup (make_markup ()) s;
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    27
50172
1a28109edc6d defer interpretation of markup via implicit print mode;
wenzelm
parents: 50164
diff changeset
    28
fun markup_implicit s = Markup.markup Isabelle_Markup.sendback s;
50164
77668b522ffe some support for implicit senback, meaning that it uses the caret position instead of explicit command exec_id;
wenzelm
parents: 50163
diff changeset
    29
50163
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    30
end;
c62ce309dc26 more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff changeset
    31