6 |
6 |
7 signature RESOURCES = |
7 signature RESOURCES = |
8 sig |
8 sig |
9 val default_qualifier: string |
9 val default_qualifier: string |
10 val init_session: |
10 val init_session: |
11 {pide: bool, |
11 {session_positions: (string * Properties.T) list, |
12 session_positions: (string * Properties.T) list, |
|
13 session_directories: (string * string) list, |
12 session_directories: (string * string) list, |
14 docs: string list, |
13 docs: string list, |
15 global_theories: (string * string) list, |
14 global_theories: (string * string) list, |
16 loaded_theories: string list} -> unit |
15 loaded_theories: string list} -> unit |
17 val finish_session_base: unit -> unit |
16 val finish_session_base: unit -> unit |
18 val is_pide: unit -> bool |
|
19 val global_theory: string -> string option |
17 val global_theory: string -> string option |
20 val loaded_theory: string -> bool |
18 val loaded_theory: string -> bool |
21 val check_session: Proof.context -> string * Position.T -> string |
19 val check_session: Proof.context -> string * Position.T -> string |
22 val check_doc: Proof.context -> string * Position.T -> string |
20 val check_doc: Proof.context -> string * Position.T -> string |
23 val master_directory: theory -> Path.T |
21 val master_directory: theory -> Path.T |
52 |
50 |
53 fun make_entry props : entry = |
51 fun make_entry props : entry = |
54 {pos = Position.of_properties props, serial = serial ()}; |
52 {pos = Position.of_properties props, serial = serial ()}; |
55 |
53 |
56 val empty_session_base = |
54 val empty_session_base = |
57 {pide = false, |
55 {session_positions = []: (string * entry) list, |
58 session_positions = []: (string * entry) list, |
|
59 session_directories = Symtab.empty: Path.T list Symtab.table, |
56 session_directories = Symtab.empty: Path.T list Symtab.table, |
60 docs = []: (string * entry) list, |
57 docs = []: (string * entry) list, |
61 global_theories = Symtab.empty: string Symtab.table, |
58 global_theories = Symtab.empty: string Symtab.table, |
62 loaded_theories = Symtab.empty: unit Symtab.table}; |
59 loaded_theories = Symtab.empty: unit Symtab.table}; |
63 |
60 |
64 val global_session_base = |
61 val global_session_base = |
65 Synchronized.var "Sessions.base" empty_session_base; |
62 Synchronized.var "Sessions.base" empty_session_base; |
66 |
63 |
67 fun init_session |
64 fun init_session |
68 {pide, session_positions, session_directories, docs, global_theories, loaded_theories} = |
65 {session_positions, session_directories, docs, global_theories, loaded_theories} = |
69 Synchronized.change global_session_base |
66 Synchronized.change global_session_base |
70 (fn _ => |
67 (fn _ => |
71 {pide = pide, |
68 {session_positions = sort_by #1 (map (apsnd make_entry) session_positions), |
72 session_positions = sort_by #1 (map (apsnd make_entry) session_positions), |
|
73 session_directories = |
69 session_directories = |
74 fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) |
70 fold_rev (fn (dir, name) => Symtab.cons_list (name, Path.explode dir)) |
75 session_directories Symtab.empty, |
71 session_directories Symtab.empty, |
76 docs = sort_by #1 (map (apsnd make_entry o rpair []) docs), |
72 docs = sort_by #1 (map (apsnd make_entry o rpair []) docs), |
77 global_theories = Symtab.make global_theories, |
73 global_theories = Symtab.make global_theories, |
78 loaded_theories = Symtab.make_set loaded_theories}); |
74 loaded_theories = Symtab.make_set loaded_theories}); |
79 |
75 |
80 fun finish_session_base () = |
76 fun finish_session_base () = |
81 Synchronized.change global_session_base |
77 Synchronized.change global_session_base |
82 (fn {global_theories, loaded_theories, ...} => |
78 (fn {global_theories, loaded_theories, ...} => |
83 {pide = false, |
79 {session_positions = [], |
84 session_positions = [], |
|
85 session_directories = Symtab.empty, |
80 session_directories = Symtab.empty, |
86 docs = [], |
81 docs = [], |
87 global_theories = global_theories, |
82 global_theories = global_theories, |
88 loaded_theories = loaded_theories}); |
83 loaded_theories = loaded_theories}); |
89 |
84 |
90 fun get_session_base f = f (Synchronized.value global_session_base); |
85 fun get_session_base f = f (Synchronized.value global_session_base); |
91 |
|
92 fun is_pide () = get_session_base #pide; |
|
93 |
86 |
94 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a; |
87 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a; |
95 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; |
88 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a; |
96 |
89 |
97 |
90 |