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