| author | wenzelm |
| Thu, 22 Nov 2012 22:21:54 +0100 | |
| changeset 50172 | 1a28109edc6d |
| parent 50164 | 77668b522ffe |
| child 50201 | c26369c9eda6 |
| permissions | -rw-r--r-- |
|
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 |