author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 50505 | 33c92722cc3d |
child 52697 | 6fb98a20c349 |
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 |
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50504
diff
changeset
|
15 |
val dialog_text: unit -> (string -> string) * string future |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
16 |
val dialog_result: serial -> string -> unit |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
17 |
end; |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
18 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
19 |
structure Active: ACTIVE = |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
20 |
struct |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
21 |
|
50498 | 22 |
(* active markup *) |
23 |
||
24 |
fun explicit_id () = |
|
25 |
(case Position.get_id (Position.thread_data ()) of |
|
26 |
SOME id => [(Markup.idN, id)] |
|
27 |
| NONE => []); |
|
28 |
||
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
29 |
fun make_markup name {implicit, properties} = |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
30 |
(name, []) |
50498 | 31 |
|> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup) |
50215 | 32 |
|> Markup.properties properties; |
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
33 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
34 |
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
|
35 |
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
|
36 |
|
50498 | 37 |
|
38 |
(* sendback area *) |
|
39 |
||
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50215
diff
changeset
|
40 |
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
|
41 |
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
|
42 |
|
50498 | 43 |
|
44 |
(* dialog via document content *) |
|
45 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
46 |
val dialogs = Synchronized.var "Active.dialogs" (Inttab.empty: string future Inttab.table); |
50498 | 47 |
|
48 |
fun dialog () = |
|
49 |
let |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
50 |
val i = serial (); |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
51 |
fun abort () = Synchronized.change dialogs (Inttab.delete_safe i); |
50498 | 52 |
val promise = Future.promise abort : string future; |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
53 |
val _ = Synchronized.change dialogs (Inttab.update_new (i, promise)); |
50504 | 54 |
fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result); |
55 |
in (result_markup, promise) end; |
|
50498 | 56 |
|
50505
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50504
diff
changeset
|
57 |
fun dialog_text () = |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50504
diff
changeset
|
58 |
let val (markup, promise) = dialog () |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50504
diff
changeset
|
59 |
in (fn s => Markup.markup (markup s) s, promise) end; |
33c92722cc3d
smarter handling of tracing messages: prover process pauses and enters user dialog;
wenzelm
parents:
50504
diff
changeset
|
60 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
61 |
fun dialog_result i result = |
50498 | 62 |
Synchronized.change_result dialogs |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50498
diff
changeset
|
63 |
(fn tab => (Inttab.lookup tab i, Inttab.delete_safe i tab)) |
50498 | 64 |
|> (fn NONE => () | SOME promise => Future.fulfill promise result); |
65 |
||
50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
66 |
end; |
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
diff
changeset
|
67 |