src/Pure/Isar/session.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18683 a8f9c192f6d1
child 18928 042608ffa2ec
permissions -rw-r--r--
simplified type attribute;
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
11509
d54301357129 export name;
wenzelm
parents: 10937
diff changeset
    10
  val name: unit -> string
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    11
  val welcome: unit -> string
17074
f6284547701b use_dir: removed hidden, added doc_versions;
wenzelm
parents: 16728
diff changeset
    12
  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool ->
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    13
    string list -> string -> string -> bool * string -> string -> int -> bool -> 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
16451
c9f1fc144132 Context.PureN;
wenzelm
parents: 15979
diff changeset
    23
val session = ref ([Context.PureN]: string list);
6346
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;
15979
wenzelm
parents: 15973
diff changeset
    26
val remote_path = ref (NONE: Url.T option);
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    27
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    28
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    29
(* access path *)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    30
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    31
fun path () = ! session_path;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    32
16451
c9f1fc144132 Context.PureN;
wenzelm
parents: 15979
diff changeset
    33
fun str_of [] = Context.PureN
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    34
  | str_of elems = space_implode "/" elems;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    35
11509
d54301357129 export name;
wenzelm
parents: 10937
diff changeset
    36
fun name () = "Isabelle/" ^ str_of (path ());
d54301357129 export name;
wenzelm
parents: 10937
diff changeset
    37
fun welcome () = "Welcome to " ^ name () ^ " (" ^ version ^ ")";
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    38
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    39
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    40
(* add_path *)
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    41
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    42
fun add_path reset s =
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    43
  let val sess = ! session @ [s] in
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    44
    (case Library.duplicates sess of
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    45
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    46
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    47
  end;
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    48
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    49
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    50
(* init *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    51
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    52
fun init reset parent name =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    53
  if not (parent mem_string (! session)) orelse not (! session_finished) then
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    54
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    55
  else (add_path reset name; session_finished := false);
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    58
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    59
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    60
fun finish () =
16728
c4c9d5df26ba finish: Output.accumulated_time;
wenzelm
parents: 16715
diff changeset
    61
  (Output.accumulated_time ();
c4c9d5df26ba finish: Output.accumulated_time;
wenzelm
parents: 16715
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
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    69
fun get_rpath rpath =
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    70
  (if rpath = "" then () else
15979
wenzelm
parents: 15973
diff changeset
    71
     if is_some (! remote_path) then
7227
a8e86b8e6fd1 Path for remote theory browsing information is now stored in referece variable rpath.
berghofe
parents: 6663
diff changeset
    72
       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
    73
     else
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    74
       remote_path := SOME (Url.unpack rpath);
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    75
   (! remote_path, rpath <> ""));
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    76
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    77
fun dumping (_, "") = NONE
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    78
  | dumping (cp, path) = SOME (cp, Path.unpack path);
7236
e077484d50d8 Better handling of path for remote theory browsing information.
berghofe
parents: 7227
diff changeset
    79
17074
f6284547701b use_dir: removed hidden, added doc_versions;
wenzelm
parents: 16728
diff changeset
    80
fun use_dir root build modes reset info doc doc_graph doc_versions
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    81
    parent name dump rpath level verbose =
11543
d61b913431c5 renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents: 11527
diff changeset
    82
  Library.setmp print_mode (modes @ ! print_mode)
17074
f6284547701b use_dir: removed hidden, added doc_versions;
wenzelm
parents: 16728
diff changeset
    83
    (Library.setmp Proofterm.proofs level (fn () =>
11543
d61b913431c5 renamed `keep_derivs' to `proofs', and made an integer;
wenzelm
parents: 11527
diff changeset
    84
      (init reset parent name;
17074
f6284547701b use_dir: removed hidden, added doc_versions;
wenzelm
parents: 16728
diff changeset
    85
       Present.init build info doc doc_graph doc_versions (path ()) name
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    86
         (dumping dump) (get_rpath rpath) verbose;
16715
ecca9fd2754f ThyInfo.time_use root;
wenzelm
parents: 16451
diff changeset
    87
       ThyInfo.time_use root;
17074
f6284547701b use_dir: removed hidden, added doc_versions;
wenzelm
parents: 16728
diff changeset
    88
       finish ()))) ()
18683
a8f9c192f6d1 Output.error_msg;
wenzelm
parents: 17207
diff changeset
    89
  handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    90
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    91
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    92
end;