equal
deleted
inserted
replaced
16 fun read f path = f (Position.file (Path.implode path)) (File.read path); |
16 fun read f path = f (Position.file (Path.implode path)) (File.read path); |
17 |
17 |
18 fun spark_open vc_name thy = |
18 fun spark_open vc_name thy = |
19 let |
19 let |
20 val (vc_path, _) = Thy_Load.check_file |
20 val (vc_path, _) = Thy_Load.check_file |
21 [Thy_Load.master_directory thy] (Path.explode vc_name); |
21 (Thy_Load.master_directory thy) (Path.explode vc_name); |
22 val (base, header) = (case Path.split_ext vc_path of |
22 val (base, header) = |
|
23 (case Path.split_ext vc_path of |
23 (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ()) |
24 (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ()) |
24 | (base, "siv") => (base, Fdl_Lexer.siv_header >> K ()) |
25 | (base, "siv") => (base, Fdl_Lexer.siv_header >> K ()) |
25 | _ => error "File name must end with .vcg or .siv"); |
26 | _ => error "File name must end with .vcg or .siv"); |
26 val fdl_path = Path.ext "fdl" base; |
27 val fdl_path = Path.ext "fdl" base; |
27 val rls_path = Path.ext "rls" base; |
28 val rls_path = Path.ext "rls" base; |