equal
deleted
inserted
replaced
13 structure SPARK_Commands: SPARK_COMMANDS = |
13 structure SPARK_Commands: SPARK_COMMANDS = |
14 struct |
14 struct |
15 |
15 |
16 fun spark_open header (prfx, files) thy = |
16 fun spark_open header (prfx, files) thy = |
17 let |
17 let |
18 val ([{src_path, text = vc_text, pos = vc_pos, ...}, |
18 val ([{src_path, text = vc_text, pos = vc_pos, ...}: Token.file, |
19 {text = fdl_text, pos = fdl_pos, ...}, |
19 {text = fdl_text, pos = fdl_pos, ...}, |
20 {text = rls_text, pos = rls_pos, ...}], thy') = files thy; |
20 {text = rls_text, pos = rls_pos, ...}], thy') = files thy; |
21 val base = fst (Path.split_ext (File.full_path (Thy_Load.master_directory thy') src_path)); |
21 val base = fst (Path.split_ext (File.full_path (Thy_Load.master_directory thy') src_path)); |
22 in |
22 in |
23 SPARK_VCs.set_vcs |
23 SPARK_VCs.set_vcs |