author | wenzelm |
Thu, 26 Jul 2012 16:54:44 +0200 | |
changeset 49533 | 0c86acc069ad |
parent 49531 | c5d0f19ef7cb |
child 49557 | 0a5f598cacec |
permissions | -rw-r--r-- |
wenzelm@30174 | 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@49472 | 12 |
val finish: unit -> unit |
wenzelm@49472 | 13 |
val init: bool -> bool -> bool -> string -> string -> bool -> string list -> |
wenzelm@49531 | 14 |
string -> string -> string * string -> string -> bool -> unit |
wenzelm@49472 | 15 |
val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b |
wenzelm@49460 | 16 |
val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> |
wenzelm@31690 | 17 |
string -> bool -> string list -> string -> string -> bool * string -> |
wenzelm@42577 | 18 |
string -> int -> bool -> bool -> int -> int -> int -> int -> unit |
wenzelm@6346 | 19 |
end; |
wenzelm@6346 | 20 |
|
wenzelm@6346 | 21 |
structure Session: SESSION = |
wenzelm@6346 | 22 |
struct |
wenzelm@6346 | 23 |
|
wenzelm@6346 | 24 |
|
wenzelm@6346 | 25 |
(* session state *) |
wenzelm@6346 | 26 |
|
wenzelm@32738 | 27 |
val session = Unsynchronized.ref ([Context.PureN]: string list); |
wenzelm@32738 | 28 |
val session_path = Unsynchronized.ref ([]: string list); |
wenzelm@32738 | 29 |
val session_finished = Unsynchronized.ref false; |
wenzelm@32738 | 30 |
val remote_path = Unsynchronized.ref (NONE: Url.T option); |
wenzelm@9414 | 31 |
|
wenzelm@9414 | 32 |
|
wenzelm@9414 | 33 |
(* access path *) |
wenzelm@6346 | 34 |
|
wenzelm@25840 | 35 |
fun id () = ! session; |
wenzelm@6346 | 36 |
fun path () = ! session_path; |
wenzelm@6346 | 37 |
|
wenzelm@16451 | 38 |
fun str_of [] = Context.PureN |
wenzelm@6346 | 39 |
| str_of elems = space_implode "/" elems; |
wenzelm@6346 | 40 |
|
wenzelm@11509 | 41 |
fun name () = "Isabelle/" ^ str_of (path ()); |
wenzelm@26109 | 42 |
|
wenzelm@30174 | 43 |
|
wenzelm@30174 | 44 |
(* welcome *) |
wenzelm@30174 | 45 |
|
wenzelm@26109 | 46 |
fun welcome () = |
wenzelm@26134 | 47 |
if Distribution.is_official then |
wenzelm@26134 | 48 |
"Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")" |
wenzelm@26134 | 49 |
else |
wenzelm@26134 | 50 |
"Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^ |
wenzelm@27643 | 51 |
(if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else ""); |
wenzelm@6346 | 52 |
|
wenzelm@30174 | 53 |
val _ = |
wenzelm@47836 | 54 |
Outer_Syntax.improper_command ("welcome", Keyword.diag) "print welcome message" |
wenzelm@30174 | 55 |
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome))); |
wenzelm@30174 | 56 |
|
wenzelm@6346 | 57 |
|
wenzelm@9414 | 58 |
(* add_path *) |
wenzelm@9414 | 59 |
|
wenzelm@9414 | 60 |
fun add_path reset s = |
wenzelm@9414 | 61 |
let val sess = ! session @ [s] in |
wenzelm@18964 | 62 |
(case duplicates (op =) sess of |
wenzelm@9414 | 63 |
[] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s])) |
wenzelm@9414 | 64 |
| dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess)) |
wenzelm@9414 | 65 |
end; |
wenzelm@9414 | 66 |
|
wenzelm@9414 | 67 |
|
wenzelm@49472 | 68 |
(* init_name *) |
wenzelm@6346 | 69 |
|
wenzelm@49472 | 70 |
fun init_name reset parent name = |
wenzelm@20664 | 71 |
if not (member (op =) (! session) parent) orelse not (! session_finished) then |
wenzelm@6346 | 72 |
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) |
wenzelm@6346 | 73 |
else (add_path reset name; session_finished := false); |
wenzelm@6346 | 74 |
|
wenzelm@6346 | 75 |
|
wenzelm@6346 | 76 |
(* finish *) |
wenzelm@6346 | 77 |
|
wenzelm@6346 | 78 |
fun finish () = |
wenzelm@37216 | 79 |
(Thy_Info.finish (); |
wenzelm@28207 | 80 |
Present.finish (); |
wenzelm@47841 | 81 |
Outer_Syntax.check_syntax (); |
wenzelm@28205 | 82 |
Future.shutdown (); |
wenzelm@6346 | 83 |
session_finished := true); |
wenzelm@6346 | 84 |
|
wenzelm@6346 | 85 |
|
wenzelm@6346 | 86 |
(* use_dir *) |
wenzelm@6346 | 87 |
|
wenzelm@49472 | 88 |
fun with_timing _ false f x = f x |
wenzelm@49472 | 89 |
| with_timing item true f x = |
wenzelm@49472 | 90 |
let |
wenzelm@49472 | 91 |
val start = Timing.start (); |
wenzelm@49472 | 92 |
val y = f x; |
wenzelm@49472 | 93 |
val timing = Timing.result start; |
wenzelm@49472 | 94 |
val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) |
wenzelm@49472 | 95 |
|> Real.fmt (StringCvt.FIX (SOME 2)); |
wenzelm@49472 | 96 |
val _ = |
wenzelm@49472 | 97 |
Output.physical_stderr ("Timing " ^ item ^ " (" ^ |
wenzelm@49472 | 98 |
string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ |
wenzelm@49472 | 99 |
Timing.message timing ^ ", factor " ^ factor ^ ")\n"); |
wenzelm@49472 | 100 |
in y end; |
wenzelm@49472 | 101 |
|
wenzelm@49531 | 102 |
fun get_rpath rpath = |
wenzelm@49531 | 103 |
(if rpath = "" then () else |
wenzelm@49531 | 104 |
if is_some (! remote_path) then |
wenzelm@49531 | 105 |
error "Path for remote theory browsing information may only be set once" |
wenzelm@49531 | 106 |
else |
wenzelm@49531 | 107 |
remote_path := SOME (Url.explode rpath); |
wenzelm@49531 | 108 |
(! remote_path, rpath <> "")); |
wenzelm@49531 | 109 |
|
wenzelm@49531 | 110 |
fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose = |
wenzelm@49472 | 111 |
(init_name reset parent name; |
wenzelm@49482 | 112 |
Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants |
wenzelm@49531 | 113 |
(path ()) name doc_dump (get_rpath rpath) verbose |
wenzelm@49482 | 114 |
(map Thy_Info.get_theory (Thy_Info.get_names ()))); |
wenzelm@49472 | 115 |
|
wenzelm@49531 | 116 |
local |
wenzelm@49531 | 117 |
|
wenzelm@49533 | 118 |
fun doc_dump (cp, dump) = (dump, if cp then "all" else "tex+sty"); |
wenzelm@49531 | 119 |
|
wenzelm@49531 | 120 |
in |
wenzelm@49531 | 121 |
|
wenzelm@49460 | 122 |
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent |
wenzelm@42577 | 123 |
name dump rpath level timing verbose max_threads trace_threads |
wenzelm@42577 | 124 |
parallel_proofs parallel_proofs_threshold = |
wenzelm@23972 | 125 |
((fn () => |
wenzelm@49531 | 126 |
(init build reset info info_path doc doc_graph doc_variants parent name |
wenzelm@49531 | 127 |
(doc_dump dump) rpath verbose; |
wenzelm@49472 | 128 |
with_timing item timing use root; |
wenzelm@23972 | 129 |
finish ())) |
wenzelm@39862 | 130 |
|> Unsynchronized.setmp Proofterm.proofs level |
wenzelm@39862 | 131 |
|> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) |
wenzelm@39862 | 132 |
|> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs |
wenzelm@42577 | 133 |
|> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold |
wenzelm@39862 | 134 |
|> Unsynchronized.setmp Multithreading.trace trace_threads |
wenzelm@39862 | 135 |
|> Unsynchronized.setmp Multithreading.max_threads |
wenzelm@23979 | 136 |
(if Multithreading.available then max_threads |
wenzelm@23979 | 137 |
else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) () |
wenzelm@31478 | 138 |
handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); |
wenzelm@6346 | 139 |
|
wenzelm@6346 | 140 |
end; |
wenzelm@49531 | 141 |
|
wenzelm@49531 | 142 |
end; |