src/Pure/Isar/session.ML
author wenzelm
Mon, 25 Feb 2008 17:57:44 +0100
changeset 26136 a5198555e3e0
parent 26134 3b499feded50
child 26137 9b47c8a2d869
permissions -rw-r--r--
fixed ChangeLog.gz path;
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
25840
8a84f00f7139 export session id;
wenzelm
parents: 25703
diff changeset
    10
  val id: unit -> string list
11509
d54301357129 export name;
wenzelm
parents: 10937
diff changeset
    11
  val name: unit -> string
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    12
  val welcome: unit -> string
24061
68d2b6cf5194 added option -T (multithreading trace mode);
wenzelm
parents: 23979
diff changeset
    13
  val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
24118
464f260e5a20 multithreading trace: int;
wenzelm
parents: 24061
diff changeset
    14
    string -> string -> bool * string -> string -> int -> bool -> int -> int -> unit
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    15
  val finish: unit -> unit
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    16
end;
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
structure Session: SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    19
struct
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    22
(* session state *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    23
16451
c9f1fc144132 Context.PureN;
wenzelm
parents: 15979
diff changeset
    24
val session = ref ([Context.PureN]: string list);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    25
val session_path = ref ([]: string list);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    26
val session_finished = ref false;
15979
wenzelm
parents: 15973
diff changeset
    27
val remote_path = ref (NONE: Url.T option);
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    28
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    29
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    30
(* access path *)
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    31
25840
8a84f00f7139 export session id;
wenzelm
parents: 25703
diff changeset
    32
fun id () = ! session;
6346
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
16451
c9f1fc144132 Context.PureN;
wenzelm
parents: 15979
diff changeset
    35
fun str_of [] = Context.PureN
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
11509
d54301357129 export name;
wenzelm
parents: 10937
diff changeset
    38
fun name () = "Isabelle/" ^ str_of (path ());
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    39
26136
a5198555e3e0 fixed ChangeLog.gz path;
wenzelm
parents: 26134
diff changeset
    40
val log = Path.explode "$ISABELLE_HOME/ChangeLog.gz";
26134
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    41
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    42
fun welcome () =
26134
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    43
  if Distribution.is_official then
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    44
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    45
  else
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    46
    "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    47
    (if File.exists log then "\nSee " ^ Path.implode (Path.expand log) ^ " for details" else "");
6346
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
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    50
(* add_path *)
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    51
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    52
fun add_path reset s =
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    53
  let val sess = ! session @ [s] in
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18928
diff changeset
    54
    (case duplicates (op =) sess of
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    55
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    56
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    57
  end;
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    58
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    59
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    60
(* init *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    61
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    62
fun init reset parent name =
20664
ffbc5a57191a member (op =);
wenzelm
parents: 18964
diff changeset
    63
  if not (member (op =) (! session) parent) orelse not (! session_finished) then
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    64
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    65
  else (add_path reset name; session_finished := false);
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
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    69
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    70
fun finish () =
16728
c4c9d5df26ba finish: Output.accumulated_time;
wenzelm
parents: 16715
diff changeset
    71
  (Output.accumulated_time ();
c4c9d5df26ba finish: Output.accumulated_time;
wenzelm
parents: 16715
diff changeset
    72
    ThyInfo.finish ();
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    73
    Present.finish ();
21957
4e44e74dc7e7 Toplevel.init_state;
wenzelm
parents: 21858
diff changeset
    74
    Toplevel.init_state ();
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    75
    session_finished := true);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    76
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    77
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    78
(* use_dir *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    79
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    80
fun get_rpath rpath =
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    81
  (if rpath = "" then () else
15979
wenzelm
parents: 15973
diff changeset
    82
     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
    83
       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
    84
     else
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    85
       remote_path := SOME (Url.explode rpath);
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    86
   (! remote_path, rpath <> ""));
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    87
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    88
fun dumping (_, "") = NONE
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    89
  | dumping (cp, path) = SOME (cp, Path.explode path);
7236
e077484d50d8 Better handling of path for remote theory browsing information.
berghofe
parents: 7227
diff changeset
    90
17074
f6284547701b use_dir: removed hidden, added doc_versions;
wenzelm
parents: 16728
diff changeset
    91
fun use_dir root build modes reset info doc doc_graph doc_versions
24061
68d2b6cf5194 added option -T (multithreading trace mode);
wenzelm
parents: 23979
diff changeset
    92
    parent name dump rpath level verbose max_threads trace_threads =
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    93
  ((fn () =>
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    94
     (init reset parent name;
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    95
      Present.init build info doc doc_graph doc_versions (path ()) name
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    96
        (dumping dump) (get_rpath rpath) verbose (map ThyInfo.theory (ThyInfo.names ()));
25703
832073e402ae removed obsolete use_noncritical (plain use is already non-critical);
wenzelm
parents: 24612
diff changeset
    97
      use root;
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    98
      finish ()))
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    99
    |> setmp_noncritical Proofterm.proofs level
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 24118
diff changeset
   100
    |> setmp_noncritical print_mode (modes @ print_mode_value ())
24061
68d2b6cf5194 added option -T (multithreading trace mode);
wenzelm
parents: 23979
diff changeset
   101
    |> setmp_noncritical Multithreading.trace trace_threads
23979
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   102
    |> setmp_noncritical Multithreading.max_threads
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   103
      (if Multithreading.available then max_threads
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   104
       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
18683
a8f9c192f6d1 Output.error_msg;
wenzelm
parents: 17207
diff changeset
   105
  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
   106
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
   107
end;