src/Pure/System/session.ML
author wenzelm
Wed May 22 14:10:45 2013 +0200 (2013-05-22 ago)
changeset 52111 1fd184eaa310
parent 52083 f852d08376f9
child 52440 67f57dc115b9
permissions -rw-r--r--
explicit management of Session.Protocol_Handlers, with protocol state and functions;
more self-contained ML/Scala module Invoke_Scala;
     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   Keyword.status ();
    58   Outer_Syntax.check_syntax ();
    59   Future.shutdown ();
    60   Event_Timer.shutdown ();
    61   session_finished := true);
    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;