src/Pure/Isar/session.ML
author webertj
Thu Oct 28 19:40:22 2004 +0200 (2004-10-28)
changeset 15269 f856f4f3258f
parent 14981 e73f8140af78
child 15433 a2cbdf16832e
permissions -rw-r--r--
isatool usedir: ML root file can now be specified (previously hard-coded as ROOT.ML)
     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: string -> 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 (*
    71 val root_file = ThyLoad.ml_path "ROOT";
    72 *)
    73 
    74 fun get_rpath rpath_str =
    75   (if rpath_str = "" then () else
    76      if is_some (!rpath) then
    77        error "Path for remote theory browsing information may only be set once"
    78      else
    79        rpath := Some (Url.unpack rpath_str);
    80    (!rpath, rpath_str <> ""));
    81 
    82 fun use_dir root_file build modes reset info doc doc_graph parent name dump rpath_str level verbose =
    83   Library.setmp print_mode (modes @ ! print_mode)
    84     (Library.setmp Proofterm.proofs level (fn () =>
    85       (init reset parent name;
    86        Present.init build info doc doc_graph (path ()) name
    87          (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str) verbose;
    88        File.use (Path.basic root_file);
    89        finish ()))) ()
    90   handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    91 
    92 
    93 end;