src/Pure/Isar/session.ML
author wenzelm
Fri Jun 17 18:33:36 2005 +0200 (2005-06-17)
changeset 16451 c9f1fc144132
parent 15979 c81578ac2d31
child 16715 ecca9fd2754f
permissions -rw-r--r--
Context.PureN;
     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 -> 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 Library.duplicates 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 (parent mem_string (! session)) 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   (ThyInfo.finish ();
    62     Present.finish ();
    63     session_finished := true);
    64 
    65 
    66 (* use_dir *)
    67 
    68 fun get_rpath rpath_str =
    69   (if rpath_str = "" then () else
    70      if is_some (! remote_path) then
    71        error "Path for remote theory browsing information may only be set once"
    72      else
    73        remote_path := SOME (Url.unpack rpath_str);
    74    (! remote_path, rpath_str <> ""));
    75 
    76 fun use_dir root build modes reset info doc doc_graph parent name dump rpath_str level verbose hide =
    77   Library.setmp print_mode (modes @ ! print_mode)
    78     (Library.setmp Proofterm.proofs level (Library.setmp IsarOutput.hide_commands hide (fn () =>
    79       (init reset parent name;
    80        Present.init build info doc doc_graph (path ()) name
    81          (if dump = "" then NONE else SOME (Path.unpack dump)) (get_rpath rpath_str) verbose;
    82        File.use (Path.basic root);
    83        finish ())))) ()
    84   handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    85 
    86 
    87 end;