author | wenzelm |
Sat, 28 Nov 2020 17:38:03 +0100 | |
changeset 72760 | 042180540068 |
parent 72758 | 9d0951e24e61 |
child 72841 | fd8d82c4433b |
permissions | -rw-r--r-- |
56208 | 1 |
(* Title: Pure/PIDE/resources.ML |
42002 | 2 |
Author: Makarius |
6168 | 3 |
|
56208 | 4 |
Resources for theories and auxiliary files. |
6168 | 5 |
*) |
6 |
||
56208 | 7 |
signature RESOURCES = |
6168 | 8 |
sig |
65532 | 9 |
val default_qualifier: string |
71875 | 10 |
val init_session: |
72669 | 11 |
{session_positions: (string * Properties.T) list, |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70049
diff
changeset
|
12 |
session_directories: (string * string) list, |
72616 | 13 |
session_chapters: (string * string) list, |
72613
d01ea9e3bd2d
clarified bibtex_entries: refer to overall session structure;
wenzelm
parents:
72511
diff
changeset
|
14 |
bibtex_entries: (string * string list) list, |
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
15 |
command_timings: Properties.T list, |
72756 | 16 |
scala_functions: (string * Position.T) list, |
67219 | 17 |
global_theories: (string * string) list, |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
18 |
loaded_theories: string list} -> unit |
72637 | 19 |
val init_session_yxml: string -> unit |
20 |
val init_session_file: Path.T -> unit |
|
65478
7c40477e0a87
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
wenzelm
parents:
65476
diff
changeset
|
21 |
val finish_session_base: unit -> unit |
65457 | 22 |
val global_theory: string -> string option |
66712 | 23 |
val loaded_theory: string -> bool |
67219 | 24 |
val check_session: Proof.context -> string * Position.T -> string |
72616 | 25 |
val session_chapter: string -> string |
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
26 |
val last_timing: Toplevel.transition -> Time.time |
72756 | 27 |
val scala_function_pos: string -> Position.T |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
28 |
val master_directory: theory -> Path.T |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48924
diff
changeset
|
29 |
val imports_of: theory -> (string * Position.T) list |
65505 | 30 |
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory |
46737 | 31 |
val thy_path: Path.T -> Path.T |
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65443
diff
changeset
|
32 |
val theory_qualifier: string -> string |
72613
d01ea9e3bd2d
clarified bibtex_entries: refer to overall session structure;
wenzelm
parents:
72511
diff
changeset
|
33 |
val theory_bibtex_entries: string -> string list |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70049
diff
changeset
|
34 |
val find_theory_file: string -> Path.T option |
67215 | 35 |
val import_name: string -> Path.T -> string -> |
36 |
{node_name: Path.T, master_dir: Path.T, theory_name: string} |
|
48898
9fc880720663
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
wenzelm
parents:
48897
diff
changeset
|
37 |
val check_thy: Path.T -> string -> |
48928 | 38 |
{master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, |
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51273
diff
changeset
|
39 |
imports: (string * Position.T) list, keywords: Thy_Header.keywords} |
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
40 |
val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
41 |
val parse_file: (theory -> Token.file) parser |
48906 | 42 |
val provide: Path.T * SHA1.digest -> theory -> theory |
69851 | 43 |
val provide_file: Token.file -> theory -> theory |
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
44 |
val provide_parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list * theory) parser |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
45 |
val provide_parse_file: (theory -> Token.file * theory) parser |
54446 | 46 |
val loaded_files_current: theory -> bool |
70049 | 47 |
val check_path: Proof.context -> Path.T option -> string * Position.T -> Path.T |
48 |
val check_file: Proof.context -> Path.T option -> string * Position.T -> Path.T |
|
49 |
val check_dir: Proof.context -> Path.T option -> string * Position.T -> Path.T |
|
6168 | 50 |
end; |
51 |
||
56208 | 52 |
structure Resources: RESOURCES = |
6168 | 53 |
struct |
54 |
||
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
55 |
(* command timings *) |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
56 |
|
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
57 |
type timings = ((string * Time.time) Inttab.table) Symtab.table; (*file -> offset -> name, time*) |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
58 |
|
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
59 |
val empty_timings: timings = Symtab.empty; |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
60 |
|
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
61 |
fun update_timings props = |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
62 |
(case Markup.parse_command_timing_properties props of |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
63 |
SOME ({file, offset, name}, time) => |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
64 |
Symtab.map_default (file, Inttab.empty) |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
65 |
(Inttab.map_default (offset, (name, time)) (fn (_, t) => (name, t + time))) |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
66 |
| NONE => I); |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
67 |
|
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
68 |
fun make_timings command_timings = |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
69 |
fold update_timings command_timings empty_timings; |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
70 |
|
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
71 |
fun approximative_id name pos = |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
72 |
(case (Position.file_of pos, Position.offset_of pos) of |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
73 |
(SOME file, SOME offset) => |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
74 |
if name = "" then NONE else SOME {file = file, offset = offset, name = name} |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
75 |
| _ => NONE); |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
76 |
|
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
77 |
fun get_timings timings tr = |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
78 |
(case approximative_id (Toplevel.name_of tr) (Toplevel.pos_of tr) of |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
79 |
SOME {file, offset, name} => |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
80 |
(case Symtab.lookup timings file of |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
81 |
SOME offsets => |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
82 |
(case Inttab.lookup offsets offset of |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
83 |
SOME (name', time) => if name = name' then SOME time else NONE |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
84 |
| NONE => NONE) |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
85 |
| NONE => NONE) |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
86 |
| NONE => NONE) |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
87 |
|> the_default Time.zeroTime; |
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
88 |
|
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
89 |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65058
diff
changeset
|
90 |
(* session base *) |
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65058
diff
changeset
|
91 |
|
65532 | 92 |
val default_qualifier = "Draft"; |
93 |
||
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67473
diff
changeset
|
94 |
type entry = {pos: Position.T, serial: serial}; |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67473
diff
changeset
|
95 |
|
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67473
diff
changeset
|
96 |
fun make_entry props : entry = |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67473
diff
changeset
|
97 |
{pos = Position.of_properties props, serial = serial ()}; |
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67473
diff
changeset
|
98 |
|
65478
7c40477e0a87
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
wenzelm
parents:
65476
diff
changeset
|
99 |
val empty_session_base = |
72758 | 100 |
({session_positions = []: (string * entry) list, |
101 |
session_directories = Symtab.empty: Path.T list Symtab.table, |
|
102 |
session_chapters = Symtab.empty: string Symtab.table, |
|
103 |
bibtex_entries = Symtab.empty: string list Symtab.table, |
|
104 |
timings = empty_timings, |
|
105 |
scala_functions = Symtab.empty: Position.T Symtab.table}, |
|
106 |
{global_theories = Symtab.empty: string Symtab.table, |
|
107 |
loaded_theories = Symtab.empty: unit Symtab.table}); |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65058
diff
changeset
|
108 |
|
65441 | 109 |
val global_session_base = |
65478
7c40477e0a87
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
wenzelm
parents:
65476
diff
changeset
|
110 |
Synchronized.var "Sessions.base" empty_session_base; |
65441 | 111 |
|
71875 | 112 |
fun init_session |
72756 | 113 |
{session_positions, session_directories, session_chapters, bibtex_entries, |
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
72758
diff
changeset
|
114 |
command_timings, scala_functions, global_theories, loaded_theories} = |
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65058
diff
changeset
|
115 |
Synchronized.change global_session_base |
65441 | 116 |
(fn _ => |
72758 | 117 |
({session_positions = sort_by #1 (map (apsnd make_entry) session_positions), |
118 |
session_directories = |
|
119 |
fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) |
|
120 |
session_directories Symtab.empty, |
|
121 |
session_chapters = Symtab.make session_chapters, |
|
122 |
bibtex_entries = Symtab.make bibtex_entries, |
|
123 |
timings = make_timings command_timings, |
|
124 |
scala_functions = Symtab.make scala_functions}, |
|
125 |
{global_theories = Symtab.make global_theories, |
|
126 |
loaded_theories = Symtab.make_set loaded_theories})); |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65058
diff
changeset
|
127 |
|
72637 | 128 |
fun init_session_yxml yxml = |
129 |
let |
|
72756 | 130 |
val (session_positions, (session_directories, (session_chapters, (bibtex_entries, |
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
72758
diff
changeset
|
131 |
(command_timings, (scala_functions, (global_theories, loaded_theories))))))) = |
72637 | 132 |
YXML.parse_body yxml |> |
133 |
let open XML.Decode in |
|
72669 | 134 |
(pair (list (pair string properties)) |
135 |
(pair (list (pair string string)) (pair (list (pair string string)) |
|
136 |
(pair (list (pair string (list string))) (pair (list properties) |
|
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
72758
diff
changeset
|
137 |
(pair (list (pair string properties)) |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
72758
diff
changeset
|
138 |
(pair (list (pair string string)) (list string)))))))) |
72637 | 139 |
end; |
140 |
in |
|
141 |
init_session |
|
72669 | 142 |
{session_positions = session_positions, |
72637 | 143 |
session_directories = session_directories, |
144 |
session_chapters = session_chapters, |
|
145 |
bibtex_entries = bibtex_entries, |
|
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
146 |
command_timings = command_timings, |
72756 | 147 |
scala_functions = map (apsnd Position.of_properties) scala_functions, |
72637 | 148 |
global_theories = global_theories, |
149 |
loaded_theories = loaded_theories} |
|
150 |
end; |
|
151 |
||
152 |
fun init_session_file path = |
|
153 |
init_session_yxml (File.read path) before File.rm path; |
|
154 |
||
65478
7c40477e0a87
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
wenzelm
parents:
65476
diff
changeset
|
155 |
fun finish_session_base () = |
7c40477e0a87
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
wenzelm
parents:
65476
diff
changeset
|
156 |
Synchronized.change global_session_base |
72758 | 157 |
(apfst (K (#1 empty_session_base))); |
65441 | 158 |
|
159 |
fun get_session_base f = f (Synchronized.value global_session_base); |
|
72758 | 160 |
fun get_session_base1 f = get_session_base (f o #1); |
161 |
fun get_session_base2 f = get_session_base (f o #2); |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65058
diff
changeset
|
162 |
|
72758 | 163 |
fun global_theory a = Symtab.lookup (get_session_base2 #global_theories) a; |
164 |
fun loaded_theory a = Symtab.defined (get_session_base2 #loaded_theories) a; |
|
65431
4a3e6cda3b94
provide session base for "isabelle build" and "isabelle console" ML process;
wenzelm
parents:
65058
diff
changeset
|
165 |
|
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
72758
diff
changeset
|
166 |
fun check_session ctxt arg = |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
72758
diff
changeset
|
167 |
Completion.check_item "session" |
71911 | 168 |
(fn (name, {pos, serial}) => |
169 |
Markup.entity Markup.sessionN name |
|
72760
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
72758
diff
changeset
|
170 |
|> Markup.properties (Position.entity_properties_of false serial pos)) |
042180540068
clarified protocol: Doc.check at run-time via Scala function;
wenzelm
parents:
72758
diff
changeset
|
171 |
(get_session_base1 #session_positions) ctxt arg; |
67493
c4e9e0c50487
treat sessions as entities with defining position;
wenzelm
parents:
67473
diff
changeset
|
172 |
|
72616 | 173 |
fun session_chapter name = |
72758 | 174 |
the_default "Unsorted" (Symtab.lookup (get_session_base1 #session_chapters) name); |
72616 | 175 |
|
72758 | 176 |
fun last_timing tr = get_timings (get_session_base1 #timings) tr; |
72638
2a7fc87495e0
refer to command_timings/last_timing via resources;
wenzelm
parents:
72637
diff
changeset
|
177 |
|
72756 | 178 |
fun scala_function_pos name = |
72758 | 179 |
Symtab.lookup (get_session_base1 #scala_functions) name |
72756 | 180 |
|> the_default Position.none; |
181 |
||
67471 | 182 |
|
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
183 |
(* manage source files *) |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
184 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
185 |
type files = |
40741
17d6293a1e26
moved file identification to thy_load.ML (where it is actually used);
wenzelm
parents:
40625
diff
changeset
|
186 |
{master_dir: Path.T, (*master directory of theory source*) |
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48924
diff
changeset
|
187 |
imports: (string * Position.T) list, (*source specification of imports*) |
48896
bb1f461a7815
simplified Thy_Load.provide: do not store full path;
wenzelm
parents:
48888
diff
changeset
|
188 |
provided: (Path.T * SHA1.digest) list}; (*source path, digest*) |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
189 |
|
48886
9604c6563226
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm
parents:
48881
diff
changeset
|
190 |
fun make_files (master_dir, imports, provided): files = |
9604c6563226
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm
parents:
48881
diff
changeset
|
191 |
{master_dir = master_dir, imports = imports, provided = provided}; |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
192 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
193 |
structure Files = Theory_Data |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
194 |
( |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
195 |
type T = files; |
48886
9604c6563226
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm
parents:
48881
diff
changeset
|
196 |
val empty = make_files (Path.current, [], []); |
72045
2c7cfd2f9b6c
more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);
wenzelm
parents:
71912
diff
changeset
|
197 |
val extend = I; |
2c7cfd2f9b6c
more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);
wenzelm
parents:
71912
diff
changeset
|
198 |
fun merge ({master_dir, imports, provided = provided1}, {provided = provided2, ...}) = |
2c7cfd2f9b6c
more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);
wenzelm
parents:
71912
diff
changeset
|
199 |
let val provided' = Library.merge (op =) (provided1, provided2) |
2c7cfd2f9b6c
more thorough extend/merge, notably for master_dir across Theory.join_theory (e.g. for @{file} antiquotation);
wenzelm
parents:
71912
diff
changeset
|
200 |
in make_files (master_dir, imports, provided') end |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
201 |
); |
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
202 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
203 |
fun map_files f = |
48886
9604c6563226
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm
parents:
48881
diff
changeset
|
204 |
Files.map (fn {master_dir, imports, provided} => |
9604c6563226
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm
parents:
48881
diff
changeset
|
205 |
make_files (f (master_dir, imports, provided))); |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
206 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
207 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
208 |
val master_directory = #master_dir o Files.get; |
41548
bd0bebf93fa6
Thy_Load.begin_theory: maintain source specification of imports;
wenzelm
parents:
41414
diff
changeset
|
209 |
val imports_of = #imports o Files.get; |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
210 |
|
65505 | 211 |
fun begin_theory master_dir {name, imports, keywords} parents = |
212 |
Theory.begin_theory name parents |
|
72162 | 213 |
|> map_files (fn _ => (Path.explode (Path.implode_symbolic master_dir), imports, [])) |
65505 | 214 |
|> Thy_Header.add_keywords keywords; |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
215 |
|
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
216 |
|
54525 | 217 |
(* theory files *) |
218 |
||
219 |
val thy_path = Path.ext "thy"; |
|
48869 | 220 |
|
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65443
diff
changeset
|
221 |
fun theory_qualifier theory = |
65457 | 222 |
(case global_theory theory of |
223 |
SOME qualifier => qualifier |
|
224 |
| NONE => Long_Name.qualifier theory); |
|
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65443
diff
changeset
|
225 |
|
66712 | 226 |
fun theory_name qualifier theory = |
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
66771
diff
changeset
|
227 |
if Long_Name.is_qualified theory orelse is_some (global_theory theory) |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
66771
diff
changeset
|
228 |
then theory |
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
66771
diff
changeset
|
229 |
else Long_Name.qualify qualifier theory; |
65471
05e5bffcf1d8
clarified loaded_theories: map to qualified theory name;
wenzelm
parents:
65457
diff
changeset
|
230 |
|
72613
d01ea9e3bd2d
clarified bibtex_entries: refer to overall session structure;
wenzelm
parents:
72511
diff
changeset
|
231 |
fun theory_bibtex_entries theory = |
72758 | 232 |
Symtab.lookup_list (get_session_base1 #bibtex_entries) (theory_qualifier theory); |
72613
d01ea9e3bd2d
clarified bibtex_entries: refer to overall session structure;
wenzelm
parents:
72511
diff
changeset
|
233 |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70049
diff
changeset
|
234 |
fun find_theory_file thy_name = |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
235 |
let |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
236 |
val thy_file = thy_path (Path.basic (Long_Name.base_name thy_name)); |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
237 |
val session = theory_qualifier thy_name; |
72758 | 238 |
val dirs = Symtab.lookup_list (get_session_base1 #session_directories) session; |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
239 |
in |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
240 |
dirs |> get_first (fn dir => |
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72162
diff
changeset
|
241 |
let val path = dir + thy_file |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
242 |
in if File.is_file path then SOME path else NONE end) |
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
243 |
end; |
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70049
diff
changeset
|
244 |
|
70717
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
245 |
fun make_theory_node node_name theory = |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
246 |
{node_name = node_name, master_dir = Path.dir node_name, theory_name = theory}; |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
247 |
|
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
248 |
fun loaded_theory_node theory = |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
249 |
{node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}; |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
250 |
|
65454 | 251 |
fun import_name qualifier dir s = |
70717
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
252 |
let |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
253 |
val theory = theory_name qualifier (Thy_Header.import_name s); |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
254 |
fun theory_node () = |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
255 |
make_theory_node (File.full_path dir (thy_path (Path.expand (Path.explode s)))) theory; |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
256 |
in |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
257 |
if not (Thy_Header.is_base_name s) then theory_node () |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
258 |
else if loaded_theory theory then loaded_theory_node theory |
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
66771
diff
changeset
|
259 |
else |
70717
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
260 |
(case find_theory_file theory of |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
261 |
SOME node_name => make_theory_node node_name theory |
cceb10dcc9f9
clarified import_name: observe directory notation more strictly;
wenzelm
parents:
70712
diff
changeset
|
262 |
| NONE => if Long_Name.is_qualified s then loaded_theory_node theory else theory_node ()) |
67104
a2fa0c6a7aff
clarified theory_name vs. loaded_theory: proper import_name for already loaded theories from other sessions (amending 4c98c929a12a);
wenzelm
parents:
66771
diff
changeset
|
263 |
end; |
65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65442
diff
changeset
|
264 |
|
48878 | 265 |
fun check_file dir file = File.check_file (File.full_path dir file); |
266 |
||
54525 | 267 |
fun check_thy dir thy_name = |
268 |
let |
|
65433 | 269 |
val thy_base_name = Long_Name.base_name thy_name; |
270 |
val master_file = |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70049
diff
changeset
|
271 |
(case find_theory_file thy_name of |
70712
a3cfe859d915
find theories via session directories only -- ignore known_theories;
wenzelm
parents:
70683
diff
changeset
|
272 |
SOME path => check_file Path.current path |
65442 | 273 |
| NONE => check_file dir (thy_path (Path.basic thy_base_name))); |
54525 | 274 |
val text = File.read master_file; |
275 |
||
276 |
val {name = (name, pos), imports, keywords} = |
|
277 |
Thy_Header.read (Path.position master_file) text; |
|
65433 | 278 |
val _ = |
279 |
thy_base_name <> name andalso |
|
280 |
error ("Bad theory name " ^ quote name ^ |
|
65442 | 281 |
" for file " ^ Path.print (Path.base master_file) ^ Position.here pos); |
54525 | 282 |
in |
283 |
{master = (master_file, SHA1.digest text), text = text, theory_pos = pos, |
|
284 |
imports = imports, keywords = keywords} |
|
285 |
end; |
|
286 |
||
287 |
||
54526 | 288 |
(* load files *) |
48898
9fc880720663
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
wenzelm
parents:
48897
diff
changeset
|
289 |
|
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
290 |
fun parse_files make_paths = |
48898
9fc880720663
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
wenzelm
parents:
48897
diff
changeset
|
291 |
Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy => |
9fc880720663
simplified Thy_Load.check_thy (again) -- no need to pass keywords nor find files in body text;
wenzelm
parents:
48897
diff
changeset
|
292 |
(case Token.get_files tok of |
54526 | 293 |
[] => |
294 |
let |
|
295 |
val master_dir = master_directory thy; |
|
55708 | 296 |
val pos = Token.pos_of tok; |
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
297 |
val src_paths = make_paths (Path.explode name); |
54526 | 298 |
in map (Command.read_file master_dir pos) src_paths end |
54520
cee77d2e9582
release file errors at runtime: Command.eval instead of Command.read;
wenzelm
parents:
54519
diff
changeset
|
299 |
| files => map Exn.release files)); |
48869 | 300 |
|
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
301 |
val parse_file = parse_files single >> (fn f => f #> the_single); |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
302 |
|
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
303 |
|
48906 | 304 |
fun provide (src_path, id) = |
305 |
map_files (fn (master_dir, imports, provided) => |
|
306 |
if AList.defined (op =) provided src_path then |
|
307 |
error ("Duplicate use of source file: " ^ Path.print src_path) |
|
308 |
else (master_dir, imports, (src_path, id) :: provided)); |
|
309 |
||
69851 | 310 |
fun provide_file (file: Token.file) = provide (#src_path file, #digest file); |
311 |
||
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
312 |
fun provide_parse_files make_paths = |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
313 |
parse_files make_paths >> (fn files => fn thy => |
48906 | 314 |
let |
315 |
val fs = files thy; |
|
55788
67699e08e969
store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
wenzelm
parents:
55708
diff
changeset
|
316 |
val thy' = fold (fn {src_path, digest, ...} => provide (src_path, digest)) fs thy; |
48906 | 317 |
in (fs, thy') end); |
318 |
||
72747
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
319 |
val provide_parse_file = provide_parse_files single >> (fn f => f #>> the_single); |
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
320 |
|
5f9d66155081
clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
wenzelm
parents:
72669
diff
changeset
|
321 |
|
43702
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43700
diff
changeset
|
322 |
fun load_file thy src_path = |
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43700
diff
changeset
|
323 |
let |
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43700
diff
changeset
|
324 |
val full_path = check_file (master_directory thy) src_path; |
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43700
diff
changeset
|
325 |
val text = File.read full_path; |
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43700
diff
changeset
|
326 |
val id = SHA1.digest text; |
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43700
diff
changeset
|
327 |
in ((full_path, id), text) end; |
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43700
diff
changeset
|
328 |
|
54446 | 329 |
fun loaded_files_current thy = |
48886
9604c6563226
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm
parents:
48881
diff
changeset
|
330 |
#provided (Files.get thy) |> |
48896
bb1f461a7815
simplified Thy_Load.provide: do not store full path;
wenzelm
parents:
48888
diff
changeset
|
331 |
forall (fn (src_path, id) => |
43702
24fb44c1086a
more abstract Thy_Load.load_file/use_file for external theory resources;
wenzelm
parents:
43700
diff
changeset
|
332 |
(case try (load_file thy) src_path of |
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
333 |
NONE => false |
48886
9604c6563226
discontinued separate list of required files -- maintain only provided files as they occur at runtime;
wenzelm
parents:
48881
diff
changeset
|
334 |
| SOME ((_, id'), _) => id = id')); |
37952 | 335 |
|
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents:
37943
diff
changeset
|
336 |
|
67217 | 337 |
(* formal check *) |
49244
fb669aff821e
formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
wenzelm
parents:
48992
diff
changeset
|
338 |
|
70049 | 339 |
fun formal_check check_file ctxt opt_dir (name, pos) = |
54705 | 340 |
let |
67214 | 341 |
fun err msg = error (msg ^ Position.here pos); |
56034
1c59b555ac4a
some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
wenzelm
parents:
55882
diff
changeset
|
342 |
|
67214 | 343 |
val _ = Context_Position.report ctxt pos Markup.language_path; |
70049 | 344 |
val dir = |
345 |
(case opt_dir of |
|
346 |
SOME dir => dir |
|
347 |
| NONE => master_directory (Proof_Context.theory_of ctxt)); |
|
72511
460d743010bc
clarified signature: overloaded "+" for Path.append;
wenzelm
parents:
72162
diff
changeset
|
348 |
val path = dir + Path.explode name handle ERROR msg => err msg; |
67214 | 349 |
val _ = Path.expand path handle ERROR msg => err msg; |
72162 | 350 |
val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path)); |
67214 | 351 |
val _ = check_file path handle ERROR msg => err msg; |
63675 | 352 |
in path end; |
353 |
||
67217 | 354 |
val check_path = formal_check I; |
355 |
val check_file = formal_check File.check_file; |
|
356 |
val check_dir = formal_check File.check_dir; |
|
357 |
||
358 |
||
359 |
(* antiquotations *) |
|
360 |
||
361 |
local |
|
362 |
||
70049 | 363 |
fun document_antiq (check: Proof.context -> Path.T option -> string * Position.T -> Path.T) = |
69281 | 364 |
Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => |
365 |
let |
|
70049 | 366 |
val _ = check ctxt NONE (name, pos); |
71899 | 367 |
val latex = Latex.string (Latex.output_ascii_breakable "/" name); |
368 |
in Latex.enclose_block "\\isatt{" "}" [latex] end); |
|
54705 | 369 |
|
69281 | 370 |
fun ML_antiq check = |
371 |
Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, (name, pos)) => |
|
70049 | 372 |
check ctxt (SOME Path.current) (name, pos) |> ML_Syntax.print_path); |
63675 | 373 |
|
56135 | 374 |
in |
375 |
||
53171 | 376 |
val _ = Theory.setup |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
377 |
(Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>session\<close> |
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:
69289
diff
changeset
|
378 |
(Scan.lift Parse.embedded_position) check_session #> |
69592
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
379 |
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
380 |
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
381 |
Thy_Output.antiquotation_raw_embedded \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
382 |
ML_Antiquotation.value_embedded \<^binding>\<open>path\<close> (ML_antiq check_path) #> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
383 |
ML_Antiquotation.value_embedded \<^binding>\<open>file\<close> (ML_antiq check_file) #> |
a80d8ec6c998
support for isabelle update -u control_cartouches;
wenzelm
parents:
69349
diff
changeset
|
384 |
ML_Antiquotation.value_embedded \<^binding>\<open>dir\<close> (ML_antiq check_dir) #> |
70015
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
69851
diff
changeset
|
385 |
ML_Antiquotation.value_embedded \<^binding>\<open>path_binding\<close> |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
69851
diff
changeset
|
386 |
(Scan.lift (Parse.position Parse.path) >> |
c8e08d8ffb93
clarified signature: more explicit type Path.binding;
wenzelm
parents:
69851
diff
changeset
|
387 |
(ML_Syntax.print_path_binding o Path.explode_binding)) #> |
69282 | 388 |
ML_Antiquotation.value \<^binding>\<open>master_dir\<close> |
389 |
(Args.theory >> (ML_Syntax.print_path o master_directory))); |
|
49244
fb669aff821e
formal markup for @{file} (for hyperlinks etc.) -- interpret path wrt. master directory as usual;
wenzelm
parents:
48992
diff
changeset
|
390 |
|
6168 | 391 |
end; |
56135 | 392 |
|
393 |
end; |