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