author | Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk> |
Wed, 16 Jan 2019 21:27:33 +0000 | |
changeset 69677 | a06b204527e6 |
parent 69349 | 7cef9e386ffe |
child 70049 | c1226e4c273e |
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 |
|
11 |
val command_parser: (Toplevel.transition -> Toplevel.transition) parser |
|
12 |
end; |
|
13 |
||
14 |
structure Sessions: SESSIONS = |
|
15 |
struct |
|
16 |
||
17 |
val root_name = "ROOT"; |
|
18 |
val theory_name = "Pure.Sessions"; |
|
19 |
||
20 |
local |
|
21 |
||
22 |
val global = |
|
23 |
Parse.$$$ "(" -- Parse.!!! (Parse.$$$ "global" -- Parse.$$$ ")") >> K true || Scan.succeed false; |
|
24 |
||
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
|
25 |
val theory_entry = Parse.theory_name --| global; |
67215 | 26 |
|
27 |
val theories = |
|
28 |
Parse.$$$ "theories" |-- Parse.!!! (Scan.optional Parse.options [] -- Scan.repeat1 theory_entry); |
|
29 |
||
68292 | 30 |
val in_path = |
31 |
Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.position Parse.path --| Parse.$$$ ")"); |
|
32 |
||
67215 | 33 |
val document_files = |
34 |
Parse.$$$ "document_files" |-- |
|
68292 | 35 |
Parse.!!! (Scan.optional in_path ("document", Position.none) |
67215 | 36 |
-- Scan.repeat1 (Parse.position Parse.path)); |
37 |
||
69677
a06b204527e6
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69349
diff
changeset
|
38 |
val prune = |
a06b204527e6
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69349
diff
changeset
|
39 |
Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.nat --| Parse.$$$ "]")) 0; |
a06b204527e6
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69349
diff
changeset
|
40 |
|
68292 | 41 |
val export_files = |
42 |
Parse.$$$ "export_files" |-- |
|
69677
a06b204527e6
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69349
diff
changeset
|
43 |
Parse.!!! |
a06b204527e6
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69349
diff
changeset
|
44 |
(Scan.optional in_path ("export", Position.none) -- prune -- Scan.repeat1 Parse.embedded); |
68292 | 45 |
|
67215 | 46 |
in |
47 |
||
48 |
val command_parser = |
|
49 |
Parse.session_name -- |
|
50 |
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.name --| Parse.$$$ ")")) [] -- |
|
51 |
Scan.optional (Parse.$$$ "in" |-- Parse.!!! (Parse.position Parse.path)) (".", Position.none) -- |
|
67220 | 52 |
(Parse.$$$ "=" |-- |
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
|
53 |
Parse.!!! (Scan.option (Parse.session_name --| Parse.!!! (Parse.$$$ "+")) -- |
67220 | 54 |
Scan.optional (Parse.$$$ "description" |-- Parse.!!! (Parse.input Parse.text)) Input.empty -- |
55 |
Scan.optional (Parse.$$$ "options" |-- Parse.!!! Parse.options) [] -- |
|
56 |
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
|
57 |
Parse.!!! (Scan.repeat1 Parse.session_name)) [] -- |
67220 | 58 |
Scan.repeat theories -- |
68292 | 59 |
Scan.repeat document_files -- |
60 |
Scan.repeat export_files)) |
|
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
|
61 |
>> (fn ((((session, _), _), dir), |
68292 | 62 |
(((((((parent, descr), options), sessions), theories), document_files), export_files))) => |
67215 | 63 |
Toplevel.keep (fn state => |
64 |
let |
|
65 |
val ctxt = Toplevel.context_of state; |
|
66 |
val thy = Toplevel.theory_of state; |
|
67 |
val session_dir = Resources.check_dir ctxt (Resources.master_directory thy) dir; |
|
68 |
||
69 |
val _ = |
|
67220 | 70 |
(the_list parent @ sessions) |> List.app (fn arg => |
71 |
ignore (Resources.check_session ctxt arg) |
|
72 |
handle ERROR msg => Output.error_message msg); |
|
73 |
||
74 |
val _ = |
|
67215 | 75 |
Context_Position.report ctxt |
76 |
(Position.range_position (Symbol_Pos.range (Input.source_explode descr))) |
|
77 |
Markup.comment; |
|
78 |
||
79 |
val _ = |
|
80 |
(options @ maps #1 theories) |> List.app (fn (x, y) => |
|
67220 | 81 |
ignore (Completion.check_option_value ctxt x y (Options.default ())) |
82 |
handle ERROR msg => Output.error_message msg); |
|
67215 | 83 |
|
84 |
val _ = |
|
85 |
maps #2 theories |> List.app (fn (s, pos) => |
|
86 |
let |
|
87 |
val {node_name, theory_name, ...} = |
|
88 |
Resources.import_name session session_dir s |
|
89 |
handle ERROR msg => error (msg ^ Position.here pos); |
|
90 |
val theory_path = the_default node_name (Resources.known_theory theory_name); |
|
91 |
val _ = Resources.check_file ctxt Path.current (Path.implode theory_path, pos); |
|
92 |
in () end); |
|
93 |
||
94 |
val _ = |
|
95 |
document_files |> List.app (fn (doc_dir, doc_files) => |
|
96 |
let |
|
97 |
val dir = Resources.check_dir ctxt session_dir doc_dir; |
|
98 |
val _ = List.app (ignore o Resources.check_file ctxt dir) doc_files; |
|
99 |
in () end); |
|
68292 | 100 |
|
101 |
val _ = |
|
69677
a06b204527e6
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69349
diff
changeset
|
102 |
export_files |> List.app (fn ((export_dir, _), _) => |
68292 | 103 |
ignore (Resources.check_path ctxt session_dir export_dir)); |
67215 | 104 |
in () end)); |
105 |
||
106 |
end; |
|
107 |
||
108 |
end; |