src/Pure/Isar/session.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 20664 ffbc5a57191a
child 21858 05f57309170c
permissions -rw-r--r--
Attrib.internal: morphism;
     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 ->
    13     string list -> string -> string -> bool * 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 session = ref ([Context.PureN]: string list);
    24 val session_path = ref ([]: string list);
    25 val session_finished = ref false;
    26 val remote_path = ref (NONE: Url.T option);
    27 
    28 
    29 (* access path *)
    30 
    31 fun path () = ! session_path;
    32 
    33 fun str_of [] = Context.PureN
    34   | str_of elems = space_implode "/" elems;
    35 
    36 fun name () = "Isabelle/" ^ str_of (path ());
    37 fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";
    38 
    39 
    40 (* add_path *)
    41 
    42 fun add_path reset s =
    43   let val sess = ! session @ [s] in
    44     (case duplicates (op =) sess of
    45       [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
    46     | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
    47   end;
    48 
    49 
    50 (* init *)
    51 
    52 fun init reset parent name =
    53   if not (member (op =) (! session) parent) orelse not (! session_finished) then
    54     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    55   else (add_path reset name; session_finished := false);
    56 
    57 
    58 (* finish *)
    59 
    60 fun finish () =
    61   (Output.accumulated_time ();
    62     ThyInfo.finish ();
    63     Present.finish ();
    64     session_finished := true);
    65 
    66 
    67 (* use_dir *)
    68 
    69 fun get_rpath rpath =
    70   (if rpath = "" then () else
    71      if is_some (! remote_path) then
    72        error "Path for remote theory browsing information may only be set once"
    73      else
    74        remote_path := SOME (Url.unpack rpath);
    75    (! remote_path, rpath <> ""));
    76 
    77 fun dumping (_, "") = NONE
    78   | dumping (cp, path) = SOME (cp, Path.unpack path);
    79 
    80 fun use_dir root build modes reset info doc doc_graph doc_versions
    81     parent name dump rpath 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 doc_versions (path ()) name
    86          (dumping dump) (get_rpath rpath) verbose;
    87        ThyInfo.time_use root;
    88        finish ()))) ()
    89   handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
    90 
    91 
    92 end;