author | wenzelm |
Thu, 13 Dec 2012 18:15:53 +0100 | |
changeset 50504 | 2cc6eab90cdf |
parent 50500 | c94bba7906d2 |
child 50505 | 33c92722cc3d |
permissions | -rw-r--r-- |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
1 |
(* Title: Pure/PIDE/active.ML |
50163
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 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
4 |
Active areas within the document (see also Tools/jEdit/src/active.scala). |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
5 |
*) |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
6 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
7 |
signature ACTIVE = |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
8 |
sig |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
9 |
val make_markup: string -> {implicit: bool, properties: Properties.T} -> Markup.T |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
10 |
val markup_implicit: string -> string -> string |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
11 |
val markup: string -> string -> string |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
12 |
val sendback_markup_implicit: string -> string |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
13 |
val sendback_markup: string -> string |
50498 | 14 |
val dialog: unit -> (string -> Markup.T) * string future |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
15 |
val dialog_result: serial -> string -> unit |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
16 |
end; |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
17 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
18 |
structure Active: ACTIVE = |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
19 |
struct |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
20 |
|
50498 | 21 |
(* active markup *) |
22 |
||
23 |
fun explicit_id () = |
|
24 |
(case Position.get_id (Position.thread_data ()) of |
|
25 |
SOME id => [(Markup.idN, id)] |
|
26 |
| NONE => []); |
|
27 |
||
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
28 |
fun make_markup name {implicit, properties} = |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
29 |
(name, []) |
50498 | 30 |
|> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup) |
50215 | 31 |
|> Markup.properties properties; |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
32 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
33 |
fun markup_implicit name s = Markup.markup (make_markup name {implicit = true, properties = []}) s; |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
34 |
fun markup name s = Markup.markup (make_markup name {implicit = false, properties = []}) s; |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
35 |
|
50498 | 36 |
|
37 |
(* sendback area *) |
|
38 |
||
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
39 |
val sendback_markup_implicit = markup_implicit Markup.sendbackN; |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
40 |
val sendback_markup = markup Markup.sendbackN; |
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
|
41 |
|
50498 | 42 |
|
43 |
(* dialog via document content *) |
|
44 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
45 |
val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table); |
50498 | 46 |
|
47 |
fun dialog () = |
|
48 |
let |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
49 |
val i = serial (); |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
50 |
fun abort () = Synchronized.change dialogs (Inttab.delete_safe i); |
50498 | 51 |
val promise = Future.promise abort : string future; |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
52 |
val _ = Synchronized.change dialogs (Inttab.update_new (i, promise)); |
50504 | 53 |
fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result); |
54 |
in (result_markup, promise) end; |
|
50498 | 55 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
56 |
fun dialog_result i result = |
50498 | 57 |
Synchronized.change_result dialogs |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
58 |
(fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab)) |
50498 | 59 |
|> (fn NONE => () | SOME promise => Future.fulfill promise result); |
60 |
||
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
61 |
end; |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
62 |