src/Pure/Isar/session.ML
author wenzelm
Sun Jul 23 12:08:07 2000 +0200 (2000-07-23)
changeset 9414 1463576f3968
parent 8807 0046be1769f9
child 10571 fdde440a9033
permissions -rw-r--r--
disallow duplicates in session identifiers;
wenzelm@6346
     1
(*  Title:      Pure/Isar/session.ML
wenzelm@6346
     2
    ID:         $Id$
wenzelm@6346
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6346
     5
wenzelm@6346
     6
Session management -- maintain state of logic images.
wenzelm@6346
     7
*)
wenzelm@6346
     8
wenzelm@6346
     9
signature SESSION =
wenzelm@6346
    10
sig
wenzelm@6346
    11
  val welcome: unit -> string
wenzelm@8196
    12
  val use_dir: bool -> bool -> string -> string -> string -> string -> string -> unit
wenzelm@6346
    13
  val finish: unit -> unit
wenzelm@6346
    14
end;
wenzelm@6346
    15
wenzelm@6346
    16
structure Session: SESSION =
wenzelm@6346
    17
struct
wenzelm@6346
    18
wenzelm@6346
    19
wenzelm@6346
    20
(* session state *)
wenzelm@6346
    21
wenzelm@6346
    22
val pure = "Pure";
wenzelm@6346
    23
wenzelm@6346
    24
val session = ref ([pure]: string list);
wenzelm@6346
    25
val session_path = ref ([]: string list);
wenzelm@6346
    26
val session_finished = ref false;
wenzelm@9414
    27
val rpath = ref (None: Url.T option);
wenzelm@9414
    28
wenzelm@9414
    29
wenzelm@9414
    30
(* access path *)
wenzelm@6346
    31
wenzelm@6346
    32
fun path () = ! session_path;
wenzelm@6346
    33
wenzelm@6346
    34
fun str_of [] = "Pure"
wenzelm@6346
    35
  | str_of elems = space_implode "/" elems;
wenzelm@6346
    36
wenzelm@6346
    37
fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
wenzelm@6346
    38
wenzelm@6346
    39
wenzelm@9414
    40
(* add_path *)
wenzelm@9414
    41
wenzelm@9414
    42
fun add_path reset s =
wenzelm@9414
    43
  let val sess = ! session @ [s] in
wenzelm@9414
    44
    (case Library.duplicates sess of
wenzelm@9414
    45
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
wenzelm@9414
    46
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
wenzelm@9414
    47
  end;
wenzelm@9414
    48
wenzelm@9414
    49
wenzelm@6346
    50
(* init *)
wenzelm@6346
    51
wenzelm@6346
    52
fun init reset parent name =
wenzelm@6346
    53
  if not (parent mem_string (! session)) orelse not (! session_finished) then
wenzelm@6346
    54
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
wenzelm@6346
    55
  else (add_path reset name; session_finished := false);
wenzelm@6346
    56
wenzelm@6346
    57
wenzelm@6346
    58
(* finish *)
wenzelm@6346
    59
wenzelm@6346
    60
fun finish () =
wenzelm@6663
    61
  (ThyInfo.finish ();
wenzelm@6346
    62
    Present.finish ();
wenzelm@6346
    63
    session_finished := true);
wenzelm@6346
    64
wenzelm@6346
    65
wenzelm@6346
    66
(* use_dir *)
wenzelm@6346
    67
wenzelm@6346
    68
val root_file = ThyLoad.ml_path "ROOT";
wenzelm@6346
    69
berghofe@7236
    70
fun get_rpath rpath_str =
berghofe@7236
    71
  (if rpath_str = "" then () else
berghofe@7227
    72
     if is_some (!rpath) then
berghofe@7227
    73
       error "Path for remote theory browsing information may only be set once"
berghofe@7227
    74
     else
berghofe@7227
    75
       rpath := Some (Url.unpack rpath_str);
berghofe@7236
    76
   (!rpath, rpath_str <> ""));
berghofe@7236
    77
wenzelm@8196
    78
fun use_dir reset info doc parent name dump rpath_str =
berghofe@7236
    79
  (init reset parent name;
wenzelm@8196
    80
   Present.init info doc (path ()) name
wenzelm@8196
    81
     (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
berghofe@7227
    82
   File.symbol_use root_file;
berghofe@7227
    83
   finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
wenzelm@6346
    84
wenzelm@6346
    85
wenzelm@6346
    86
end;