# HG changeset patch
# User wenzelm
# Date 1590605485 -7200
# Node ID b9fbc93f3a248cff14262436abc9bd0ed97f2db2
# Parent  d2509353648265a2698e253495ecca40578c4b87
clarified markup;

diff -r d25093536482 -r b9fbc93f3a24 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed May 27 20:38:59 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed May 27 20:51:25 2020 +0200
@@ -68,8 +68,6 @@
   val export_pathN: string val export_path: string -> T
   val urlN: string val url: string -> T
   val docN: string val doc: string -> T
-  val bash_functionN: string val bash_function: string -> T
-  val scala_functionN: string val scala_function: string -> T
   val markupN: string
   val consistentN: string
   val unbreakableN: string
@@ -83,6 +81,8 @@
   val wordsN: string val words: T
   val hiddenN: string val hidden: T
   val deleteN: string val delete: T
+  val bash_functionN: string
+  val scala_functionN: string
   val system_optionN: string
   val sessionN: string
   val theoryN: string
@@ -407,8 +407,6 @@
 val (export_pathN, export_path) = markup_string "export_path" nameN;
 val (urlN, url) = markup_string "url" nameN;
 val (docN, doc) = markup_string "doc" nameN;
-val (bash_functionN, bash_function) = markup_string "bash_function" nameN;
-val (scala_functionN, scala_function) = markup_string "scala_function" nameN;
 
 
 (* pretty printing *)
@@ -450,6 +448,8 @@
 
 (* misc entities *)
 
+val bash_functionN = "bash_function";
+val scala_functionN = "scala_function";
 val system_optionN = "system_option";
 
 val sessionN = "session";
diff -r d25093536482 -r b9fbc93f3a24 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed May 27 20:38:59 2020 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed May 27 20:51:25 2020 +0200
@@ -95,8 +95,8 @@
 fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
 
 
-fun check_name which kind markup ctxt (name, pos) =
-  Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt (name, pos);
+fun check_name which kind markup ctxt arg =
+  Completion.check_item kind markup (get_session_base which |> sort_by #1) ctxt arg;
 
 val check_session =
   check_name #session_positions "session"
diff -r d25093536482 -r b9fbc93f3a24 src/Pure/System/isabelle_system.ML
--- a/src/Pure/System/isabelle_system.ML	Wed May 27 20:38:59 2020 +0200
+++ b/src/Pure/System/isabelle_system.ML	Wed May 27 20:51:25 2020 +0200
@@ -52,8 +52,8 @@
   |> split_lines |> map_filter (space_explode " " #> try List.last);
 
 fun check_bash_function ctxt arg =
-  Completion.check_item Markup.bash_functionN (Markup.bash_function o #1)
-    (bash_functions () |> map (rpair ())) ctxt arg;
+  Completion.check_entity Markup.bash_functionN
+    (bash_functions () |> map (rpair Position.none)) ctxt arg;
 
 
 (* directory operations *)
diff -r d25093536482 -r b9fbc93f3a24 src/Pure/System/scala.ML
--- a/src/Pure/System/scala.ML	Wed May 27 20:38:59 2020 +0200
+++ b/src/Pure/System/scala.ML	Wed May 27 20:51:25 2020 +0200
@@ -76,8 +76,8 @@
 fun functions () = space_explode "," (getenv "ISABELLE_SCALA_FUNCTIONS");
 
 fun check_function ctxt arg =
-  Completion.check_item Markup.scala_functionN (Markup.scala_function o #1)
-    (functions () |> sort_strings |> map (rpair ())) ctxt arg;
+  Completion.check_entity Markup.scala_functionN
+    (functions () |> sort_strings |> map (rpair Position.none)) ctxt arg;
 
 val _ = Theory.setup
  (ML_Antiquotation.inline_embedded \<^binding>\<open>scala_function\<close>