9 val id: unit -> string list |
9 val id: unit -> string list |
10 val name: unit -> string |
10 val name: unit -> string |
11 val welcome: unit -> string |
11 val welcome: unit -> string |
12 val finish: unit -> unit |
12 val finish: unit -> unit |
13 val init: bool -> bool -> bool -> string -> string -> bool -> string list -> |
13 val init: bool -> bool -> bool -> string -> string -> bool -> string list -> |
14 string -> string -> bool * string -> string -> bool -> unit |
14 string -> string -> string * string -> string -> bool -> unit |
15 val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b |
15 val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b |
16 val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> |
16 val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> |
17 string -> bool -> string list -> string -> string -> bool * string -> |
17 string -> bool -> string list -> string -> string -> bool * string -> |
18 string -> int -> bool -> bool -> int -> int -> int -> int -> unit |
18 string -> int -> bool -> bool -> int -> int -> int -> int -> unit |
19 end; |
19 end; |
83 session_finished := true); |
83 session_finished := true); |
84 |
84 |
85 |
85 |
86 (* use_dir *) |
86 (* use_dir *) |
87 |
87 |
88 fun get_rpath rpath = |
|
89 (if rpath = "" then () else |
|
90 if is_some (! remote_path) then |
|
91 error "Path for remote theory browsing information may only be set once" |
|
92 else |
|
93 remote_path := SOME (Url.explode rpath); |
|
94 (! remote_path, rpath <> "")); |
|
95 |
|
96 fun dumping (_, "") = NONE |
|
97 | dumping (cp, path) = SOME (cp, Path.explode path); |
|
98 |
|
99 fun with_timing _ false f x = f x |
88 fun with_timing _ false f x = f x |
100 | with_timing item true f x = |
89 | with_timing item true f x = |
101 let |
90 let |
102 val start = Timing.start (); |
91 val start = Timing.start (); |
103 val y = f x; |
92 val y = f x; |
108 Output.physical_stderr ("Timing " ^ item ^ " (" ^ |
97 Output.physical_stderr ("Timing " ^ item ^ " (" ^ |
109 string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ |
98 string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^ |
110 Timing.message timing ^ ", factor " ^ factor ^ ")\n"); |
99 Timing.message timing ^ ", factor " ^ factor ^ ")\n"); |
111 in y end; |
100 in y end; |
112 |
101 |
113 fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose = |
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" |
|
106 else |
|
107 remote_path := SOME (Url.explode rpath); |
|
108 (! remote_path, rpath <> "")); |
|
109 |
|
110 fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose = |
114 (init_name reset parent name; |
111 (init_name reset parent name; |
115 Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants |
112 Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants |
116 (path ()) name (dumping dump) (get_rpath rpath) verbose |
113 (path ()) name doc_dump (get_rpath rpath) verbose |
117 (map Thy_Info.get_theory (Thy_Info.get_names ()))); |
114 (map Thy_Info.get_theory (Thy_Info.get_names ()))); |
|
115 |
|
116 local |
|
117 |
|
118 fun doc_dump (cp, dump) = (if cp then "all" else "tex+sty", dump); |
|
119 |
|
120 in |
118 |
121 |
119 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent |
122 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent |
120 name dump rpath level timing verbose max_threads trace_threads |
123 name dump rpath level timing verbose max_threads trace_threads |
121 parallel_proofs parallel_proofs_threshold = |
124 parallel_proofs parallel_proofs_threshold = |
122 ((fn () => |
125 ((fn () => |
123 (init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose; |
126 (init build reset info info_path doc doc_graph doc_variants parent name |
|
127 (doc_dump dump) rpath verbose; |
124 with_timing item timing use root; |
128 with_timing item timing use root; |
125 finish ())) |
129 finish ())) |
126 |> Unsynchronized.setmp Proofterm.proofs level |
130 |> Unsynchronized.setmp Proofterm.proofs level |
127 |> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) |
131 |> Unsynchronized.setmp print_mode (modes @ print_mode_value ()) |
128 |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs |
132 |> Unsynchronized.setmp Goal.parallel_proofs parallel_proofs |