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;
     1 (*  Title:      Pure/PIDE/session.ML
     2     Author:     Makarius
     3 
     4 Prover session: persistent state of logic image.
     5 *)
     6 
     7 signature SESSION =
     8 sig
     9   val name: unit -> string
    10   val welcome: unit -> string
    11   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
    12     (Path.T * Path.T) list -> string -> string * string -> bool -> unit
    13   val finish: unit -> unit
    14   val protocol_handler: string -> unit
    15   val init_protocol_handlers: unit -> unit
    16 end;
    17 
    18 structure Session: SESSION =
    19 struct
    20 
    21 (** session identification -- not thread-safe **)
    22 
    23 val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
    24 val session_finished = Unsynchronized.ref false;
    25 
    26 fun name () = "Isabelle/" ^ #name (! session);
    27 
    28 fun welcome () =
    29   if Distribution.is_identified then
    30     "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
    31   else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
    32 
    33 
    34 (* init *)
    35 
    36 fun init build info info_path doc doc_graph doc_output doc_variants doc_files
    37     parent (chapter, name) verbose =
    38   if #name (! session) <> parent orelse not (! session_finished) then
    39     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    40   else
    41     let
    42       val _ = session := {chapter = chapter, name = name};
    43       val _ = session_finished := false;
    44     in
    45       Present.init build info info_path (if doc = "false" then "" else doc)
    46         doc_graph doc_output doc_variants doc_files (chapter, name)
    47         verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
    48     end;
    49 
    50 
    51 (* finish *)
    52 
    53 fun finish () =
    54  (Execution.shutdown ();
    55   Thy_Info.finish ();
    56   Present.finish ();
    57   Future.shutdown ();
    58   Event_Timer.shutdown ();
    59   Future.shutdown ();
    60   session_finished := true);
    61 
    62 
    63 
    64 (** protocol handlers **)
    65 
    66 val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
    67 
    68 fun protocol_handler name =
    69   Synchronized.change protocol_handlers (fn handlers =>
    70    (Output.try_protocol_message (Markup.protocol_handler name) [];
    71     if not (member (op =) handlers name) then ()
    72     else warning ("Redefining protocol handler: " ^ quote name);
    73     update (op =) name handlers));
    74 
    75 fun init_protocol_handlers () =
    76   Synchronized.value protocol_handlers
    77   |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
    78 
    79 end;