equal
deleted
inserted
replaced
4 Build Isabelle sessions. |
4 Build Isabelle sessions. |
5 *) |
5 *) |
6 |
6 |
7 signature BUILD = |
7 signature BUILD = |
8 sig |
8 sig |
9 val add_hook: ((theory * Document_Output.segment list) list -> unit) -> unit |
9 type hook = string -> (theory * Document_Output.segment list) list -> unit |
|
10 val add_hook: hook -> unit |
10 end; |
11 end; |
11 |
12 |
12 structure Build: BUILD = |
13 structure Build: BUILD = |
13 struct |
14 struct |
14 |
15 |
26 in y end; |
27 in y end; |
27 |
28 |
28 |
29 |
29 (* build theories *) |
30 (* build theories *) |
30 |
31 |
|
32 type hook = string -> (theory * Document_Output.segment list) list -> unit; |
|
33 |
31 local |
34 local |
32 val hooks = |
35 val hooks = Synchronized.var "Build.hooks" ([]: hook list); |
33 Synchronized.var "Build.hooks" |
|
34 ([]: ((theory * Document_Output.segment list) list -> unit) list); |
|
35 in |
36 in |
36 |
37 |
37 fun add_hook hook = Synchronized.change hooks (cons hook); |
38 fun add_hook hook = Synchronized.change hooks (cons hook); |
38 |
39 |
39 fun apply_hooks loaded_theories = |
40 fun apply_hooks qualifier loaded_theories = |
40 Synchronized.value hooks |
41 Synchronized.value hooks |
41 |> List.app (fn hook => hook loaded_theories); |
42 |> List.app (fn hook => hook qualifier loaded_theories); |
42 |
43 |
43 end; |
44 end; |
44 |
45 |
45 |
46 |
46 fun build_theories qualifier (options, thys) = |
47 fun build_theories qualifier (options, thys) = |
62 |> Unsynchronized.setmp print_mode |
63 |> Unsynchronized.setmp print_mode |
63 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) |
64 (space_explode "," (Options.string options "print_mode") @ print_mode_value ())) thys) |
64 else |
65 else |
65 (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
66 (Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
66 " (undefined " ^ commas conds ^ ")\n"); []) |
67 " (undefined " ^ commas conds ^ ")\n"); []) |
67 in apply_hooks loaded_theories end; |
68 in apply_hooks qualifier loaded_theories end; |
68 |
69 |
69 |
70 |
70 (* build session *) |
71 (* build session *) |
71 |
72 |
72 val _ = |
73 val _ = |