1 (* Title: Pure/System/session.ML
2 Author: Markus Wenzel, TU Muenchen
4 Session management -- maintain state of logic images.
9 val id: unit -> string list
10 val name: unit -> string
11 val welcome: unit -> string
12 val finish: unit -> unit
13 val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
14 string -> string -> string * string -> string -> bool -> unit
15 val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
16 val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
17 string -> bool -> string list -> string -> string -> bool * string ->
18 string -> int -> bool -> bool -> int -> int -> int -> int -> unit
21 structure Session: SESSION =
27 val session = Unsynchronized.ref ([Context.PureN]: string list);
28 val session_path = Unsynchronized.ref ([]: string list);
29 val session_finished = Unsynchronized.ref false;
30 val remote_path = Unsynchronized.ref (NONE: Url.T option);
35 fun id () = ! session;
36 fun path () = ! session_path;
38 fun str_of [] = Context.PureN
39 | str_of elems = space_implode "/" elems;
41 fun name () = "Isabelle/" ^ str_of (path ());
47 if Distribution.is_official then
48 "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
50 "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
51 (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
54 Outer_Syntax.improper_command ("welcome", Keyword.diag) "print welcome message"
55 (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
60 fun add_path reset s =
61 let val sess = ! session @ [s] in
62 (case duplicates (op =) sess of
63 [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
64 | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
70 fun init_name reset parent name =
71 if not (member (op =) (! session) parent) orelse not (! session_finished) then
72 error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
73 else (add_path reset name; session_finished := false);
81 Outer_Syntax.check_syntax ();
83 session_finished := true);
88 fun with_timing _ false f x = f x
89 | with_timing item true f x =
91 val start = Timing.start ();
93 val timing = Timing.result start;
94 val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing)
95 |> Real.fmt (StringCvt.FIX (SOME 2));
97 Output.physical_stderr ("Timing " ^ item ^ " (" ^
98 string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
99 Timing.message timing ^ ", factor " ^ factor ^ ")\n");
102 fun get_rpath rpath =
103 (if rpath = "" then () else
104 if is_some (! remote_path) then
105 error "Path for remote theory browsing information may only be set once"
107 remote_path := SOME (Url.explode rpath);
108 (! remote_path, rpath <> ""));
110 fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose =
111 (init_name reset parent name;
112 Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
113 (path ()) name doc_dump (get_rpath rpath) verbose
114 (map Thy_Info.get_theory (Thy_Info.get_names ())));
118 fun doc_dump (cp, dump) = (dump, if cp then "all" else "tex+sty");
122 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
123 name dump rpath level timing verbose max_threads trace_threads
124 parallel_proofs parallel_proofs_threshold =
126 (init build reset info info_path doc doc_graph doc_variants parent name
127 (doc_dump dump) rpath verbose;
128 with_timing item timing use root;
130 |> Unsynchronized.setmp Proofterm.proofs level
131 |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())
132 |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs
133 |> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold
134 |> Unsynchronized.setmp Multithreading.trace trace_threads
135 |> Unsynchronized.setmp Multithreading.max_threads
136 (if Multithreading.available then max_threads
137 else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
138 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);