src/Pure/Isar/session.ML
author wenzelm
Thu, 18 Jan 2001 20:40:47 +0100
changeset 10937 5651e0636e38
parent 10571 fdde440a9033
child 11509 d54301357129
permissions -rw-r--r--
tuned;
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
8807
wenzelm
parents: 8196
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     5
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     6
Session management -- maintain state of logic images.
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     9
signature SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    10
sig
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    11
  val welcome: unit -> string
10571
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    12
  val use_dir:
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    13
    string list -> bool -> bool -> string -> string -> string -> string -> string -> unit
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    14
  val finish: unit -> unit
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    15
end;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    16
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    17
structure Session: SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    18
struct
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    19
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
(* session state *)
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 pure = "Pure";
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    24
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    25
val session = ref ([pure]: string list);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    26
val session_path = ref ([]: string list);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    27
val session_finished = ref false;
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    28
val rpath = ref (None: Url.T option);
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    29
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    30
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    31
(* access path *)
6346
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
fun path () = ! session_path;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    34
10937
wenzelm
parents: 10571
diff changeset
    35
fun str_of [] = pure
6346
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
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    41
(* add_path *)
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    42
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    43
fun add_path reset s =
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    44
  let val sess = ! session @ [s] in
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    45
    (case Library.duplicates sess of
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    46
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    47
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    48
  end;
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    49
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    50
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    51
(* init *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    52
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    53
fun init reset parent name =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    54
  if not (parent mem_string (! session)) orelse not (! session_finished) then
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    55
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    56
  else (add_path reset name; session_finished := false);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    57
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
(* finish *)
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 finish () =
6663
3f87294c8704 ThyInfo.finalize_all renamed to ThyInfo.finish;
wenzelm
parents: 6651
diff changeset
    62
  (ThyInfo.finish ();
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    63
    Present.finish ();
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    64
    session_finished := true);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    65
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
(* use_dir *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    68
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    69
val root_file = ThyLoad.ml_path "ROOT";
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    70
7236
e077484d50d8 Better handling of path for remote theory browsing information.
berghofe
parents: 7227
diff changeset
    71
fun get_rpath rpath_str =
e077484d50d8 Better handling of path for remote theory browsing information.
berghofe
parents: 7227
diff changeset
    72
  (if rpath_str = "" then () else
7227
a8e86b8e6fd1 Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents: 6663
diff changeset
    73
     if is_some (!rpath) then
a8e86b8e6fd1 Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents: 6663
diff changeset
    74
       error "Path for remote theory browsing information may only be set once"
a8e86b8e6fd1 Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents: 6663
diff changeset
    75
     else
a8e86b8e6fd1 Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents: 6663
diff changeset
    76
       rpath := Some (Url.unpack rpath_str);
7236
e077484d50d8 Better handling of path for remote theory browsing information.
berghofe
parents: 7227
diff changeset
    77
   (!rpath, rpath_str <> ""));
e077484d50d8 Better handling of path for remote theory browsing information.
berghofe
parents: 7227
diff changeset
    78
10571
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    79
fun use_dir modes reset info doc parent name dump rpath_str =
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    80
  Library.setmp print_mode (modes @ ! print_mode) (fn () =>
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    81
    (init reset parent name;
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    82
     Present.init info doc (path ()) name
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    83
       (if dump = "" then None else Some (Path.unpack dump)) (get_rpath rpath_str);
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    84
     File.symbol_use root_file;
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    85
     finish ())) ()
fdde440a9033 use_dir: modes;
wenzelm
parents: 9414
diff changeset
    86
  handle exn => (writeln (Toplevel.exn_message exn); exit 1);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    87
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    88
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    89
end;