author | wenzelm |
Sat, 27 Aug 2022 12:18:49 +0200 | |
changeset 75998 | c36e5c6f3069 |
parent 75986 | 27d98da31985 |
child 76005 | a9bbf075f431 |
permissions | -rw-r--r-- |
67215 | 1 |
(* Title: Pure/Thy/sessions.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Support for session ROOT syntax. |
|
5 |
*) |
|
6 |
||
7 |
signature SESSIONS = |
|
8 |
sig |
|
9 |
val root_name: string |
|
10 |
val theory_name: string |
|
75986
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75679
diff
changeset
|
11 |
val chapter_definition_parser: (Toplevel.transition -> Toplevel.transition) parser |
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75679
diff
changeset
|
12 |
val session_parser: (Toplevel.transition -> Toplevel.transition) parser |
67215 | 13 |
end; |
14 |
||
15 |
structure Sessions: SESSIONS = |
|
16 |
struct |
|
17 |
||
18 |
val root_name = "ROOT"; |
|
19 |
val theory_name = "Pure.Sessions"; |
|
20 |
||
21 |
local |
|
22 |
||
75998 | 23 |
val description = |
24 |
Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.embedded)) Input.empty; |
|
25 |
||
72841 | 26 |
val theory_entry = Parse.input Parse.theory_name --| Parse.opt_keyword "global"; |
67215 | 27 |
|
28 |
val theories = |
|
29 |
Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry); |
|
30 |
||
68292 | 31 |
val in_path = |
72841 | 32 |
Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.path_input --| Parse.$$$ ")"); |
68292 | 33 |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
70683
diff
changeset
|
34 |
val document_theories = |
72841 | 35 |
Parse.$$$ "document_theories" |-- Scan.repeat1 (Parse.input Parse.theory_name); |
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
70683
diff
changeset
|
36 |
|
67215 | 37 |
val document_files = |
38 |
Parse.$$$ "document_files" |-- |
|
72841 | 39 |
Parse.!!! (Scan.optional in_path (Input.string "document") -- Scan.repeat1 Parse.path_input); |
67215 | 40 |
|
69671 | 41 |
val prune = |
42 |
Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0; |
|
43 |
||
68292 | 44 |
val export_files = |
45 |
Parse.$$$ "export_files" |-- |
|
72841 | 46 |
Parse.!!! (Scan.optional in_path (Input.string "export") -- prune -- Scan.repeat1 Parse.embedded); |
47 |
||
75679
aa89255b704c
support for classpath artifacts within session structure:
wenzelm
parents:
74887
diff
changeset
|
48 |
val export_classpath = |
aa89255b704c
support for classpath artifacts within session structure:
wenzelm
parents:
74887
diff
changeset
|
49 |
Parse.$$$ "export_classpath" |-- Scan.repeat Parse.embedded; |
aa89255b704c
support for classpath artifacts within session structure:
wenzelm
parents:
74887
diff
changeset
|
50 |
|
72841 | 51 |
fun path_source source path = |
52 |
Input.source (Input.is_delimited source) (Path.implode path) (Input.range_of source); |
|
68292 | 53 |
|
67215 | 54 |
in |
55 |
||
75986
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75679
diff
changeset
|
56 |
val chapter_definition_parser = |
75998 | 57 |
Parse.chapter_name -- description >> (fn (_, descr) => |
58 |
Toplevel.keep (fn state => |
|
59 |
let |
|
60 |
val ctxt = Toplevel.context_of state; |
|
61 |
val _ = |
|
62 |
Context_Position.report ctxt |
|
63 |
(Position.range_position (Symbol_Pos.range (Input.source_explode descr))) |
|
64 |
Markup.comment; |
|
65 |
in () end)); |
|
75986
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75679
diff
changeset
|
66 |
|
27d98da31985
support 'chapter_definition' with description for presentation purposes;
wenzelm
parents:
75679
diff
changeset
|
67 |
val session_parser = |
67215 | 68 |
Parse.session_name -- |
69 |
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] -- |
|
72841 | 70 |
Scan.optional (Parse.$$$ "in" |-- Parse.!!! Parse.path_input) (Input.string ".") -- |
67220 | 71 |
(Parse.$$$ "=" |-- |
75998 | 72 |
Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- description -- |
67220 | 73 |
Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] -- |
74 |
Scan.optional (Parse.$$$ "sessions" |-- |
|
69349
7cef9e386ffe
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
wenzelm
parents:
68808
diff
changeset
|
75 |
Parse.!!! (Scan.repeat1 Parse.session_name)) [] -- |
72841 | 76 |
Scan.optional (Parse.$$$ "directories" |-- Parse.!!! (Scan.repeat1 Parse.path_input)) [] -- |
67220 | 77 |
Scan.repeat theories -- |
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
70683
diff
changeset
|
78 |
Scan.optional document_theories [] -- |
68292 | 79 |
Scan.repeat document_files -- |
75679
aa89255b704c
support for classpath artifacts within session structure:
wenzelm
parents:
74887
diff
changeset
|
80 |
Scan.repeat export_files -- |
aa89255b704c
support for classpath artifacts within session structure:
wenzelm
parents:
74887
diff
changeset
|
81 |
Scan.optional export_classpath [])) |
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
70683
diff
changeset
|
82 |
>> (fn (((((session, _), _), dir), |
75679
aa89255b704c
support for classpath artifacts within session structure:
wenzelm
parents:
74887
diff
changeset
|
83 |
((((((((((parent, descr), options), sessions), directories), theories), |
aa89255b704c
support for classpath artifacts within session structure:
wenzelm
parents:
74887
diff
changeset
|
84 |
document_theories), document_files), export_files), _)))) => |
67215 | 85 |
Toplevel.keep (fn state => |
86 |
let |
|
87 |
val ctxt = Toplevel.context_of state; |
|
70049 | 88 |
val session_dir = Resources.check_dir ctxt NONE dir; |
67215 | 89 |
|
90 |
val _ = |
|
67220 | 91 |
(the_list parent @ sessions) |> List.app (fn arg => |
92 |
ignore (Resources.check_session ctxt arg) |
|
93 |
handle ERROR msg => Output.error_message msg); |
|
94 |
||
95 |
val _ = |
|
67215 | 96 |
Context_Position.report ctxt |
97 |
(Position.range_position (Symbol_Pos.range (Input.source_explode descr))) |
|
98 |
Markup.comment; |
|
99 |
||
100 |
val _ = |
|
101 |
(options @ maps #1 theories) |> List.app (fn (x, y) => |
|
67220 | 102 |
ignore (Completion.check_option_value ctxt x y (Options.default ())) |
103 |
handle ERROR msg => Output.error_message msg); |
|
67215 | 104 |
|
72841 | 105 |
fun check_thy source = |
106 |
ignore (Resources.check_file ctxt (SOME Path.current) source) |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
70683
diff
changeset
|
107 |
handle ERROR msg => Output.error_message msg; |
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
70683
diff
changeset
|
108 |
|
67215 | 109 |
val _ = |
72841 | 110 |
maps #2 theories |> List.app (fn source => |
67215 | 111 |
let |
72841 | 112 |
val s = Input.string_of source; |
113 |
val pos = Input.pos_of source; |
|
67215 | 114 |
val {node_name, theory_name, ...} = |
115 |
Resources.import_name session session_dir s |
|
116 |
handle ERROR msg => error (msg ^ Position.here pos); |
|
72841 | 117 |
val thy_path = the_default node_name (Resources.find_theory_file theory_name); |
118 |
in check_thy (path_source source thy_path) end); |
|
67215 | 119 |
|
120 |
val _ = |
|
70681 | 121 |
directories |> List.app (ignore o Resources.check_dir ctxt (SOME session_dir)); |
70668 | 122 |
|
123 |
val _ = |
|
72841 | 124 |
document_theories |> List.app (fn source => |
125 |
let |
|
126 |
val thy = Input.string_of source; |
|
127 |
val pos = Input.pos_of source; |
|
128 |
in |
|
129 |
(case Resources.find_theory_file thy of |
|
130 |
NONE => Output.error_message ("Unknown theory " ^ quote thy ^ Position.here pos) |
|
131 |
| SOME path => check_thy (path_source source path)) |
|
132 |
end); |
|
72600
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
70683
diff
changeset
|
133 |
|
2fa4f25d9d07
official support for document theories from other sessions;
wenzelm
parents:
70683
diff
changeset
|
134 |
val _ = |
67215 | 135 |
document_files |> List.app (fn (doc_dir, doc_files) => |
136 |
let |
|
70049 | 137 |
val dir = Resources.check_dir ctxt (SOME session_dir) doc_dir; |
138 |
val _ = List.app (ignore o Resources.check_file ctxt (SOME dir)) doc_files; |
|
67215 | 139 |
in () end); |
68292 | 140 |
|
141 |
val _ = |
|
69671 | 142 |
export_files |> List.app (fn ((export_dir, _), _) => |
70049 | 143 |
ignore (Resources.check_path ctxt (SOME session_dir) export_dir)); |
67215 | 144 |
in () end)); |
145 |
||
146 |
end; |
|
147 |
||
148 |
end; |