src/Pure/System/session.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32738 15bb09ca0378
child 36950 75b8f26f2f07
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
wenzelm@30173
     1
(*  Title:      Pure/System/session.ML
wenzelm@6346
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6346
     3
wenzelm@6346
     4
Session management -- maintain state of logic images.
wenzelm@6346
     5
*)
wenzelm@6346
     6
wenzelm@6346
     7
signature SESSION =
wenzelm@6346
     8
sig
wenzelm@25840
     9
  val id: unit -> string list
wenzelm@11509
    10
  val name: unit -> string
wenzelm@6346
    11
  val welcome: unit -> string
wenzelm@31688
    12
  val use_dir: string -> string -> bool -> string list -> bool -> bool ->
wenzelm@31688
    13
    string -> bool -> string list -> string -> string -> bool * string ->
wenzelm@32061
    14
    string -> int -> bool -> bool -> int -> int -> int -> unit
wenzelm@6346
    15
  val finish: unit -> unit
wenzelm@6346
    16
end;
wenzelm@6346
    17
wenzelm@6346
    18
structure Session: SESSION =
wenzelm@6346
    19
struct
wenzelm@6346
    20
wenzelm@6346
    21
wenzelm@6346
    22
(* session state *)
wenzelm@6346
    23
wenzelm@32738
    24
val session = Unsynchronized.ref ([Context.PureN]: string list);
wenzelm@32738
    25
val session_path = Unsynchronized.ref ([]: string list);
wenzelm@32738
    26
val session_finished = Unsynchronized.ref false;
wenzelm@32738
    27
val remote_path = Unsynchronized.ref (NONE: Url.T option);
wenzelm@9414
    28
wenzelm@9414
    29
wenzelm@9414
    30
(* access path *)
wenzelm@6346
    31
wenzelm@25840
    32
fun id () = ! session;
wenzelm@6346
    33
fun path () = ! session_path;
wenzelm@6346
    34
wenzelm@16451
    35
fun str_of [] = Context.PureN
wenzelm@6346
    36
  | str_of elems = space_implode "/" elems;
wenzelm@6346
    37
wenzelm@11509
    38
fun name () = "Isabelle/" ^ str_of (path ());
wenzelm@26109
    39
wenzelm@30173
    40
wenzelm@30173
    41
(* welcome *)
wenzelm@30173
    42
wenzelm@26109
    43
fun welcome () =
wenzelm@26134
    44
  if Distribution.is_official then
wenzelm@26134
    45
    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
wenzelm@26134
    46
  else
wenzelm@26134
    47
    "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
wenzelm@27643
    48
    (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
wenzelm@6346
    49
wenzelm@30173
    50
val _ =
wenzelm@30173
    51
  OuterSyntax.improper_command "welcome" "print welcome message" OuterKeyword.diag
wenzelm@30173
    52
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
wenzelm@30173
    53
wenzelm@6346
    54
wenzelm@9414
    55
(* add_path *)
wenzelm@9414
    56
wenzelm@9414
    57
fun add_path reset s =
wenzelm@9414
    58
  let val sess = ! session @ [s] in
wenzelm@18964
    59
    (case duplicates (op =) sess of
wenzelm@9414
    60
      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
wenzelm@9414
    61
    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
wenzelm@9414
    62
  end;
wenzelm@9414
    63
wenzelm@9414
    64
wenzelm@6346
    65
(* init *)
wenzelm@6346
    66
wenzelm@6346
    67
fun init reset parent name =
wenzelm@20664
    68
  if not (member (op =) (! session) parent) orelse not (! session_finished) then
wenzelm@6346
    69
    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
wenzelm@6346
    70
  else (add_path reset name; session_finished := false);
wenzelm@6346
    71
wenzelm@6346
    72
wenzelm@6346
    73
(* finish *)
wenzelm@6346
    74
wenzelm@6346
    75
fun finish () =
wenzelm@31688
    76
  (ThyInfo.finish ();
wenzelm@28207
    77
    Present.finish ();
wenzelm@28205
    78
    Future.shutdown ();
wenzelm@6346
    79
    session_finished := true);
wenzelm@6346
    80
wenzelm@6346
    81
wenzelm@6346
    82
(* use_dir *)
wenzelm@6346
    83
wenzelm@17207
    84
fun get_rpath rpath =
wenzelm@17207
    85
  (if rpath = "" then () else
wenzelm@15979
    86
     if is_some (! remote_path) then
berghofe@7227
    87
       error "Path for remote theory browsing information may only be set once"
berghofe@7227
    88
     else
wenzelm@21858
    89
       remote_path := SOME (Url.explode rpath);
wenzelm@17207
    90
   (! remote_path, rpath <> ""));
wenzelm@17207
    91
wenzelm@17207
    92
fun dumping (_, "") = NONE
wenzelm@21858
    93
  | dumping (cp, path) = SOME (cp, Path.explode path);
berghofe@7236
    94
wenzelm@31688
    95
fun use_dir item root build modes reset info doc doc_graph doc_versions parent
wenzelm@31688
    96
    name dump rpath level timing verbose max_threads trace_threads parallel_proofs =
wenzelm@23972
    97
  ((fn () =>
wenzelm@23972
    98
     (init reset parent name;
wenzelm@23972
    99
      Present.init build info doc doc_graph doc_versions (path ()) name
wenzelm@26612
   100
        (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
wenzelm@31688
   101
      if timing then
wenzelm@31688
   102
        let
wenzelm@31688
   103
          val start = start_timing ();
wenzelm@31688
   104
          val _ = use root;
wenzelm@31688
   105
          val stop = end_timing start;
wenzelm@31898
   106
          val _ =
wenzelm@31898
   107
            Output.std_error ("Timing " ^ item ^ " (" ^
wenzelm@31898
   108
              string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
wenzelm@31898
   109
              #message stop ^ ")\n");
wenzelm@31688
   110
        in () end
wenzelm@31688
   111
      else use root;
wenzelm@23972
   112
      finish ()))
wenzelm@23972
   113
    |> setmp_noncritical Proofterm.proofs level
wenzelm@24612
   114
    |> setmp_noncritical print_mode (modes @ print_mode_value ())
wenzelm@29435
   115
    |> setmp_noncritical Goal.parallel_proofs parallel_proofs
wenzelm@24061
   116
    |> setmp_noncritical Multithreading.trace trace_threads
wenzelm@23979
   117
    |> setmp_noncritical Multithreading.max_threads
wenzelm@23979
   118
      (if Multithreading.available then max_threads
wenzelm@23979
   119
       else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
wenzelm@31478
   120
  handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
wenzelm@6346
   121
wenzelm@6346
   122
end;