src/Pure/PIDE/session.ML
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
parent 62944 3ee643c5ed00
permissions -rw-r--r--
clarified modules;
     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 get_name: unit -> string
    10   val welcome: unit -> string
    11   val get_keywords: unit -> Keyword.keywords
    12   val init: HTML.symbols -> bool -> bool -> Path.T -> string -> string -> (string * string) list ->
    13     (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
    14   val shutdown: unit -> unit
    15   val finish: unit -> unit
    16   val protocol_handler: string -> unit
    17   val init_protocol_handlers: unit -> unit
    18 end;
    19 
    20 structure Session: SESSION =
    21 struct
    22 
    23 (** persistent session information **)
    24 
    25 val session = Synchronized.var "Session.session" ({chapter = "", name = ""}, true);
    26 
    27 fun get_name () = #name (#1 (Synchronized.value session));
    28 
    29 fun description () = "Isabelle/" ^ get_name ();
    30 
    31 fun welcome () =
    32   if Distribution.is_identified then
    33     "Welcome to " ^ description () ^ " (" ^ Distribution.version ^ ")"
    34   else "Unofficial version of " ^ description () ^ " (" ^ Distribution.version ^ ")";
    35 
    36 
    37 (* base syntax *)
    38 
    39 val keywords = Synchronized.var "Session.keywords" Keyword.empty_keywords;
    40 
    41 fun get_keywords () = Synchronized.value keywords;
    42 
    43 fun update_keywords () =
    44   Synchronized.change keywords
    45     (K (fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory)
    46       (Thy_Info.get_names ()) Keyword.empty_keywords));
    47 
    48 
    49 (* init *)
    50 
    51 fun init symbols build info info_path doc doc_output doc_variants doc_files graph_file
    52     parent (chapter, name) verbose =
    53   (Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
    54     if parent_name <> parent orelse not parent_finished then
    55       error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    56     else ({chapter = chapter, name = name}, false));
    57     Present.init symbols build info info_path (if doc = "false" then "" else doc)
    58       doc_output doc_variants doc_files graph_file (chapter, name) verbose);
    59 
    60 
    61 (* finish *)
    62 
    63 fun shutdown () =
    64  (Execution.shutdown ();
    65   Event_Timer.shutdown ();
    66   Future.shutdown ());
    67 
    68 fun finish () =
    69  (shutdown ();
    70   Thy_Info.finish ();
    71   Present.finish ();
    72   shutdown ();
    73   update_keywords ();
    74   Synchronized.change session (apsnd (K true)));
    75 
    76 
    77 
    78 (** protocol handlers **)
    79 
    80 val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
    81 
    82 fun protocol_handler name =
    83   if Thread_Data.is_virtual then ()
    84   else
    85     Synchronized.change protocol_handlers (fn handlers =>
    86      (Output.try_protocol_message (Markup.protocol_handler name) [];
    87       if not (member (op =) handlers name) then ()
    88       else warning ("Redefining protocol handler: " ^ quote name);
    89       update (op =) name handlers));
    90 
    91 fun init_protocol_handlers () =
    92   if Thread_Data.is_virtual then ()
    93   else
    94     Synchronized.value protocol_handlers
    95     |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) []);
    96 
    97 end;