src/Pure/Isar/session.ML
author wenzelm
Thu, 11 Mar 1999 12:32:40 +0100
changeset 6346 643a1bd31a91
child 6641 254ab03bd082
permissions -rw-r--r--
moved Thy/session.ML to Isar/session.ML;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/session.ML
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     4
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     5
Session management -- maintain state of logic images.
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     6
*)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     7
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     8
signature SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     9
sig
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    10
  val welcome: unit -> string
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    11
  val use_dir: bool -> bool -> string -> string -> unit
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    12
  val finish: unit -> unit
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    13
end;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    14
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    15
structure Session: SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    16
struct
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    17
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    18
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    19
(* session state *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    20
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    21
val pure = "Pure";
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    22
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    23
val session = ref ([pure]: string list);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    24
val session_path = ref ([]: string list);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    25
val session_finished = ref false;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    26
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    27
fun path () = ! session_path;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    28
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    29
fun add_path reset s =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    30
  (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    31
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    32
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    33
(* diagnostics *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    34
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    35
fun str_of [] = "Pure"
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    36
  | str_of elems = space_implode "/" elems;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    37
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    38
fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    39
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    40
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    41
(* init *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    42
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    43
fun init reset parent name =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    44
  if not (parent mem_string (! session)) orelse not (! session_finished) then
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    45
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    46
  else (add_path reset name; session_finished := false);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    47
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    48
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    49
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    50
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    51
fun finish () =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    52
  (ThyInfo.finalize_all ();
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    53
    Present.finish ();
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    54
    session_finished := true);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    55
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    56
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    57
(* use_dir *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    58
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    59
val root_file = ThyLoad.ml_path "ROOT";
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    60
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    61
fun use_dir reset info parent name =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    62
  (init reset parent name;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    63
    Present.init info (path ()) name;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    64
    Symbol.use root_file;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    65
    finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    66
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    67
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    68
end;