src/Pure/PIDE/active.ML
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 50505 33c92722cc3d
child 52697 6fb98a20c349
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    22
(* active markup *)
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    23
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    24
fun explicit_id () =
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    25
  (case Position.get_id (Position.thread_data ()) of
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    26
    SOME id => [(Markup.idN, id)]
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    27
  | NONE => []);
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    31
  |> not implicit ? (fn markup => Markup.properties (explicit_id ()) markup)
50215
97959912840a more general sendback properties;
wenzelm
parents: 50212
diff changeset
    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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    37
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    38
(* sendback area *)
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    43
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    44
(* dialog via document content *)
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    47
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    48
fun dialog () =
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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
wenzelm
parents: 50500
diff changeset
    54
    fun result_markup result = Markup.properties (explicit_id ()) (Markup.dialog i result);
wenzelm
parents: 50500
diff changeset
    55
  in (result_markup, promise) end;
50498
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    64
  |> (fn NONE => () | SOME promise => Future.fulfill promise result);
6647ba2775c1 support dialog via document content;
wenzelm
parents: 50450
diff changeset
    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