src/Pure/System/session.ML
author wenzelm
Mon Jul 15 10:25:35 2013 +0200 (2013-07-15 ago)
changeset 52655 3b2b1ef13979
parent 52440 67f57dc115b9
child 53192 04df1d236e1c
permissions -rw-r--r--
more careful termination of removed execs, leaving running execs undisturbed;
     1 (*  Title:      Pure/System/session.ML
     2     Author:     Makarius
     3 
     4 Session management -- internal state of logic images.
     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     string -> string * string -> bool * 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_official 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
    37     parent (chapter, name) doc_dump 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 (chapter, name)
    47         doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
    48     end;
    49 
    50 
    51 (* finish *)
    52 
    53 fun finish () =
    54  (Goal.shutdown_futures ();
    55   Thy_Info.finish ();
    56   Present.finish ();
    57   Outer_Syntax.check_syntax ();
    58   Future.shutdown ();
    59   Event_Timer.shutdown ();
    60   session_finished := true);
    61 
    62 
    63 (** protocol handlers **)
    64 
    65 val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
    66 
    67 fun protocol_handler name =
    68   Synchronized.change protocol_handlers (fn handlers =>
    69    (Output.try_protocol_message (Markup.protocol_handler name) "";
    70     if not (member (op =) handlers name) then ()
    71     else warning ("Redefining protocol handler: " ^ quote name);
    72     update (op =) name handlers));
    73 
    74 fun init_protocol_handlers () =
    75   Synchronized.value protocol_handlers
    76   |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
    77 
    78 end;