src/Pure/Isar/session.ML
author wenzelm
Fri Nov 09 00:17:09 2001 +0100 (2001-11-09)
changeset 12120 a08c61932501
parent 11910 8b8923bfc259
child 14981 e73f8140af78
permissions -rw-r--r--
File.use;
     1 (*  Title:      Pure/Isar/session.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Session management -- maintain state of logic images.
     7 *)
     8 
     9 signature SESSION =
    10 sig
    11   val name: unit -> string
    12   val welcome: unit -> string
    13   val use_dir: bool -> string list -> bool -> bool -> string -> bool -> string
    14     -> string -> string -> string -> int -> bool -> unit
    15   val finish: unit -> unit
    16 end;
    17 
    18 structure Session: SESSION =
    19 struct
    20 
    21 
    22 (* session state *)
    23 
    24 val pure = "Pure";
    25 
    26 val session = ref ([pure]: string list);
    27 val session_path = ref ([]: string list);
    28 val session_finished = ref false;
    29 val rpath = ref (None: Url.T option);
    30 
    31 
    32 (* access path *)
    33 
    34 fun path () = ! session_path;
    35 
    36 fun str_of [] = pure
    37   | str_of elems = space_implode "/" elems;
    38 
    39 fun name () = "Isabelle/" ^ str_of (path ());
    40 fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";
    41 
    42 
    43 (* add_path *)
    44 
    45 fun add_path reset s =
    46   let val sess = ! session @ [s] in
    47     (case Library.duplicates sess of
    48       [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
    49     | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
    50   end;
    51 
    52 
    53 (* init *)
    54 
    55 fun init reset parent name =
    56   if not (parent mem_string (! session)) orelse not (! session_finished) then
    57     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    58   else (add_path reset name; session_finished := false);
    59 
    60 
    61 (* finish *)
    62 
    63 fun finish () =
    64   (ThyInfo.finish ();
    65     Present.finish ();
    66     session_finished := true);
    67 
    68 
    69 (* use_dir *)
    70 
    71 val root_file = ThyLoad.ml_path "ROOT";
    72 
    73 fun get_rpath rpath_str =
    74   (if rpath_str = "" then () else
    75      if is_some (!rpath) then
    76        error "Path for remote theory browsing information may only be set once"
    77      else
    78        rpath := Some (Url.unpack rpath_str);
    79    (!rpath, rpath_str <> ""));
    80 
    81 fun use_dir build modes reset info doc doc_graph parent name dump rpath_str level verbose =
    82   Library.setmp print_mode (modes @ ! print_mode)
    83     (Library.setmp Proofterm.proofs level (fn () =>
    84       (init reset parent name;
    85        Present.init build info doc doc_graph (path ()) name
    86          (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
    87        File.use root_file;
    88        finish ()))) ()
    89   handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    90 
    91 
    92 end;