src/Pure/Isar/session.ML
changeset 11509 d54301357129
parent 10937 5651e0636e38
child 11527 4db3876f1224
equal deleted inserted replaced
11508:168dbdaedb71 11509:d54301357129
     6 Session management -- maintain state of logic images.
     6 Session management -- maintain state of logic images.
     7 *)
     7 *)
     8 
     8 
     9 signature SESSION =
     9 signature SESSION =
    10 sig
    10 sig
       
    11   val name: unit -> string
    11   val welcome: unit -> string
    12   val welcome: unit -> string
    12   val use_dir:
    13   val use_dir:
    13     string list -> bool -> bool -> string -> string -> string -> string -> string -> unit
    14     string list -> bool -> bool -> string -> string -> string -> string -> string -> unit
    14   val finish: unit -> unit
    15   val finish: unit -> unit
    15 end;
    16 end;
    33 fun path () = ! session_path;
    34 fun path () = ! session_path;
    34 
    35 
    35 fun str_of [] = pure
    36 fun str_of [] = pure
    36   | str_of elems = space_implode "/" elems;
    37   | str_of elems = space_implode "/" elems;
    37 
    38 
    38 fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
    39 fun name () = "Isabelle/" ^ str_of (path ());
       
    40 fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";
    39 
    41 
    40 
    42 
    41 (* add_path *)
    43 (* add_path *)
    42 
    44 
    43 fun add_path reset s =
    45 fun add_path reset s =