equal
deleted
inserted
replaced
13 {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, |
13 {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, |
14 imports: (string * Position.T) list, keywords: Thy_Header.keywords} |
14 imports: (string * Position.T) list, keywords: Thy_Header.keywords} |
15 val parse_files: string -> (theory -> Token.file list) parser |
15 val parse_files: string -> (theory -> Token.file list) parser |
16 val provide: Path.T * SHA1.digest -> theory -> theory |
16 val provide: Path.T * SHA1.digest -> theory -> theory |
17 val provide_parse_files: string -> (theory -> Token.file list * theory) parser |
17 val provide_parse_files: string -> (theory -> Token.file list * theory) parser |
18 val loaded_files: theory -> Path.T list |
|
19 val loaded_files_current: theory -> bool |
18 val loaded_files_current: theory -> bool |
20 val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory |
19 val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory |
21 val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T -> |
20 val load_thy: bool -> (Toplevel.transition -> Time.time option) -> int -> Path.T -> |
22 Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int |
21 Thy_Header.header -> Position.T -> string -> theory list -> theory * (unit -> unit) * int |
23 end; |
22 end; |
113 #provided (Files.get thy) |> |
112 #provided (Files.get thy) |> |
114 forall (fn (src_path, id) => |
113 forall (fn (src_path, id) => |
115 (case try (load_file thy) src_path of |
114 (case try (load_file thy) src_path of |
116 NONE => false |
115 NONE => false |
117 | SOME ((_, id'), _) => id = id')); |
116 | SOME ((_, id'), _) => id = id')); |
118 |
|
119 (*Proof General legacy*) |
|
120 fun loaded_files thy = |
|
121 let val {master_dir, provided, ...} = Files.get thy |
|
122 in map (File.full_path master_dir o #1) provided end; |
|
123 |
117 |
124 |
118 |
125 (* load theory *) |
119 (* load theory *) |
126 |
120 |
127 fun begin_theory master_dir {name, imports, keywords} parents = |
121 fun begin_theory master_dir {name, imports, keywords} parents = |