src/Pure/PIDE/session.ML
author wenzelm
Wed Dec 03 14:04:38 2014 +0100 (2014-12-03 ago)
changeset 59083 88b0b1f28adc
parent 58928 23d0ffd48006
child 59086 94b2690ad494
permissions -rw-r--r--
tuned signature;
wenzelm@56210
     1
(*  Title:      Pure/PIDE/session.ML
wenzelm@52052
     2
    Author:     Makarius
wenzelm@6346
     3
wenzelm@56210
     4
Prover session: persistent state of logic image.
wenzelm@6346
     5
*)
wenzelm@6346
     6
wenzelm@6346
     7
signature SESSION =
wenzelm@6346
     8
sig
wenzelm@11509
     9
  val name: unit -> string
wenzelm@6346
    10
  val welcome: unit -> string
wenzelm@51399
    11
  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
wenzelm@56533
    12
    (Path.T * Path.T) list -> string -> string * string -> bool -> unit
wenzelm@48457
    13
  val finish: unit -> unit
wenzelm@52111
    14
  val protocol_handler: string -> unit
wenzelm@52111
    15
  val init_protocol_handlers: unit -> unit
wenzelm@6346
    16
end;
wenzelm@6346
    17
wenzelm@6346
    18
structure Session: SESSION =
wenzelm@6346
    19
struct
wenzelm@6346
    20
wenzelm@52111
    21
(** session identification -- not thread-safe **)
wenzelm@6346
    22
wenzelm@51399
    23
val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
wenzelm@32738
    24
val session_finished = Unsynchronized.ref false;
wenzelm@48542
    25
wenzelm@51399
    26
fun name () = "Isabelle/" ^ #name (! session);
wenzelm@30173
    27
wenzelm@26109
    28
fun welcome () =
wenzelm@57649
    29
  if Distribution.is_identified then
wenzelm@26134
    30
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
wenzelm@48990
    31
  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
wenzelm@6346
    32
wenzelm@6346
    33
wenzelm@51399
    34
(* init *)
wenzelm@9414
    35
wenzelm@56533
    36
fun init build info info_path doc doc_graph doc_output doc_variants doc_files
wenzelm@56530
    37
    parent (chapter, name) verbose =
wenzelm@51399
    38
  if #name (! session) <> parent orelse not (! session_finished) then
wenzelm@6346
    39
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
wenzelm@51399
    40
  else
wenzelm@51399
    41
    let
wenzelm@51399
    42
      val _ = session := {chapter = chapter, name = name};
wenzelm@51399
    43
      val _ = session_finished := false;
wenzelm@51399
    44
    in
wenzelm@51399
    45
      Present.init build info info_path (if doc = "false" then "" else doc)
wenzelm@56533
    46
        doc_graph doc_output doc_variants doc_files (chapter, name)
wenzelm@56530
    47
        verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
wenzelm@51399
    48
    end;
wenzelm@6346
    49
wenzelm@6346
    50
wenzelm@6346
    51
(* finish *)
wenzelm@6346
    52
wenzelm@6346
    53
fun finish () =
wenzelm@53192
    54
 (Execution.shutdown ();
wenzelm@49911
    55
  Thy_Info.finish ();
wenzelm@49911
    56
  Present.finish ();
wenzelm@50430
    57
  Future.shutdown ();
wenzelm@52050
    58
  Event_Timer.shutdown ();
wenzelm@55386
    59
  Future.shutdown ();
wenzelm@49911
    60
  session_finished := true);
wenzelm@6346
    61
wenzelm@52111
    62
wenzelm@56210
    63
wenzelm@52111
    64
(** protocol handlers **)
wenzelm@52111
    65
wenzelm@52111
    66
val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
wenzelm@52111
    67
wenzelm@52111
    68
fun protocol_handler name =
wenzelm@52111
    69
  Synchronized.change protocol_handlers (fn handlers =>
wenzelm@56333
    70
   (Output.try_protocol_message (Markup.protocol_handler name) [];
wenzelm@52111
    71
    if not (member (op =) handlers name) then ()
wenzelm@52111
    72
    else warning ("Redefining protocol handler: " ^ quote name);
wenzelm@52111
    73
    update (op =) name handlers));
wenzelm@52111
    74
wenzelm@52111
    75
fun init_protocol_handlers () =
wenzelm@52111
    76
  Synchronized.value protocol_handlers
wenzelm@56333
    77
  |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
wenzelm@52111
    78
wenzelm@6346
    79
end;