--- a/src/HOL/Tools/Nitpick/kodkod.scala Sat Nov 28 15:15:53 2020 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Sat Nov 28 15:17:14 2020 +0100
@@ -154,6 +154,7 @@
object Fun extends Scala.Fun("kodkod")
{
+ val here = Scala_Project.here
def apply(args: String): String =
{
val (timeout, (solve_all, (max_solutions, (max_threads, kki)))) =
--- a/src/Pure/PIDE/resources.ML Sat Nov 28 15:15:53 2020 +0100
+++ b/src/Pure/PIDE/resources.ML Sat Nov 28 15:17:14 2020 +0100
@@ -14,6 +14,7 @@
bibtex_entries: (string * string list) list,
command_timings: Properties.T list,
docs: string list,
+ scala_functions: (string * Position.T) list,
global_theories: (string * string) list,
loaded_theories: string list} -> unit
val init_session_yxml: string -> unit
@@ -25,6 +26,7 @@
val session_chapter: string -> string
val last_timing: Toplevel.transition -> Time.time
val check_doc: Proof.context -> string * Position.T -> string
+ val scala_function_pos: string -> Position.T
val master_directory: theory -> Path.T
val imports_of: theory -> (string * Position.T) list
val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
@@ -103,6 +105,7 @@
bibtex_entries = Symtab.empty: string list Symtab.table,
timings = empty_timings,
docs = []: (string * entry) list,
+ scala_functions = Symtab.empty: Position.T Symtab.table,
global_theories = Symtab.empty: string Symtab.table,
loaded_theories = Symtab.empty: unit Symtab.table};
@@ -110,8 +113,8 @@
Synchronized.var "Sessions.base" empty_session_base;
fun init_session
- {session_positions, session_directories, session_chapters,
- bibtex_entries, command_timings, docs, global_theories, loaded_theories} =
+ {session_positions, session_directories, session_chapters, bibtex_entries,
+ command_timings, docs, scala_functions, global_theories, loaded_theories} =
Synchronized.change global_session_base
(fn _ =>
{session_positions = sort_by #1 (map (apsnd make_entry) session_positions),
@@ -122,19 +125,22 @@
bibtex_entries = Symtab.make bibtex_entries,
timings = make_timings command_timings,
docs = sort_by #1 (map (apsnd make_entry o rpair []) docs),
+ scala_functions = Symtab.make scala_functions,
global_theories = Symtab.make global_theories,
loaded_theories = Symtab.make_set loaded_theories});
fun init_session_yxml yxml =
let
- val (session_positions, (session_directories, (session_chapters,
- (bibtex_entries, (command_timings, (docs, (global_theories, loaded_theories))))))) =
+ val (session_positions, (session_directories, (session_chapters, (bibtex_entries,
+ (command_timings, (docs, (scala_functions, (global_theories, loaded_theories)))))))) =
YXML.parse_body yxml |>
let open XML.Decode in
(pair (list (pair string properties))
(pair (list (pair string string)) (pair (list (pair string string))
(pair (list (pair string (list string))) (pair (list properties)
- (pair (list string) (pair (list (pair string string)) (list string))))))))
+ (pair (list string)
+ (pair (list (pair string properties))
+ (pair (list (pair string string)) (list string)))))))))
end;
in
init_session
@@ -144,6 +150,7 @@
bibtex_entries = bibtex_entries,
command_timings = command_timings,
docs = docs,
+ scala_functions = map (apsnd Position.of_properties) scala_functions,
global_theories = global_theories,
loaded_theories = loaded_theories}
end;
@@ -160,6 +167,7 @@
bibtex_entries = Symtab.empty,
timings = empty_timings,
docs = [],
+ scala_functions = Symtab.empty,
global_theories = global_theories,
loaded_theories = loaded_theories});
@@ -184,6 +192,10 @@
val check_doc = check_name #docs "documentation" (Markup.doc o #1);
+fun scala_function_pos name =
+ Symtab.lookup (get_session_base #scala_functions) name
+ |> the_default Position.none;
+
(* manage source files *)
--- a/src/Pure/PIDE/resources.scala Sat Nov 28 15:15:53 2020 +0100
+++ b/src/Pure/PIDE/resources.scala Sat Nov 28 15:17:14 2020 +0100
@@ -34,15 +34,17 @@
pair(list(pair(string, list(string))),
pair(list(properties),
pair(list(string),
- pair(list(pair(string, string)), list(string))))))))(
+ pair(list(pair(string, properties)),
+ pair(list(pair(string, string)), list(string)))))))))(
(sessions_structure.session_positions,
(sessions_structure.dest_session_directories,
(sessions_structure.session_chapters,
(sessions_structure.bibtex_entries,
(command_timings,
(session_base.doc_names,
+ (Scala.functions.map(fun => (fun.name, fun.position)),
(session_base.global_theories.toList,
- session_base.loaded_theories.keys)))))))))
+ session_base.loaded_theories.keys))))))))))
}
--- a/src/Pure/System/scala.ML Sat Nov 28 15:15:53 2020 +0100
+++ b/src/Pure/System/scala.ML Sat Nov 28 15:17:14 2020 +0100
@@ -79,7 +79,7 @@
fun check_function ctxt arg =
Completion.check_entity Markup.scala_functionN
- (functions () |> sort_strings |> map (rpair Position.none)) ctxt arg;
+ (functions () |> sort_strings |> map (fn a => (a, Resources.scala_function_pos a))) ctxt arg;
val _ = Theory.setup
(ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>
--- a/src/Pure/System/scala.scala Sat Nov 28 15:15:53 2020 +0100
+++ b/src/Pure/System/scala.scala Sat Nov 28 15:17:14 2020 +0100
@@ -20,6 +20,8 @@
abstract class Fun(val name: String) extends Function[String, String]
{
override def toString: String = name
+ def position: Properties.T = here.position
+ def here: Scala_Project.Here
def apply(arg: String): String
}
@@ -34,11 +36,13 @@
object Echo extends Fun("echo")
{
+ val here = Scala_Project.here
def apply(arg: String): String = arg
}
object Sleep extends Fun("sleep")
{
+ val here = Scala_Project.here
def apply(seconds: String): String =
{
val t =
@@ -123,6 +127,7 @@
object Toplevel extends Fun("scala_toplevel")
{
+ val here = Scala_Project.here
def apply(arg: String): String =
{
val (interpret, source) =
--- a/src/Pure/Thy/bibtex.scala Sat Nov 28 15:15:53 2020 +0100
+++ b/src/Pure/Thy/bibtex.scala Sat Nov 28 15:17:14 2020 +0100
@@ -147,6 +147,7 @@
object Check_Database extends Scala.Fun("bibtex_check_database")
{
+ val here = Scala_Project.here
def apply(database: String): String =
{
import XML.Encode._