src/Pure/Isar/session.ML
author berghofe
Tue Aug 17 14:00:30 1999 +0200 (1999-08-17)
changeset 7227 a8e86b8e6fd1
parent 6663 3f87294c8704
child 7236 e077484d50d8
permissions -rw-r--r--
Path for remote theory browsing information is now stored in referece variable rpath.
wenzelm@6346
     1
(*  Title:      Pure/Isar/session.ML
wenzelm@6346
     2
    ID:         $Id$
wenzelm@6346
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6346
     4
wenzelm@6346
     5
Session management -- maintain state of logic images.
wenzelm@6346
     6
*)
wenzelm@6346
     7
wenzelm@6346
     8
signature SESSION =
wenzelm@6346
     9
sig
wenzelm@6346
    10
  val welcome: unit -> string
berghofe@6651
    11
  val use_dir: bool -> bool -> string -> string -> string -> unit
wenzelm@6346
    12
  val finish: unit -> unit
wenzelm@6346
    13
end;
wenzelm@6346
    14
wenzelm@6346
    15
structure Session: SESSION =
wenzelm@6346
    16
struct
wenzelm@6346
    17
wenzelm@6346
    18
wenzelm@6346
    19
(* session state *)
wenzelm@6346
    20
wenzelm@6346
    21
val pure = "Pure";
wenzelm@6346
    22
wenzelm@6346
    23
val session = ref ([pure]: string list);
wenzelm@6346
    24
val session_path = ref ([]: string list);
wenzelm@6346
    25
val session_finished = ref false;
wenzelm@6346
    26
wenzelm@6346
    27
fun path () = ! session_path;
wenzelm@6346
    28
wenzelm@6346
    29
fun add_path reset s =
wenzelm@6346
    30
  (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
wenzelm@6346
    31
wenzelm@6346
    32
wenzelm@6346
    33
(* diagnostics *)
wenzelm@6346
    34
wenzelm@6346
    35
fun str_of [] = "Pure"
wenzelm@6346
    36
  | str_of elems = space_implode "/" elems;
wenzelm@6346
    37
wenzelm@6346
    38
fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
wenzelm@6346
    39
wenzelm@6346
    40
wenzelm@6346
    41
(* init *)
wenzelm@6346
    42
wenzelm@6346
    43
fun init reset parent name =
wenzelm@6346
    44
  if not (parent mem_string (! session)) orelse not (! session_finished) then
wenzelm@6346
    45
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
wenzelm@6346
    46
  else (add_path reset name; session_finished := false);
wenzelm@6346
    47
wenzelm@6346
    48
wenzelm@6346
    49
(* finish *)
wenzelm@6346
    50
wenzelm@6346
    51
fun finish () =
wenzelm@6663
    52
  (ThyInfo.finish ();
wenzelm@6346
    53
    Present.finish ();
wenzelm@6346
    54
    session_finished := true);
wenzelm@6346
    55
wenzelm@6346
    56
wenzelm@6346
    57
(* use_dir *)
wenzelm@6346
    58
wenzelm@6346
    59
val root_file = ThyLoad.ml_path "ROOT";
wenzelm@6346
    60
berghofe@7227
    61
val rpath = ref (None : Url.T option);
berghofe@7227
    62
berghofe@7227
    63
fun use_dir reset info parent name rpath_str =
wenzelm@6346
    64
  (init reset parent name;
berghofe@7227
    65
   if rpath_str = "" then () else
berghofe@7227
    66
     if is_some (!rpath) then
berghofe@7227
    67
       error "Path for remote theory browsing information may only be set once"
berghofe@7227
    68
     else
berghofe@7227
    69
       rpath := Some (Url.unpack rpath_str);
berghofe@7227
    70
   Present.init info (path ()) name (!rpath);
berghofe@7227
    71
   File.symbol_use root_file;
berghofe@7227
    72
   finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
wenzelm@6346
    73
wenzelm@6346
    74
wenzelm@6346
    75
end;