15 load_commands: (string * Position.T) list, |
15 load_commands: (string * Position.T) list, |
16 scala_functions: (string * ((bool * bool) * Position.T)) list, |
16 scala_functions: (string * ((bool * bool) * Position.T)) list, |
17 global_theories: (string * string) list, |
17 global_theories: (string * string) list, |
18 loaded_theories: string list} -> unit |
18 loaded_theories: string list} -> unit |
19 val init_session_yxml: string -> unit |
19 val init_session_yxml: string -> unit |
20 val init_session_file: Path.T -> unit |
20 val init_session_env: unit -> unit |
21 val finish_session_base: unit -> unit |
21 val finish_session_base: unit -> unit |
22 val global_theory: string -> string option |
22 val global_theory: string -> string option |
23 val loaded_theory: string -> bool |
23 val loaded_theory: string -> bool |
24 val check_session: Proof.context -> string * Position.T -> string |
24 val check_session: Proof.context -> string * Position.T -> string |
25 val last_timing: Toplevel.transition -> Time.time |
25 val last_timing: Toplevel.transition -> Time.time |
26 val check_load_command: Proof.context -> string * Position.T -> string |
26 val check_load_command: Proof.context -> string * Position.T -> string |
27 val scala_functions: unit -> string list |
|
28 val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool) |
27 val check_scala_function: Proof.context -> string * Position.T -> string * (bool * bool) |
29 val master_directory: theory -> Path.T |
28 val master_directory: theory -> Path.T |
30 val imports_of: theory -> (string * Position.T) list |
29 val imports_of: theory -> (string * Position.T) list |
31 val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory |
30 val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory |
32 val thy_path: Path.T -> Path.T |
31 val thy_path: Path.T -> Path.T |
150 scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions, |
149 scala_functions = (map o apsnd o apsnd) Position.of_properties scala_functions, |
151 global_theories = global_theories, |
150 global_theories = global_theories, |
152 loaded_theories = loaded_theories} |
151 loaded_theories = loaded_theories} |
153 end; |
152 end; |
154 |
153 |
155 fun init_session_file path = |
154 fun init_session_env () = |
156 init_session_yxml (File.read path) before File.rm path; |
155 (case getenv "ISABELLE_INIT_SESSION" of |
|
156 "" => () |
|
157 | name => |
|
158 try File.read (Path.explode name) |
|
159 |> Option.app init_session_yxml); |
|
160 |
|
161 val _ = init_session_env (); |
157 |
162 |
158 fun finish_session_base () = |
163 fun finish_session_base () = |
159 Synchronized.change global_session_base |
164 Synchronized.change global_session_base |
160 (apfst (K (#1 empty_session_base))); |
165 (apfst (K (#1 empty_session_base))); |
161 |
166 |
178 Completion.check_entity Markup.load_commandN (get_session_base1 #load_commands) ctxt arg; |
183 Completion.check_entity Markup.load_commandN (get_session_base1 #load_commands) ctxt arg; |
179 |
184 |
180 |
185 |
181 (* Scala functions *) |
186 (* Scala functions *) |
182 |
187 |
183 (*raw bootstrap environment*) |
|
184 fun scala_functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS"); |
|
185 |
|
186 val scala_function_default = the_default ((true, false), Position.none); |
|
187 |
|
188 (*regular resources*) |
|
189 fun scala_function a = |
|
190 (a, scala_function_default (Symtab.lookup (get_session_base1 #scala_functions) a)); |
|
191 |
|
192 fun check_scala_function ctxt arg = |
188 fun check_scala_function ctxt arg = |
193 let |
189 let |
194 val funs = scala_functions () |> sort_strings |> map scala_function; |
190 val table = get_session_base1 #scala_functions; |
195 val name = Completion.check_entity Markup.scala_functionN (map (apsnd #2) funs) ctxt arg; |
191 val funs = Symtab.fold (fn (a, (_, pos)) => cons (a, pos)) table [] |> sort_by #1; |
196 val flags = #1 (scala_function_default (AList.lookup (op =) funs name)); |
192 val name = Completion.check_entity Markup.scala_functionN funs ctxt arg; |
|
193 val flags = #1 (the (Symtab.lookup table name)); |
197 in (name, flags) end; |
194 in (name, flags) end; |
198 |
195 |
199 val _ = Theory.setup |
196 val _ = Theory.setup |
200 (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close> |
197 (Document_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_function\<close> |
201 (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #> |
198 (Scan.lift Parse.embedded_position) (#1 oo check_scala_function) #> |