src/Pure/Isar/session.ML
author haftmann
Thu May 24 08:37:37 2007 +0200 (2007-05-24)
changeset 23086 12320f6e2523
parent 21957 4e44e74dc7e7
child 23898 461cb831d510
permissions -rw-r--r--
tuned Pure/General/name_space.ML
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@11509
    10
  val name: unit -> string
wenzelm@6346
    11
  val welcome: unit -> string
wenzelm@17074
    12
  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool ->
wenzelm@17207
    13
    string list -> string -> string -> bool * string -> string -> int -> bool -> unit
wenzelm@6346
    14
  val finish: unit -> unit
wenzelm@6346
    15
end;
wenzelm@6346
    16
wenzelm@6346
    17
structure Session: SESSION =
wenzelm@6346
    18
struct
wenzelm@6346
    19
wenzelm@6346
    20
wenzelm@6346
    21
(* session state *)
wenzelm@6346
    22
wenzelm@16451
    23
val session = ref ([Context.PureN]: string list);
wenzelm@6346
    24
val session_path = ref ([]: string list);
wenzelm@6346
    25
val session_finished = ref false;
wenzelm@15979
    26
val remote_path = ref (NONE: Url.T option);
wenzelm@9414
    27
wenzelm@9414
    28
wenzelm@9414
    29
(* access path *)
wenzelm@6346
    30
wenzelm@6346
    31
fun path () = ! session_path;
wenzelm@6346
    32
wenzelm@16451
    33
fun str_of [] = Context.PureN
wenzelm@6346
    34
  | str_of elems = space_implode "/" elems;
wenzelm@6346
    35
wenzelm@11509
    36
fun name () = "Isabelle/" ^ str_of (path ());
wenzelm@11509
    37
fun welcome () = "Welcome to " ^ name () ^ " (" ^ 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@18964
    44
    (case duplicates (op =) 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@20664
    53
  if not (member (op =) (! session) parent) 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@16728
    61
  (Output.accumulated_time ();
wenzelm@16728
    62
    ThyInfo.finish ();
wenzelm@6346
    63
    Present.finish ();
wenzelm@21957
    64
    Toplevel.init_state ();
wenzelm@6346
    65
    session_finished := true);
wenzelm@6346
    66
wenzelm@6346
    67
wenzelm@6346
    68
(* use_dir *)
wenzelm@6346
    69
wenzelm@17207
    70
fun get_rpath rpath =
wenzelm@17207
    71
  (if rpath = "" then () else
wenzelm@15979
    72
     if is_some (! remote_path) then
berghofe@7227
    73
       error "Path for remote theory browsing information may only be set once"
berghofe@7227
    74
     else
wenzelm@21858
    75
       remote_path := SOME (Url.explode rpath);
wenzelm@17207
    76
   (! remote_path, rpath <> ""));
wenzelm@17207
    77
wenzelm@17207
    78
fun dumping (_, "") = NONE
wenzelm@21858
    79
  | dumping (cp, path) = SOME (cp, Path.explode path);
berghofe@7236
    80
wenzelm@17074
    81
fun use_dir root build modes reset info doc doc_graph doc_versions
wenzelm@17207
    82
    parent name dump rpath level verbose =
wenzelm@11543
    83
  Library.setmp print_mode (modes @ ! print_mode)
wenzelm@17074
    84
    (Library.setmp Proofterm.proofs level (fn () =>
wenzelm@11543
    85
      (init reset parent name;
wenzelm@17074
    86
       Present.init build info doc doc_graph doc_versions (path ()) name
wenzelm@17207
    87
         (dumping dump) (get_rpath rpath) verbose;
wenzelm@16715
    88
       ThyInfo.time_use root;
wenzelm@17074
    89
       finish ()))) ()
wenzelm@18683
    90
  handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
wenzelm@6346
    91
wenzelm@6346
    92
wenzelm@6346
    93
end;