author  wenzelm 
Wed, 08 Aug 2012 12:33:40 +0200  
changeset 48731  a45ba78abcc1 
parent 48709  719f458cd89e 
child 48804  6348e5fca42e 
permissions  rwrr 
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  2 
Author: Markus Wenzel, TU Muenchen 
3 

4 
Session management  maintain state of logic images. 

5 
*) 

6 

7 
signature SESSION = 

8 
sig 

25840  9 
val id: unit > string list 
11509  10 
val name: unit > string 
6346  11 
val welcome: unit > string 
48457  12 
val finish: unit > unit 
13 
val init: bool > bool > bool > string > string > bool > string list > 

48543  14 
string > string > string * Present.dump_mode > string > bool > unit 
48457  15 
val with_timing: string > bool > ('a > 'b) > 'a > 'b 
48445  16 
val use_dir: string > string > bool > string list > bool > bool > string > 
31688  17 
string > bool > string list > string > string > bool * string > 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
39733
diff
changeset

18 
string > int > bool > bool > int > int > int > int > unit 
6346  19 
end; 
20 

21 
structure Session: SESSION = 

22 
struct 

23 

24 
(* session state *) 

25 

32738  26 
val session = Unsynchronized.ref ([Context.PureN]: string list); 
27 
val session_finished = Unsynchronized.ref false; 

48542  28 

29 
fun id () = ! session; 

30 
fun name () = "Isabelle/" ^ List.last (! session); 

9414  31 

32 

33 
(* access path *) 

6346  34 

48542  35 
val session_path = Unsynchronized.ref ([]: string list); 
36 
val remote_path = Unsynchronized.ref (NONE: Url.T option); 

6346  37 

48542  38 
fun path () = ! session_path; 
26109
c69c3559355b
more elaborate structure Distribution (filledin 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 (filledin by makedist);
wenzelm
parents:
25840
diff
changeset

43 
fun welcome () = 
26134  44 
if Distribution.is_official then 
45 
"Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")" 

46 
else 

47 
"Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^ 

27643  48 
(if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else ""); 
6346  49 

50 

9414  51 
(* add_path *) 
52 

53 
fun add_path reset s = 

54 
let val sess = ! session @ [s] in 

18964  55 
(case duplicates (op =) sess of 
9414  56 
[] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s])) 
48542  57 
 dups => error ("Duplicate session identifiers " ^ commas_quote dups)) 
9414  58 
end; 
59 

60 

48457  61 
(* init_name *) 
6346  62 

48457  63 
fun init_name reset parent name = 
20664  64 
if not (member (op =) (! session) parent) orelse not (! session_finished) then 
6346  65 
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) 
66 
else (add_path reset name; session_finished := false); 

67 

68 

69 
(* finish *) 

70 

71 
fun finish () = 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset

72 
(Thy_Info.finish (); 
28207  73 
Present.finish (); 
48709
719f458cd89e
prefer static Build.outer_syntax in Isabelle/Scala session  discontinued incremental protocol;
wenzelm
parents:
48698
diff
changeset

74 
Keyword.status (); 
46970
9667e0dcb5e2
check declared vs. defined commands at end of session;
wenzelm
parents:
46961
diff
changeset

75 
Outer_Syntax.check_syntax (); 
28205  76 
Future.shutdown (); 
48698
2585042b1a30
pass Isabelle/Scala system options into ML process of Isar tty or build jobs;
wenzelm
parents:
48646
diff
changeset

77 
Options.reset_default (); 
6346  78 
session_finished := true); 
79 

80 

81 
(* use_dir *) 

82 

48457  83 
fun with_timing _ false f x = f x 
84 
 with_timing item true f x = 

85 
let 

86 
val start = Timing.start (); 

87 
val y = f x; 

88 
val timing = Timing.result start; 

89 
val factor = Time.toReal (#cpu timing) / Time.toReal (#elapsed timing) 

90 
> Real.fmt (StringCvt.FIX (SOME 2)); 

91 
val _ = 

92 
Output.physical_stderr ("Timing " ^ item ^ " (" ^ 

93 
string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ 

94 
Timing.message timing ^ ", factor " ^ factor ^ ")\n"); 

95 
in y end; 

96 

48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

97 
fun get_rpath rpath = 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

98 
(if rpath = "" then () else 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

99 
if is_some (! remote_path) then 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

100 
error "Path for remote theory browsing information may only be set once" 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

101 
else 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

102 
remote_path := SOME (Url.explode rpath); 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

103 
(! remote_path, rpath <> "")); 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

104 

c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

105 
fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose = 
48457  106 
(init_name reset parent name; 
48467
a4318c36a829
more precise propagation of options: build, session, theories;
wenzelm
parents:
48457
diff
changeset

107 
Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

108 
(path ()) name doc_dump (get_rpath rpath) verbose 
48467
a4318c36a829
more precise propagation of options: build, session, theories;
wenzelm
parents:
48457
diff
changeset

109 
(map Thy_Info.get_theory (Thy_Info.get_names ()))); 
48457  110 

48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

111 
local 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

112 

48543  113 
fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty); 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

114 

c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

115 
in 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

116 

48445  117 
fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
39733
diff
changeset

118 
name dump rpath level timing verbose max_threads trace_threads 
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
39733
diff
changeset

119 
parallel_proofs parallel_proofs_threshold = 
23972  120 
((fn () => 
48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

121 
(init build reset info info_path doc doc_graph doc_variants parent name 
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

122 
(doc_dump dump) rpath verbose; 
48457  123 
with_timing item timing use root; 
23972  124 
finish ())) 
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

125 
> Unsynchronized.setmp Proofterm.proofs level 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

126 
> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

127 
> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs 
41703
d27950860514
parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;
wenzelm
parents:
39733
diff
changeset

128 
> Unsynchronized.setmp Goal.parallel_proofs_threshold parallel_proofs_threshold 
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

129 
> Unsynchronized.setmp Multithreading.trace trace_threads 
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
37216
diff
changeset

130 
> Unsynchronized.setmp Multithreading.max_threads 
23979  131 
(if Multithreading.available then max_threads 
132 
else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) () 

31478  133 
handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); 
6346  134 

135 
end; 

48516
c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

136 

c5d0f19ef7cb
refined "document_dump_mode": "all", "tex+sty", "tex";
wenzelm
parents:
48467
diff
changeset

137 
end; 