src/Pure/Isar/session.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7236 e077484d50d8
child 7730 ba9e55b92998
permissions -rw-r--r--
removed extra shyps error;
     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 -> 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 val rpath = ref (None : Url.T option);
    27 
    28 fun path () = ! session_path;
    29 
    30 fun add_path reset s =
    31   (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
    32 
    33 
    34 (* diagnostics *)
    35 
    36 fun str_of [] = "Pure"
    37   | str_of elems = space_implode "/" elems;
    38 
    39 fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
    40 
    41 
    42 (* init *)
    43 
    44 fun init reset parent name =
    45   if not (parent mem_string (! session)) orelse not (! session_finished) then
    46     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    47   else (add_path reset name; session_finished := false);
    48 
    49 
    50 (* finish *)
    51 
    52 fun finish () =
    53   (ThyInfo.finish ();
    54     Present.finish ();
    55     session_finished := true);
    56 
    57 
    58 (* use_dir *)
    59 
    60 val root_file = ThyLoad.ml_path "ROOT";
    61 
    62 fun get_rpath rpath_str =
    63   (if rpath_str = "" then () else
    64      if is_some (!rpath) then
    65        error "Path for remote theory browsing information may only be set once"
    66      else
    67        rpath := Some (Url.unpack rpath_str);
    68    (!rpath, rpath_str <> ""));
    69 
    70 fun use_dir reset info parent name rpath_str =
    71   (init reset parent name;
    72    Present.init info (path ()) name (get_rpath rpath_str);
    73    File.symbol_use root_file;
    74    finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    75 
    76 
    77 end;