src/Pure/System/session.ML
author wenzelm
Mon, 03 May 2010 20:13:36 +0200
changeset 36615 88756a5a92fc
parent 32738 15bb09ca0378
child 36950 75b8f26f2f07
permissions -rw-r--r--
renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30173
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
     1
(*  Title:      Pure/System/session.ML
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     3
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     4
Session management -- maintain state of logic images.
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
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     7
signature SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
     8
sig
25840
8a84f00f7139 export session id;
wenzelm
parents: 25703
diff changeset
     9
  val id: unit -> string list
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
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
    12
  val use_dir: string -> string -> bool -> string list -> bool -> bool ->
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
    13
    string -> bool -> string list -> string -> string -> bool * string ->
32061
11f8ee55662d parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;
wenzelm
parents: 31898
diff changeset
    14
    string -> int -> bool -> bool -> int -> 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
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    24
val session = Unsynchronized.ref ([Context.PureN]: string list);
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    25
val session_path = Unsynchronized.ref ([]: string list);
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    26
val session_finished = Unsynchronized.ref false;
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 32061
diff changeset
    27
val remote_path = Unsynchronized.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
30173
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    40
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    41
(* welcome *)
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    42
26109
c69c3559355b more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents: 25840
diff changeset
    43
fun welcome () =
26134
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    44
  if Distribution.is_official then
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    45
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    46
  else
3b499feded50 welcome: actually check for ChangeLog.gz;
wenzelm
parents: 26109
diff changeset
    47
    "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
27643
cc13e03124f0 explicit Distribution.changelog;
wenzelm
parents: 26612
diff changeset
    48
    (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    49
30173
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    50
val _ =
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    51
  OuterSyntax.improper_command "welcome" "print welcome message" OuterKeyword.diag
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    52
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
wenzelm
parents: 29435
diff changeset
    53
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    54
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    55
(* add_path *)
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    56
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    57
fun add_path reset s =
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    58
  let val sess = ! session @ [s] in
18964
67f572e03236 renamed gen_duplicates to duplicates;
wenzelm
parents: 18928
diff changeset
    59
    (case duplicates (op =) sess of
9414
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    60
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    61
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    62
  end;
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    63
1463576f3968 disallow duplicates in session identifiers;
wenzelm
parents: 8807
diff changeset
    64
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    65
(* init *)
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
fun init reset parent name =
20664
ffbc5a57191a member (op =);
wenzelm
parents: 18964
diff changeset
    68
  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
    69
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    70
  else (add_path reset name; session_finished := false);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    71
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    72
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    73
(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    74
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    75
fun finish () =
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
    76
  (ThyInfo.finish ();
28207
e2431cc4dc66 finish: Future.shutdown last;
wenzelm
parents: 28205
diff changeset
    77
    Present.finish ();
28205
17a81e481142 finish: Future.shutdown;
wenzelm
parents: 27643
diff changeset
    78
    Future.shutdown ();
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    79
    session_finished := true);
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    80
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    81
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    82
(* use_dir *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
    83
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    84
fun get_rpath rpath =
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    85
  (if rpath = "" then () else
15979
wenzelm
parents: 15973
diff changeset
    86
     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
    87
       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
    88
     else
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    89
       remote_path := SOME (Url.explode rpath);
17207
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    90
   (! remote_path, rpath <> ""));
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    91
19aa5ad633a7 use_dir: added copy-dump option;
wenzelm
parents: 17074
diff changeset
    92
fun dumping (_, "") = NONE
21858
05f57309170c avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
wenzelm
parents: 20664
diff changeset
    93
  | dumping (cp, path) = SOME (cp, Path.explode path);
7236
e077484d50d8 Better handling of path for remote theory browsing information.
berghofe
parents: 7227
diff changeset
    94
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
    95
fun use_dir item root build modes reset info doc doc_graph doc_versions parent
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
    96
    name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    97
  ((fn () =>
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    98
     (init reset parent name;
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
    99
      Present.init build info doc doc_graph doc_versions (path ()) name
26612
f9c3c2110b03 ThyInfo.get_theory;
wenzelm
parents: 26601
diff changeset
   100
        (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
   101
      if timing then
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
   102
        let
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
   103
          val start = start_timing ();
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
   104
          val _ = use root;
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
   105
          val stop = end_timing start;
31898
82d5190ff7c8 more detailed timing message;
wenzelm
parents: 31688
diff changeset
   106
          val _ =
82d5190ff7c8 more detailed timing message;
wenzelm
parents: 31688
diff changeset
   107
            Output.std_error ("Timing " ^ item ^ " (" ^
82d5190ff7c8 more detailed timing message;
wenzelm
parents: 31688
diff changeset
   108
              string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
82d5190ff7c8 more detailed timing message;
wenzelm
parents: 31688
diff changeset
   109
              #message stop ^ ")\n");
31688
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
   110
        in () end
f27cc190083b usedir: internal timing option;
wenzelm
parents: 31478
diff changeset
   111
      else use root;
23972
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
   112
      finish ()))
9c418fa38f7e added usedir option -M: max threads;
wenzelm
parents: 23936
diff changeset
   113
    |> setmp_noncritical Proofterm.proofs level
24612
d1b315bdb8d7 avoid direct access to print_mode;
wenzelm
parents: 24118
diff changeset
   114
    |> setmp_noncritical print_mode (modes @ print_mode_value ())
29435
a5f84ac14609 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
wenzelm
parents: 28207
diff changeset
   115
    |> setmp_noncritical Goal.parallel_proofs parallel_proofs
24061
68d2b6cf5194 added option -T (multithreading trace mode);
wenzelm
parents: 23979
diff changeset
   116
    |> setmp_noncritical Multithreading.trace trace_threads
23979
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   117
    |> setmp_noncritical Multithreading.max_threads
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   118
      (if Multithreading.available then max_threads
a15c13a54ab5 Secure.use_noncritical root;
wenzelm
parents: 23972
diff changeset
   119
       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
31478
5e412e4c6546 ML_Compiler.exn_message;
wenzelm
parents: 30173
diff changeset
   120
  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
6346
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
   121
643a1bd31a91 moved Thy/session.ML to Isar/session.ML;
wenzelm
parents:
diff changeset
   122
end;