src/Pure/Isar/session.ML
author wenzelm
Fri Mar 19 11:24:00 1999 +0100 (1999-03-19)
changeset 6404 2daaf2943c79
parent 6346 643a1bd31a91
child 6641 254ab03bd082
permissions -rw-r--r--
common qed and end of proofs;
     1 (*  Title:      Pure/Isar/session.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Session management -- maintain state of logic images.
     6 *)
     7 
     8 signature SESSION =
     9 sig
    10   val welcome: unit -> string
    11   val use_dir: bool -> bool -> string -> string -> unit
    12   val finish: unit -> unit
    13 end;
    14 
    15 structure Session: SESSION =
    16 struct
    17 
    18 
    19 (* session state *)
    20 
    21 val pure = "Pure";
    22 
    23 val session = ref ([pure]: string list);
    24 val session_path = ref ([]: string list);
    25 val session_finished = ref false;
    26 
    27 fun path () = ! session_path;
    28 
    29 fun add_path reset s =
    30   (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
    31 
    32 
    33 (* diagnostics *)
    34 
    35 fun str_of [] = "Pure"
    36   | str_of elems = space_implode "/" elems;
    37 
    38 fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
    39 
    40 
    41 (* init *)
    42 
    43 fun init reset parent name =
    44   if not (parent mem_string (! session)) orelse not (! session_finished) then
    45     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    46   else (add_path reset name; session_finished := false);
    47 
    48 
    49 (* finish *)
    50 
    51 fun finish () =
    52   (ThyInfo.finalize_all ();
    53     Present.finish ();
    54     session_finished := true);
    55 
    56 
    57 (* use_dir *)
    58 
    59 val root_file = ThyLoad.ml_path "ROOT";
    60 
    61 fun use_dir reset info parent name =
    62   (init reset parent name;
    63     Present.init info (path ()) name;
    64     Symbol.use root_file;
    65     finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    66 
    67 
    68 end;